Büchi Store

Equivalent

G ((¬ p1 ∧ ¬ p2) ∧ t1 ∧ t2) → F (p1 ∨ p2)

Complement

Classification

Temporal Hierarchy
Unknown

Spec Patterns
Unknown

DBW-Recognizable
Yes

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

Automaton Type: Nondeterministic Büchi
#1	ID: 3170		Author: GOAL	#2	N/A			#3	N/A
St: 2		Tr: 32	Date: 2017-02-19 22:26:10
Description:
Download: GFF Promela Add to Cart
Acceptance condition: s1

Automaton Type: Deterministic Büchi
#1	ID: 3170		Author: GOAL	#2	N/A			#3	N/A
St: 2		Tr: 32	Date: 2017-02-19 22:26:10
Description:
Download: GFF Promela Add to Cart
Acceptance condition: s1