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 (t → (p → ¬ u U (q ∧ ¬ u ∧ ¬ s ∧ X ((¬ u ∧ ¬ s) U r))) U (u ∨ G (p → q ∧ ¬ s ∧ X (¬ s U r)))) Equivalent: G (t → (p → ¬ u U (q ∧ ¬ u ∧ ¬ s ∧ X ((¬ u ∧ ¬ s) U r))) U (u ∨ G (p → q ∧ ¬ s ∧ X (¬ s U r))))
Complement: ¬ G (t → (p → ¬ u U (q ∧ ¬ u ∧ ¬ s ∧ X ((¬ u ∧ ¬ s) U r))) U (u ∨ G (p → q ∧ ¬ s ∧ X (¬ s U r))))
NBW
F (p ∧ X p) ∧ F (q ∧ X q) Equivalent: F (p ∧ X p) ∧ F (q ∧ X q)
Complement:
DBW
F (p1 ∧ F p2) ∧ F (q1 ∧ F q2) Equivalent: F (p1 ∧ F p2) ∧ F (q1 ∧ F q2)
Complement:
DBW
G (Q → G P) → G (Q ∧ ¬ R ∧ F R → ¬ P U (S ∨ R)) → ¬ P W S Equivalent: G (Q → G P) → G (Q ∧ ¬ R ∧ F R → ¬ P U (S ∨ R)) → ¬ P W S
Complement:
NBW
¬ G (q → (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ ¬ p W r ∨ G p))))) Equivalent: ¬ G (q → (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ ¬ p W r ∨ G p)))))
Complement: G (q → (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ ¬ p W r ∨ G 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
G (q → (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ ¬ p W r ∨ G p))))) Equivalent: G (q → (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ ¬ p W r ∨ G p)))))
Complement: ¬ G (q → (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ (¬ p ∧ ¬ r) U (r ∨ (p ∧ ¬ r) U (r ∨ ¬ p W r ∨ G p)))))
NBW
F s → (q ∧ X (¬ s U r) → X (¬ s U (r ∧ F p))) U s Equivalent: F s → (q ∧ X (¬ s U r) → X (¬ s U (r ∧ F p))) U s
Complement: ¬ (F s → (q ∧ X (¬ s U r) → X (¬ s U (r ∧ F p))) U s)
NBW
¬ G (s → (p → ¬ t U (q ∧ ¬ t ∧ X (¬ t U r))) U (t ∨ G (p → q ∧ X F r))) Equivalent: ¬ G (s → (p → ¬ t U (q ∧ ¬ t ∧ X (¬ t U r))) U (t ∨ G (p → q ∧ X F r)))
Complement: G (s → (p → ¬ t U (q ∧ ¬ t ∧ X (¬ t U r))) U (t ∨ G (p → q ∧ X F r)))
NBW
G (s → (p → ¬ t U (q ∧ ¬ t ∧ X (¬ t U r))) U (t ∨ G (p → q ∧ X F r))) Equivalent: G (s → (p → ¬ t U (q ∧ ¬ t ∧ X (¬ t U r))) U (t ∨ G (p → q ∧ X F r)))
Complement: ¬ G (s → (p → ¬ t U (q ∧ ¬ t ∧ X (¬ t U r))) U (t ∨ G (p → q ∧ X F r)))
NBW
G (s ∧ F t → (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p))) U t) Equivalent: G (s ∧ F t → (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p))) U t)
Complement: ¬ G (s ∧ F t → (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p))) U t)
NBW
¬ G (t → (p → ¬ u U (q ∧ ¬ u ∧ ¬ s ∧ X ((¬ u ∧ ¬ s) U r))) U (u ∨ G (p → q ∧ ¬ s ∧ X (¬ s U r)))) Equivalent: ¬ G (t → (p → ¬ u U (q ∧ ¬ u ∧ ¬ s ∧ X ((¬ u ∧ ¬ s) U r))) U (u ∨ G (p → q ∧ ¬ s ∧ X (¬ s U r))))
Complement: G (t → (p → ¬ u U (q ∧ ¬ u ∧ ¬ s ∧ X ((¬ u ∧ ¬ s) U r))) U (u ∨ G (p → q ∧ ¬ s ∧ X (¬ s U r))))
NBW
F (p ∧ X (p ∧ X p)) ∧ F (q ∧ X (q ∧ X q)) Equivalent: F (p ∧ X (p ∧ X p)) ∧ F (q ∧ X (q ∧ X q))
Complement:
DBW
F (p1 ∧ F (p2 ∧ F p3)) ∧ F (q1 ∧ F (q2 ∧ F q3)) Equivalent: F (p1 ∧ F (p2 ∧ F p3)) ∧ F (q1 ∧ F (q2 ∧ F q3))
Complement:
DBW
G (s → (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p))) U (t ∨ G (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p))))) Equivalent: G (s → (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p))) U (t ∨ G (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p)))))
Complement: ¬ G (s → (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p))) U (t ∨ G (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p)))))
NBW