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