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