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