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