Büchi · co-Büchi · Rabin · Streett
A run on an infinite word never ends, so acceptance can't be “did we stop somewhere good?” It has to be a property of what happens infinitely often. Four classical answers, side by side.
The one thing that matters
For a run ρ, write Inf(ρ) for the set of states visited infinitely often. Since the state space is finite, Inf(ρ) is non-empty, and every finite prefix of the run is irrelevant to it. Every condition below is a predicate on Inf(ρ) and nothing else — two runs with the same limit set are accepted or rejected together.
Two abbreviations do all the work:
Inf(S) ≡ Inf(ρ) ∩ S ≠ ∅ Fin(S) ≡ Inf(ρ) ∩ S = ∅
Read Inf(S) as “the run keeps coming back to S” and Fin(S) as “the run eventually leaves S and never returns.” Note that Fin is exactly ¬Inf — the duality between the conditions falls out of that one fact.
The four conditions
Inf(F) ≡ Inf(ρ) ∩ F ≠ ∅
A single set F of accepting states. The run is accepted if it hits F again and again, forever. The simplest possible answer, and the one most tools are built around.
The gaps between visits can grow without bound. Büchi says nothing about how often — only that there is always a next time.
Fin(F) ≡ Inf(ρ) ∩ F = ∅
The complement of Büchi. Now F marks states the run must eventually stop visiting: there is some point after which the run stays out of F forever. Good for “eventually the system settles.”
The vertical rule marks the last visit to F. Its position is unbounded — no fixed deadline exists, which is exactly why deterministic co-Büchi automata cannot express recurrence.
⋁ᵢ ( Fin(Bᵢ) ∧ Inf(Gᵢ) )
A list of pairs (B₁,G₁) … (B_k,G_k). The run is accepted if at least one pair works out: the run eventually abandons Bᵢ for good, while returning to Gᵢ forever. One witnessing pair is enough; the others may fail freely.
Bᵢ stops (Fin) and Gᵢ keeps recurring (Inf) — the pair is witnessed. Because acceptance is a disjunction, Rabin sits naturally on the existential side: it is the condition you get from Safra determinization.
⋀ᵢ ( Fin(Bᵢ) ∨ Inf(Gᵢ) )
The dual of Rabin. Every pair must hold, and each one is a promise rather than a demand: if the run keeps returning to Bᵢ, it must also keep returning to Gᵢ. Read Bᵢ as “request” and Gᵢ as “grant” and this is strong fairness — GF request → GF grant.
Pair 1 is satisfied by granting; pair 2 is satisfied by silence — the requests stop, so nothing is owed. Both must hold simultaneously for the run to be accepted.
Try it
Since acceptance depends only on Inf(ρ), a run is fully described for our purposes by which sets it visits infinitely often. Toggle them and watch the four verdicts move.
In Inf(ρ)?
Büchi and co-Büchi use F. Rabin and Streett use the two pairs (B₁,G₁) and (B₂,G₂).
Relationships
Push a negation through Rabin and De Morgan hands you Streett with the components swapped, because ¬Fin = Inf and ¬Inf = Fin. The same move takes Büchi to co-Büchi. Complementing an automaton is therefore free at the level of the acceptance condition — the cost is all in determinization.
Both single-set conditions are degenerate one-pair cases: Büchi is Rabin with B = ∅, and co-Büchi is Streett with G = ∅.
Parity is the condition expressible as both a Rabin and a Streett condition — the chain case, where the sets are linearly ordered by inclusion. That is why parity games are the ones that sit in NP ∩ co-NP and why parity is the target of choice for synthesis: it inherits the closure properties of Rabin and Streett while keeping memoryless determinacy for both players.
| Condition | Deterministic power | Games |
|---|---|---|
| Büchi | Strictly weaker than ω-regular | Polynomial |
| co-Büchi | Strictly weaker; incomparable to Büchi | Polynomial |
| Parity | All of ω-regular | NP ∩ co-NP; quasi-polynomial |
| Rabin | All of ω-regular | NP-complete |
| Streett | All of ω-regular | co-NP-complete |
Memoryless strategies exist for the protagonist in Rabin games and for the antagonist in Streett games — the asymmetry is the same duality showing up in strategy complexity. The classic example separating deterministic Büchi from ω-regular is FG a: no deterministic Büchi automaton recognizes it.
A note on conventions
This page follows the HOA format convention: pairs are written (B, G) with Fin on the first component and Inf on the second, for both Rabin and Streett. That orientation makes the De Morgan duality literal — flip the connectives, swap Fin and Inf, and you have the other condition.
Many textbooks instead write Streett pairs as (E, F) with the condition “for all i, if F is visited infinitely often then E is too,” which puts the Inf on the first component. The conditions are the same; only the naming differs. It is worth flagging explicitly when teaching, because students reading two sources at once will otherwise conclude that one of them is wrong.