Büchi Store

Equivalent

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

Complement

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

Classification

Temporal Hierarchy
Safety

Spec Patterns
Existence

DBW-Recognizable
Yes

ID: 2915
Author: GOAL
St: 2
Tr: 12
Acceptance Condition: s0, s1