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

F G (q ∨ Y (p S (p ∧ ¬ q))) Equivalent: F G (q ∨ Y (p S (p ∧ ¬ q))) F G p ∨ F G q
Complement: ¬ (F G p ∨ F G q) ¬ F G (q ∨ Y (p S (p ∧ ¬ q))) G F (¬ q ∧ Z ((¬ p ∨ q) B (¬ p ∧ (¬ p ∨ q)))) G F ¬ p ∧ G F ¬ q
NBW
¬ (G F p ∧ G F q) Equivalent: ¬ (G F p ∧ G F q) F G (¬ q ∨ Z (¬ p B (q ∧ ¬ p))) F G ¬ p ∨ F G ¬ q ¬ G F (q ∧ Y (¬ q S p))
Complement: G F (q ∧ Y (¬ q S p)) G F p ∧ G F q
NBW
¬ G (p → F (q ∧ ¬ r ∧ X (¬ r U s))) Equivalent: ¬ G (p → F (q ∧ ¬ r ∧ X (¬ r U s))) F (p ∧ G (¬ q ∨ r ∨ X (¬ s W (r ∧ ¬ s))))
Complement: G (p → F (q ∧ ¬ s ∧ X (¬ s U r))) G (p → F (q ∧ ¬ r ∧ X (¬ r U s)))
NBW
¬ G (G F p → F q) Equivalent: ¬ (G F p → G F q) ¬ (G F q ∨ F G ¬ p) F (G F p ∧ G ¬ q) F G ¬ q ∧ G F p ¬ G (G F p → F q) G F p ∧ F G ¬ q
Complement: G (G F p → F q) G F p → G F q G F q ∨ F G ¬ p
NBW
¬ (G F p ∨ F G q) Equivalent: ¬ (G F p ∨ F G q) F G ¬ p ∧ G F ¬ q
Complement: G F p ∨ F G q
NBW
G F p ∧ F G q Equivalent: G F p ∧ F G q
Complement: F G ¬ p ∨ G F ¬ q
NBW
¬ G (p ∧ X F q → X F (q ∧ F r)) Equivalent: ¬ G (p ∧ X F q → X F (q ∧ F r)) F (p ∧ X F q ∧ X G (¬ q ∨ G ¬ r))
Complement: G (p ∧ X F q → X F (q ∧ F r))
NBW
p → X F q Equivalent: p → X F q
Complement:
DBW
G ¬ p ∨ F q Equivalent: ¬ F p ∨ F q G ¬ p ∨ F q
Complement:
NBW
F p U q Equivalent: F p U q
Complement:
DBW
F p ∨ G q Equivalent: F p ∨ G q
Complement:
NBW
G p → G q Equivalent: G p → G q
Complement:
NBW
G p → F q Equivalent: G p → F q
Complement:
NBW
¬ F p U q Equivalent: ¬ F p U q
Complement:
NBW
(p ∨ q) U (F ¬ q ∧ ¬ p) Equivalent: (p ∨ q) U (F ¬ q ∧ ¬ p)
Complement:
DBW