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