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 → p U q) Equivalent: F (p ∧ ¬ q W (¬ p ∧ ¬ q)) • ¬ G (p → p U q)
Complement: G (p → p U q)
NBW
F (p ∧ (¬ p ∨ q) R (p ∨ ¬ q)) Equivalent: F (p ∧ (¬ p ∨ q) R (p ∨ ¬ q))
Complement: G (p → (p ∧ ¬ q) U (¬ p ∧ q))
NBW
¬ (G ¬ r ∨ F (r ∧ ¬ p W q)) Equivalent: ¬ (G ¬ r ∨ F (r ∧ ¬ p W q))
Complement: G ¬ r ∨ F (r ∧ ¬ p W q)
NBW
¬ (F r → (p → ¬ r U (q ∧ ¬ r)) U r) Equivalent: ¬ (F r → (p → ¬ r U (q ∧ ¬ r)) U r)
Complement: F r → (p → ¬ r U (q ∧ ¬ r)) U r
NBW
G (p → X F q) Equivalent: G (p → X F q)
Complement:
DBW
p ∧ G (p → X X p) Equivalent: p ∧ G (p → X X p)
Complement:
NBW
F G (p U q) Equivalent: F G (p U q)
Complement:
NBW
F G (F p → q) Equivalent: F G (F p → q)
Complement:
NBW
G (p → G (¬ p U q)) Equivalent: G (p → G (¬ p U q))
Complement:
NBW
G (b → X (a U b)) Equivalent: G (b → X (a U b))
Complement:
NBW
F a U G b Equivalent: F a U G b
Complement:
NBW
G (F p → F q) Equivalent: G (F p → F q)
Complement:
NBW
G (p → X F (q ∨ r)) Equivalent: G (p → X F (q ∨ r))
Complement:
DBW
G (p → G F (q ∨ r)) Equivalent: G (p → G F (q ∨ r))
Complement:
DBW
G F ¬ p ∧ F ¬ q Equivalent: G F ¬ p ∧ F ¬ q
Complement:
DBW