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