Büchi Store

Equivalent

G (q ∧ ¬ r → p W r)

Complement

¬ G (q ∧ ¬ r → p W r)

Classification

Temporal Hierarchy
Safety

Spec Patterns
Universality

DBW-Recognizable
Yes

ID: 2921
Author: GOAL
St: 2
Tr: 13
Acceptance Condition: s0, s1