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 ∨ 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
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