Büchi Store

Equivalent

¬ p W p W ¬ p W p W G ¬ p

Complement

¬ (¬ p W p W ¬ p W p W G ¬ p)
(((F p U (¬ p ∧ F p)) U (p ∧ F p U (¬ p ∧ F p))) U (¬ p ∧ (F p U (¬ p ∧ F p)) U (p ∧ F p U (¬ p ∧ F p)))) U (p ∧ ((F p U (¬ p ∧ F p)) U (p ∧ F p U (¬ p ∧ F p))) U (¬ p ∧ (F p U (¬ p ∧ F p)) U (p ∧ F p U (¬ p ∧ F p))))

Classification

Temporal Hierarchy
Safety

Spec Patterns
Bounded Existence

DBW-Recognizable
Yes

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

Automaton Type: Nondeterministic Büchi
#1	ID: 546		Author: GOAL	#2	ID: 569		Author: GOAL	#3	N/A
St: 5		Tr: 9	Date: 2010-01-12 00:00:00	St: 6		Tr: 11	Date: 2010-01-13 00:00:00
Description:				Description:
Download: GFF Promela Add to Cart				Download: GFF Promela Add to Cart
Acceptance condition: {s0, s1, s2, s3, s4}				Acceptance condition: {s1, s2, s3, s4, s5}

Automaton Type: Deterministic Büchi
#1	ID: 2542		Author: GOAL	#2	ID: 2563		Author: GOAL	#3	ID: 2518		Author: GOAL
St: 6		Tr: 12	Date: 2011-12-07 00:00:00	St: 6		Tr: 12	Date: 2011-12-07 00:00:00	St: 10		Tr: 20	Date: 2011-12-07 00:00:00
Description:				Description:				Description:
Download: GFF Promela Add to Cart				Download: GFF Promela Add to Cart				Download: GFF Promela Add to Cart
Acceptance condition: {s0, s1, s2, s3, s4}				Acceptance condition: {s0, s1, s2, s3, s4}				Acceptance condition: {s0, s1, s2, s4, s5}

Automaton Type: Nondeterministic Co-Büchi
#1	ID: 2262		Author: GOAL	#2	ID: 2277		Author: GOAL	#3	N/A
St: 7		Tr: 14	Date: 2011-12-07 00:00:00	St: 7		Tr: 14	Date: 2011-12-07 00:00:00
Description:				Description:
Download: GFF Add to Cart				Download: GFF Add to Cart
Acceptance condition: {s0, s6}				Acceptance condition: {s0, s6}

Automaton Type: Deterministic Co-Büchi
#1	ID: 2262		Author: GOAL	#2	ID: 2277		Author: GOAL	#3	N/A
St: 7		Tr: 14	Date: 2011-12-07 00:00:00	St: 7		Tr: 14	Date: 2011-12-07 00:00:00
Description:				Description:
Download: GFF Add to Cart				Download: GFF Add to Cart
Acceptance condition: {s0, s6}				Acceptance condition: {s0, s6}

Automaton Type: Nondeterministic Muller
#1	ID: 952		Author: GOAL	#2	ID: 973		Author: GOAL	#3	N/A
St: 5		Tr: 9	Date: 2011-12-07 00:00:00	St: 6		Tr: 11	Date: 2011-12-07 00:00:00
Description:				Description:
Download: GFF Add to Cart				Download: GFF Add to Cart
Acceptance condition: { {s0}, {s1}, {s2}, {s3}, {s4} }				Acceptance condition: { {s1}, {s2}, {s3}, {s4}, {s5} }

Automaton Type: Nondeterministic Rabin
#1	ID: 1274		Author: GOAL	#2	ID: 1295		Author: GOAL	#3	N/A
St: 5		Tr: 9	Date: 2011-12-07 00:00:00	St: 6		Tr: 11	Date: 2011-12-07 00:00:00
Description:				Description:
Download: GFF Add to Cart				Download: GFF Add to Cart
Acceptance condition: { (∅, {s0, s1, s2, s3, s4}) }				Acceptance condition: { (∅, {s1, s2, s3, s4, s5}) }

Automaton Type: Nondeterministic Streett
#1	ID: 1599		Author: GOAL	#2	ID: 1620		Author: GOAL	#3	N/A
St: 5		Tr: 9	Date: 2011-12-07 00:00:00	St: 6		Tr: 11	Date: 2011-12-07 00:00:00
Description:				Description:
Download: GFF Add to Cart				Download: GFF Add to Cart
Acceptance condition: { ({s0, s1, s2, s3, s4}, {s0, s1, s2, s3, s4}) }				Acceptance condition: { ({s1, s2, s3, s4, s5}, {s0, s1, s2, s3, s4, s5}) }

Automaton Type: Nondeterministic Parity
#1	ID: 1924		Author: GOAL	#2	ID: 1945		Author: GOAL	#3	N/A
St: 5		Tr: 9	Date: 2011-12-07 00:00:00	St: 6		Tr: 11	Date: 2011-12-07 00:00:00
Description:				Description:
Download: GFF Add to Cart				Download: GFF Add to Cart
Acceptance condition: 0: {s0, s1, s2, s3, s4}				Acceptance condition: 0: {s1, s2, s3, s4, s5}, 1: {s0}

Automaton Type: Deterministic Parity
#1	ID: 2778		Author: GOAL	#2	ID: 2799		Author: GOAL	#3	N/A
St: 6		Tr: 12	Date: 2011-12-07 00:00:00	St: 7		Tr: 14	Date: 2011-12-07 00:00:00
Description:				Description:
Download: GFF Add to Cart				Download: GFF Add to Cart
Acceptance condition: 0: {s0, s1, s2, s3, s4}, 1: {s5}				Acceptance condition: 0: {s0, s1, s2, s3, s4, s5}, 1: {s6}