Büchi Store

Equivalent

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

Complement

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

Classification

Temporal Hierarchy
Unknown

Spec Patterns
Response Chain

DBW-Recognizable
Unknown

ID: 2939
Author: GOAL
St: 12
Tr: 386
Acceptance Condition: s1, s6, s7