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