A PHP Error was encountered

Severity: Notice

Message: Undefined index: SyntaxForm

Filename: models/formulaemodel.php

Line Number: 316

A PHP Error was encountered

Severity: Notice

Message: Undefined index: Format2Form

Filename: models/formulaemodel.php

Line Number: 316

A PHP Error was encountered

Severity: Notice

Message: Undefined index: UnicodeForm

Filename: models/formulaemodel.php

Line Number: 316

A PHP Error was encountered

Severity: Notice

Message: Undefined index: SyntaxForm

Filename: models/formulaemodel.php

Line Number: 316

A PHP Error was encountered

Severity: Notice

Message: Undefined index: Format2Form

Filename: models/formulaemodel.php

Line Number: 316

A PHP Error was encountered

Severity: Notice

Message: Undefined index: UnicodeForm

Filename: models/formulaemodel.php

Line Number: 316

Büchi Store

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"
¬ (F p → ¬ q U (p ∨ r ∧ ¬ q ∧ X (¬ q U s))) Equivalent: ¬ (F p → ¬ q U (p ∨ r ∧ ¬ q ∧ X (¬ q U s))) • F p ∧ (¬ p ∧ (¬ r ∨ q ∨ X (¬ s W (q ∧ ¬ s)))) W (q ∧ ¬ p ∧ (¬ r ∨ q ∨ X (¬ s W (q ∧ ¬ s))))
Complement: F p → ¬ q U (p ∨ r ∧ ¬ q ∧ X (¬ q U s))
NBW
G (p → G (q → r ∧ X F s)) Equivalent: G (p → G (q → r ∧ X F s))
Complement: ¬ G (p → G (q → r ∧ X F s)) • ¬ G (¬ p ∨ G (¬ q ∨ r ∧ X F s)) • F (p ∧ F (q ∧ (¬ r ∨ X G ¬ s)))
NBW
G (p → G (q → r ∧ ¬ s ∧ X (¬ s U t))) Equivalent: G (p → G (q → r ∧ ¬ s ∧ X (¬ s U t)))
Complement: ¬ G (p → G (q → r ∧ ¬ s ∧ X (¬ s U t))) • F (p ∧ F (q ∧ (¬ r ∨ s ∨ X (¬ t W (s ∧ ¬ t)))))
NBW
¬ G (p → G (q → r ∧ X F s)) Equivalent: ¬ G (p → G (q → r ∧ X F s)) • ¬ G (¬ p ∨ G (¬ q ∨ r ∧ X F s)) • F (p ∧ F (q ∧ (¬ r ∨ X G ¬ s)))
Complement: G (p → G (q → r ∧ X F s))
NBW
¬ G (p → G (q → r ∧ ¬ s ∧ X (¬ s U t))) Equivalent: ¬ G (p → G (q → r ∧ ¬ s ∧ X (¬ s U t))) • F (p ∧ F (q ∧ (¬ r ∨ s ∨ X (¬ t W (s ∧ ¬ t)))))
Complement: G (p → G (q → r ∧ ¬ s ∧ X (¬ s U t)))
NBW
¬ G (s → F p → ¬ p U (t ∨ q ∧ ¬ p ∧ X (¬ p U r))) Equivalent: ¬ G (s → F p → ¬ p U (t ∨ q ∧ ¬ p ∧ X (¬ p U r)))
Complement: G (s → F p → ¬ p U (t ∨ q ∧ ¬ p ∧ X (¬ p U r)))
NBW
¬ (F s → (p → ¬ s U (q ∧ ¬ s ∧ X (¬ s U r))) U s) Equivalent: ¬ (F s → (p → ¬ s U (q ∧ ¬ s ∧ X (¬ s U r))) U s)
Complement: F s → (p → ¬ s U (q ∧ ¬ s ∧ X (¬ s U r))) U s
NBW
¬ (F t → (p → ¬ t U (q ∧ ¬ t ∧ ¬ s ∧ X ((¬ t ∧ ¬ s) U r))) U t) Equivalent: ¬ (F t → (p → ¬ t U (q ∧ ¬ t ∧ ¬ s ∧ X ((¬ t ∧ ¬ s) U r))) U t)
Complement: F t → (p → ¬ t U (q ∧ ¬ t ∧ ¬ s ∧ X ((¬ t ∧ ¬ s) U r))) U t
NBW
G F p ∧ G F q ∧ G F r Equivalent: G F p ∧ G F q ∧ G F r
Complement:
DBW
¬ (G ¬ s ∨ ¬ s U (s ∧ F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r)))) Equivalent: ¬ (G ¬ s ∨ ¬ s U (s ∧ F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r))))
Complement: G ¬ s ∨ ¬ s U (s ∧ F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r)))
NBW
F G p ∨ F G q ∨ F G r Equivalent: F G p ∨ F G q ∨ F G r
Complement:
NBW
G (p ∧ X F q → X F (q ∧ F r)) Equivalent: G (p ∧ X F q → X F (q ∧ F r))
Complement: ¬ G (p ∧ X F q → X F (q ∧ F r)) • F (p ∧ X F q ∧ X G (¬ q ∨ G ¬ r))
NBW
¬ (F s → (q ∧ X (¬ s U r) → X (¬ s U (r ∧ F p))) U s) Equivalent: ¬ (F s → (q ∧ X (¬ s U r) → X (¬ s U (r ∧ F p))) U s)
Complement: F s → (q ∧ X (¬ s U r) → X (¬ s U (r ∧ F p))) U s
NBW
Equivalent:
Complement:
NBW
Equivalent:
Complement:
NBW