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

View the filtered language classes in the "Containment Lattice"
G (p → X (q ∧ r)) Equivalent: G (p → X (q ∧ r))
Complement:
NBW
G (p → X (q ∧ ¬ r) ∨ ¬ q ∧ r) Equivalent: G (p → X (q ∧ ¬ r) ∨ ¬ q ∧ r)
Complement:
NBW
G (p → X (q ∧ ¬ r)) Equivalent: G (p → X (q ∧ ¬ r))
Complement:
NBW
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