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 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
G F p ∨ F G q Equivalent: G F p ∨ F G q
Complement: ¬ (G F p ∨ F G q) • F G ¬ p ∧ G F ¬ q
NBW
p → G (p ∧ q) Equivalent: p → G (p ∧ q)
Complement:
NBW
p → F (p ∧ q) Equivalent: p → F (p ∧ q)
Complement:
DBW
p → X q Equivalent: p → X q
Complement:
NBW
X p → Gq Equivalent: X p → Gq
Complement:
NBW
G ¬ p ∨ Fq Equivalent: G ¬ p ∨ Fq
Complement:
NBW
G p → q Equivalent: G p → q
Complement:
DBW
G ¬ p → ¬ q Equivalent: G ¬ p → ¬ q
Complement:
DBW
a ∧ X b Equivalent: a ∧ X b
Complement:
NBW
X X → p Equivalent: X X → p
Complement:
NBW
G p → q ∨ r Equivalent: G p → q ∨ r
Complement:
DBW