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 (p → X q) Equivalent: ¬ G (p → X q)
Complement:
NBW
F p R Fq Equivalent: F p R Fq
Complement:
NBW
F p → G q Equivalent: F p → G q
Complement:
NBW
F (p R q) Equivalent: F (p R q)
Complement:
NBW
F (p ∨ G q) Equivalent: F (p ∨ G q)
Complement:
NBW
G F ¬ p ∧ ¬ q Equivalent: G F ¬ p ∧ ¬ q
Complement:
NBW
¬ p ∧ G F ¬ p Equivalent: ¬ p ∧ G F ¬ p
Complement:
NBW
G F ¬ p ∧ q Equivalent: G F ¬ p ∧ q
Complement:
NBW
G ¬ p W q Equivalent: G ¬ p W q
Complement:
NBW
X p R q Equivalent: X p R q
Complement:
NBW
X p U q Equivalent: X p U q
Complement:
NBW
G p ∨ G q Equivalent: G p ∨ G q • G q ∨ G p • G (H p ∨ H q)
Complement: ¬ (G p ∨ G q) • F ¬ p ∧ F ¬ q • F ¬ q ∧ F ¬ p • ¬ (G q ∨ G p) • F (O ¬ p ∧ O ¬ q) • ¬ G (H p ∨ H q)
NBW
G ¬ p ∨ G ¬ q Equivalent: ¬ (F p ∧ F q) • G ¬ p ∨ G ¬ q
Complement: F p ∧ F q
NBW
¬ ((p ∨ Z q) U r) Equivalent: ¬ ((p ∨ Z q) U r) • ¬ (p ∨ Z q) R ¬ r • ¬ r W (¬ p ∧ Y ¬ q ∧ ¬ r)
Complement: (p ∨ Z q) U r
NBW
F p → ¬ q U (r ∨ p) Equivalent: F p → ¬ q U (r ∨ p)
Complement: F p ∧ (¬ r ∧ ¬ p) W (q ∧ ¬ r ∧ ¬ p) • ¬ (F p → ¬ q U (r ∨ p))
NBW