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 (s ∧ F t → ¬ p U (t ∨ q ∧ ¬ p ∧ X (¬ p U r))) Equivalent: G (s ∧ F t → ¬ p U (t ∨ q ∧ ¬ p ∧ X (¬ p U r)))
Complement: ¬ G (s ∧ F t → ¬ p U (t ∨ q ∧ ¬ p ∧ X (¬ p U r)))
NBW
G (s → F p → ¬ p U (t ∨ q ∧ ¬ p ∧ X (¬ p U r))) Equivalent: G (s → F p → ¬ p U (t ∨ q ∧ ¬ p ∧ X (¬ p U r)))
Complement: ¬ G (s → F p → ¬ p U (t ∨ q ∧ ¬ p ∧ X (¬ p U r)))
NBW
¬ (F q → (¬ p ∧ ¬ q) U (q ∨ (p ∧ ¬ q) U (q ∨ (¬ p ∧ ¬ q) U (q ∨ (p ∧ ¬ q) U (q ∨ ¬ p U q))))) Equivalent: ¬ (F q → (¬ p ∧ ¬ q) U (q ∨ (p ∧ ¬ q) U (q ∨ (¬ p ∧ ¬ q) U (q ∨ (p ∧ ¬ q) U (q ∨ ¬ p U q)))))
Complement: F q → (¬ p ∧ ¬ q) U (q ∨ (p ∧ ¬ q) U (q ∨ (¬ p ∧ ¬ q) U (q ∨ (p ∧ ¬ q) U (q ∨ ¬ p U q))))
NBW
¬ (F p → ¬ p U (p ∧ ¬ q W q W ¬ q W q W G ¬ q)) Equivalent: ¬ (F p → ¬ p U (p ∧ ¬ q W q W ¬ q W q W G ¬ q)) • F p ∧ (¬ p ∨ (((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q)))) U (q ∧ ((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))))) W (p ∧ (¬ p ∨ (((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q)))) U (q ∧ ((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))))))
Complement: F p → ¬ p U (p ∧ ¬ q W q W ¬ q W q W G ¬ q)
NBW
G (s → ¬ (q ∧ ¬ t ∧ X (¬ t U (r ∧ ¬ t))) U (t ∨ p) ∨ G ¬ (q ∧ X F r)) Equivalent: G (s → ¬ (q ∧ ¬ t ∧ X (¬ t U (r ∧ ¬ t))) U (t ∨ p) ∨ G ¬ (q ∧ X F r))
Complement: ¬ G (s → ¬ (q ∧ ¬ t ∧ X (¬ t U (r ∧ ¬ t))) U (t ∨ p) ∨ G ¬ (q ∧ X F r))
NBW
G (s → G (q ∧ X F r → X (¬ r U (r ∧ F p)))) Equivalent: G (s → G (q ∧ X F r → X (¬ r U (r ∧ F p))))
Complement: ¬ G (s → G (q ∧ X F r → X (¬ r U (r ∧ F p))))
NBW
G (G (cond1 → F cond2) ∧ G (cond2 → F cond1) ∧ G (cond3 → F cond4)) → G (cond5 → F cond6) Equivalent: G (G (cond1 → F cond2) ∧ G (cond2 → F cond1) ∧ G (cond3 → F cond4)) → G (cond5 → F cond6)
Complement:
NBW
G F p ∧ G F q ∧ G F r ∧ G F s ∧ G F t ∧ G F u Equivalent: G F p ∧ G F q ∧ G F r ∧ G F s ∧ G F t ∧ G F u
Complement:
DBW
F G p ∨ F G q ∨ F G r ∨ F G s ∨ F G t ∨ F G u Equivalent: F G p ∨ F G q ∨ F G r ∨ F G s ∨ F G t ∨ F G u
Complement:
NBW
F p1 ∧ F p2 ∧ F p3 Equivalent: F p1 ∧ F p2 ∧ F p3
Complement:
DBW
G (p → X X X q) Equivalent: G (p → X X X q)
Complement:
NBW
(G p → G F q) ∧ F r Equivalent: (G p → G F q) ∧ F r
Complement:
NBW
F q → (¬ p ∧ ¬ q) U (q ∨ (p ∧ ¬ q) U (q ∨ (¬ p ∧ ¬ q) U (q ∨ (p ∧ ¬ q) U (q ∨ ¬ p U q)))) Equivalent: F q → (¬ p ∧ ¬ q) U (q ∨ (p ∧ ¬ q) U (q ∨ (¬ p ∧ ¬ q) U (q ∨ (p ∧ ¬ q) U (q ∨ ¬ p U q))))
Complement: ¬ (F q → (¬ p ∧ ¬ q) U (q ∨ (p ∧ ¬ q) U (q ∨ (¬ p ∧ ¬ q) U (q ∨ (p ∧ ¬ q) U (q ∨ ¬ p U q)))))
NBW
G ¬ s ∨ ¬ s U (s ∧ (F (q ∧ X F r) → ¬ q U p)) Equivalent: G ¬ s ∨ ¬ s U (s ∧ (F (q ∧ X F r) → ¬ q U p))
Complement: ¬ (G ¬ s ∨ ¬ s U (s ∧ (F (q ∧ X F r) → ¬ q U p)))
NBW
¬ G (q ∧ F r → (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ ¬ p U r))))) Equivalent: ¬ G (q ∧ F r → (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ ¬ p U r)))))
Complement: G (q ∧ F r → (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ ¬ p U r)))))
NBW