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 U p) Equivalent: ¬ G (p → ¬ q U p)
Complement:
NBW
G (p ∧ X ¬ p) Equivalent: G (p ∧ X ¬ p)
Complement:
NBW
G (¬ p ∨ ¬ q) ∧ G (¬ p ∨ ¬ r) ∧ G (¬ q ∨ ¬ r) Equivalent: G (¬ p ∨ ¬ q) ∧ G (¬ p ∨ ¬ r) ∧ G (¬ q ∨ ¬ r)
Complement: ¬ (G (¬ p ∨ ¬ q) ∧ G (¬ p ∨ ¬ r) ∧ G (¬ q ∨ ¬ r))
NBW
p ∧ q ∧ Fr Equivalent: p ∧ q ∧ Fr
Complement:
NBW
F (p → Fq) Equivalent: F (p → Fq)
Complement:
DBW
¬ G (¬ p → q) Equivalent: ¬ G (¬ p → q)
Complement:
DBW
G p ∧ q Equivalent: G p ∧ q
Complement:
NBW
G p ∧ ¬ q Equivalent: G p ∧ ¬ q
Complement:
NBW
¬ p ∧ G q Equivalent: ¬ p ∧ G q
Complement:
NBW
F (¬ p ∨ q) Equivalent: F (¬ p ∨ q)
Complement:
DBW
G ¬ p ∧ ¬ q Equivalent: G ¬ p ∧ ¬ q
Complement:
NBW
(p ∨ q) U (¬ q ∧ ¬ p) Equivalent: (p ∨ q) U (¬ q ∧ ¬ p)
Complement:
DBW
¬ p W (p ∧ ¬ q) Equivalent: ¬ p W (p ∧ ¬ q)
Complement:
NBW
(p ∧ q) U (p ∨ q) Equivalent: (p ∧ q) U (p ∨ q)
Complement:
NBW
(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