Büchi Automata and the Automata-Logic Correspondence

Origin. J. Richard Büchi, "On a decision method in restricted second order arithmetic" (1962), which introduced ω-automata to prove S1S decidable; Rabin (1969) extended it to trees and S2S; McNaughton (1966) gave the determinization. Vardi and Wolper's "An automata-theoretic approach to automatic program verification" (1986) turned the theorem into the technology every model checker runs on.

Models. A logic and a machine describe the same sets. Büchi's theorem says the ω-words definable in monadic second-order logic are exactly those a finite automaton accepts by visiting an accepting state infinitely often. That equivalence converts every question about a temporal formula into a question about a machine — satisfiability becomes emptiness, entailment becomes containment, model checking becomes a product construction and a cycle search.

Formalism.

Büchi automaton: A = (Q, Σ, δ, q₀, F) over infinite words. A run ρ ∈ Q^ω is accepting iff Inf(ρ) ∩ F ≠ ∅ — some accepting state recurs infinitely often. L(A) ⊆ Σ^ω is the ω-regular language accepted.

Büchi's theorem (1962): L ⊆ Σ^ω is MSO-definable iff L is ω-regular. Hence S1S — monadic second-order theory of one successor — is decidable. The decision procedure is: translate the formula to an automaton, test emptiness.

Non-determinism is essential: Deterministic Büchi automata are strictly weaker — they cannot accept "finitely many a's". McNaughton (1966): every ω-regular language is accepted by a deterministic Muller automaton. Safra (1988) gave the construction, with a 2^O(n log n) blow-up that is optimal. So the acceptance condition, not the machine, is what determinization costs.

The LTL pipeline (Vardi–Wolper 1986): LTL formula φ ⟶ Büchi automaton A_φ with L(A_φ) = models of φ System M ⟶ Büchi automaton A_M Model checking M ⊨ φ: test L(A_M) ∩ L(A_¬φ) = ∅ Emptiness = "no reachable accepting cycle" = nested depth-first search, linear time. Complexity: PSPACE-complete, and the exponential is in the formula, not the system — which is why model checking is practical.

The acceptance-condition hierarchy: Büchi ⊊ (deterministic) — but nondeterministic Büchi = Muller = Rabin = Streett = parity. Parity is the one that makes the μ-calculus's model checking a parity game.

Rabin (1969): Tree automata; S2S decidable. The hardest decidability result of its era, and the source of the decidability of most modal and temporal logics by interpretation.

Symbols.

Metatheory. Büchi's equivalence is the load-bearing theorem of verification: it is why LTL is decidable, why model checking is a graph algorithm rather than a proof search, and why the PSPACE bound sits on the formula rather than the state space. Rabin's tree theorem extends it to branching time and is the reason CTL, CTL*, and the μ-calculus are decidable — most decidability results in Modal are obtained by interpreting into S2S. The determinization gap is the subject's standing technical fact: nondeterministic Büchi automata are as expressive as any ω-automaton and cannot be determinized within the Büchi condition, so Safra's construction changes the condition and pays 2^O(n log n), which is optimal and is the bottleneck in every LTL synthesis tool.

Applies to. LTL model checking, and the SPIN/NuSMV line of tools. Decidability of temporal and modal logics via S1S and S2S. Reactive synthesis, where the determinization cost dominates. Parity games, which are the μ-calculus's acceptance condition. Descriptive complexity over infinite words.

Limitations. The translation from LTL to a Büchi automaton is exponential in the formula, and while that is where you want the exponential, it is still exponential — large specifications are the practical wall. Determinization is unavoidable for synthesis and for probabilistic model checking, and Safra's construction is notoriously hard to implement correctly. S2S is decidable and non-elementary, so the decidability results it delivers are theoretical rather than usable directly. And the correspondence is for ω-regular properties: anything needing counting or arithmetic falls outside, which is why real-time and probabilistic extensions need different machinery.

© 2026 Lingenic LLC