Büchi Store

Equivalent

G (t → (p → ¬ u U (q ∧ ¬ u ∧ ¬ s ∧ X ((¬ u ∧ ¬ s) U r))) U (u ∨ G (p → q ∧ ¬ s ∧ X (¬ s U r))))

Complement

¬ G (t → (p → ¬ u U (q ∧ ¬ u ∧ ¬ s ∧ X ((¬ u ∧ ¬ s) U r))) U (u ∨ G (p → q ∧ ¬ s ∧ X (¬ s U r))))

Classification

Temporal Hierarchy
Unknown

Spec Patterns
Constrained Chain Patterns

DBW-Recognizable
Unknown

View this language class, its ancestors, and its descendants in the "Containment Lattice".

Automaton Type: Nondeterministic Büchi
#1	ID: 2950		Author: GOAL	#2	N/A			#3	N/A
St: 8		Tr: 372	Date: 2012-05-21 16:21:32
Description:
Download: GFF Promela Add to Cart
Acceptance condition: s1, s10, s11