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