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

¬ 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
¬ G (p → ¬ p U q) Equivalent: ¬ G (p → ¬ p U q)
Complement:
DBW
G (p ∨ F q) Equivalent: G (p ∨ F q)
Complement:
DBW
G p U ¬ p Equivalent: G p U ¬ p
Complement:
NBW
G (p ∨ ¬ O q) Equivalent: G (p ∨ ¬ O q)
Complement:
NBW