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 → G (q → F r)) Equivalent: G (p → G (q → F r))
Complement: ¬ G (p → G (q → F r)) F (p ∧ F (q ∧ G ¬ r))
NBW
G (s ∧ ¬ r → (p → ¬ r U (q ∧ ¬ r)) W r) Equivalent: G (s ∧ ¬ r → (p → ¬ r U (q ∧ ¬ r)) W r)
Complement: ¬ G (s ∧ ¬ r → (p → ¬ r U (q ∧ ¬ r)) W r)
NBW
¬ G (p → F (q ∧ F r)) Equivalent: F (p ∧ G (¬ q ∨ G ¬ r)) ¬ G (p → F (q ∧ F r))
Complement: G (p → F (q ∧ F r))
NBW
G (p → F G q) Equivalent: F G (O p → q) G (p → F G q)
Complement: F (p ∧ G F ¬ q) ¬ F G (O p → q) ¬ G (p → F G q) G F (O p ∧ ¬ q)
NBW
¬ G (p → G (q → F r)) Equivalent: ¬ G (p → G (q → F r)) F (p ∧ F (q ∧ G ¬ r))
Complement: G (p → G (q → F r))
NBW
¬ (F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r))) Equivalent: ¬ (F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r))) F p ∧ (¬ q ∨ p ∨ X (¬ r W (p ∧ ¬ r))) W (p ∧ (¬ q ∨ p ∨ X (¬ r W (p ∧ ¬ r))))
Complement: F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r))
NBW
¬ G (p → F (q ∧ X F r)) Equivalent: ¬ G (p → F (q ∧ X F r))
Complement: G (p → F (q ∧ X F r))
NBW
F G a ∧ G F q Equivalent: F G a ∧ G F q
Complement:
NBW
X a ∧ G (a → X X a) Equivalent: X a ∧ G (a → X X a)
Complement:
NBW
G (Q ∧ ¬ R ∧ F R) → (P → ¬ R U (S ∧ ¬ R)) U R Equivalent: G (Q ∧ ¬ R ∧ F R) → (P → ¬ R U (S ∧ ¬ R)) U R
Complement:
NBW
F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r)) Equivalent: F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r))
Complement: ¬ (F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r))) F p ∧ (¬ q ∨ p ∨ X (¬ r W (p ∧ ¬ r))) W (p ∧ (¬ q ∨ p ∨ X (¬ r W (p ∧ ¬ r))))
NBW
F (p ∧ X F q) → ¬ p U r Equivalent: F (p ∧ X F q) → ¬ p U r
Complement: ¬ (F (p ∧ X F q) → ¬ p U r) F (p ∧ X F q) ∧ ¬ r W (p ∧ ¬ r)
NBW
F (p ∧ X F q) ∧ ¬ r W (p ∧ ¬ r) Equivalent: ¬ (F (p ∧ X F q) → ¬ p U r) F (p ∧ X F q) ∧ ¬ r W (p ∧ ¬ r)
Complement: F (p ∧ X F q) → ¬ p U r
NBW
G F (q ∧ Y (¬ q S p)) Equivalent: G F (q ∧ Y (¬ q S p)) G F p ∧ G F q
Complement: ¬ (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))
DBW
G F (¬ q ∧ Z ((¬ p ∨ q) B (¬ p ∧ (¬ p ∨ q)))) Equivalent: ¬ (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
Complement: F G (q ∨ Y (p S (p ∧ ¬ q))) F G p ∨ F G q
NBW