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