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"
F (p ∧ G q) Equivalent: F (p ∧ G q)
Complement: ¬ F (p ∧ G q) • G (¬ p ∨ F ¬ q)
NBW
¬ G (p → F q) Equivalent: F (p ∧ G ¬ q) • ¬ G (p → F q) • F G (¬ q S (p ∧ ¬ q)) • ¬ G F (¬ p B q)
Complement: G (p → F q) • G (¬ p ∨ F q) • G F (¬ p B q)
NBW
¬ G F p Equivalent: F (¬ p W (False ∧ ¬ p)) • F G ¬ p • ¬ G (True U p) • ¬ G F p • ¬ F G F p • G F G ¬ p
Complement: G (True U p) • G F p • F G F p
NBW
¬ G F (p ∨ q) Equivalent: F G (¬ p ∧ ¬ q) • ¬ G F (p ∨ q) • ¬ (G F p ∨ G F q) • F G ¬ p ∧ F G ¬ q
Complement: G F (p ∨ q) • G F p ∨ G F q
NBW
¬ (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