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