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