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

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