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