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
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) 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