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

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