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