Büchi Store

Equivalent

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

Complement

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

Classification

Temporal Hierarchy
Unknown

Spec Patterns
Response Chain

DBW-Recognizable
Unknown

ID: 2940
Author: GOAL
St: 17
Tr: 594
Acceptance Condition: s1, s2, s3, s7, s19, s20