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