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 U (q ∧ ¬ p)) Equivalent: G (p U (q ∧ ¬ p))
Complement:
NBW
G (p → G (q → Fr)) Equivalent: G (p → G (q → Fr))
Complement:
NBW
G (p → ¬ R W (P ∧ ¬ R)) Equivalent: G (p → ¬ R W (P ∧ ¬ R))
Complement:
NBW
G (p → q → F r) Equivalent: G (p → q → F r)
Complement:
DBW
G ((¬ p1 ∧ ¬ p2) ∧ t1 ∧ t2) → F (p1 ∨ p2) Equivalent: G ((¬ p1 ∧ ¬ p2) ∧ t1 ∧ t2) → F (p1 ∨ p2)
Complement:
DBW
G (p → X p) Equivalent: G (p → X p) G (p → G p)
Complement: F (p ∧ X ¬ p) F (p ∧ F ¬ p) ¬ G (p → X p) ¬ G (p → G p)
NBW
G (p ∧ ¬ q → Z (p ∨ q)) Equivalent: G (p → p B q) G (p ∧ ¬ q → Z (p ∨ q))
Complement: F (p ∧ ¬ q ∧ Y (¬ p ∧ ¬ q)) F (p ∧ ¬ q S (¬ p ∧ ¬ q)) ¬ G (p → p B q) ¬ G (p ∧ ¬ q → Z (p ∨ q))
NBW
G (p → p S q) Equivalent: G (p → p S q)
Complement: F (p ∧ ¬ q B (¬ p ∧ ¬ q)) ¬ G (p → p S q)
NBW
G (p ∧ ¬ q → X (p ∨ q)) Equivalent: G (p → p W q) G (p ∧ ¬ q → X (p ∨ q))
Complement: F (p ∧ ¬ q ∧ X (¬ p ∧ ¬ q)) F (p ∧ ¬ q U (¬ p ∧ ¬ q)) ¬ G (p → p W q) ¬ G (p ∧ ¬ q → X (p ∨ q))
NBW
G (p → ¬ q W r) Equivalent: G (p → ¬ q W r) G (q → ¬ p B r)
Complement: F (p ∧ ¬ r U (q ∧ ¬ r)) F (q ∧ ¬ r S (p ∧ ¬ r)) ¬ G (p → ¬ q W r) ¬ G (q → ¬ p B r)
NBW
G (p ∨ q S r) Equivalent: G (p ∨ q S r)
Complement: F (¬ p ∧ ¬ r B (¬ q ∧ ¬ r)) ¬ G (p ∨ q S r)
NBW
G (¬ p ∨ O ¬ q) Equivalent: ¬ F (p ∧ H q) G (¬ p ∨ O ¬ q)
Complement: F (p ∧ H q)
NBW
G (q → G ¬ p) Equivalent: G (q → G ¬ p) ¬ F (p ∧ O q) G (¬ p ∨ H ¬ q)
Complement: F (p ∧ O q) ¬ G (q → G ¬ p)
NBW
∃ t : G ((t ↔ Z ¬ t) ∧ (t → p)) Equivalent: ∃ t : G ((t ↔ Z ¬ t) ∧ (t → p)) ∃ t : t ∧ G ((t → p) ∧ (t ↔ X ¬ t)) ∃ t : t ∧ G (t ↔ X ¬ t) ∧ G (t → p)
Complement: ¬ (∃ t : t ∧ G (t ↔ X ¬ t) ∧ G (t → p)) ∀ t : ¬ t ∨ F (t ∧ X t ∨ X ¬ t ∧ ¬ t) ∨ F (t ∧ ¬ p)
NBW
G (p → q W r) Equivalent: G (p → q W r)
Complement: F (p ∧ ¬ r U (¬ q ∧ ¬ r)) ¬ G (p → q W r)
NBW