Sorted by


Refresh


Filtered by

Automaton Type

Select / Deselect All














State Size

Select / Deselect All






Formula Length

Select / Deselect All






Temporal Hierarchy

Select / Deselect All








Spec Patterns

Select / Deselect All











Refresh


Grouped By


Refresh

View the filtered language classes in the "Containment Lattice"
¬ G (p → F (q ∧ ¬ r ∧ X (¬ r U s))) Equivalent: ¬ G (p → F (q ∧ ¬ r ∧ X (¬ r U s))) • F (p ∧ G (¬ q ∨ r ∨ X (¬ s W (r ∧ ¬ s))))
Complement: G (p → F (q ∧ ¬ s ∧ X (¬ s U r))) • G (p → F (q ∧ ¬ r ∧ X (¬ r U s)))
NBW
¬ G (G F p → F q) Equivalent: ¬ (G F p → G F q) • ¬ (G F q ∨ F G ¬ p) • F (G F p ∧ G ¬ q) • F G ¬ q ∧ G F p • ¬ G (G F p → F q) • G F p ∧ F G ¬ q
Complement: G (G F p → F q) • G F p → G F q • G F q ∨ F G ¬ p
NBW
¬ (G F p ∨ F G q) Equivalent: ¬ (G F p ∨ F G q) • F G ¬ p ∧ G F ¬ q
Complement: G F p ∨ F G q
NBW
G F p ∧ F G q Equivalent: G F p ∧ F G q
Complement: F G ¬ p ∨ G F ¬ q
NBW
¬ G (p ∧ X F q → X F (q ∧ F r)) Equivalent: ¬ G (p ∧ X F q → X F (q ∧ F r)) • F (p ∧ X F q ∧ X G (¬ q ∨ G ¬ r))
Complement: G (p ∧ X F q → X F (q ∧ F r))
NBW
p → X F q Equivalent: p → X F q
Complement:
DBW
G ¬ p ∨ F q Equivalent: ¬ F p ∨ F q • G ¬ p ∨ F q
Complement:
NBW
F p U q Equivalent: F p U q
Complement:
DBW
F p ∨ G q Equivalent: F p ∨ G q
Complement:
NBW
G p → G q Equivalent: G p → G q
Complement:
NBW
G p → F q Equivalent: G p → F q
Complement:
NBW
¬ F p U q Equivalent: ¬ F p U q
Complement:
NBW
(p ∨ q) U (F ¬ q ∧ ¬ p) Equivalent: (p ∨ q) U (F ¬ q ∧ ¬ p)
Complement:
DBW
G p → X (q ∨ r) Equivalent: G p → X (q ∨ r)
Complement:
NBW
G p → q U r Equivalent: G p → q U r
Complement:
NBW