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