Parity automaton

A parity automaton is an automaton on infinite words that accepts a run based on the parity (even or odd) of the highest priority state visited infinitely often. Each state is assigned a natural number priority, and the run is accepting if the maximum priority seen infinitely often is even. This acceptance condition, introduced in the context of infinite games and modal μ-calculus model checking, has become the lingua franca of automata-theoretic verification because it combines expressive power with algorithmic tractability.\n\nParity automata are expressively equivalent to Büchi, Rabin, and Streett automata: every language recognized by any of these models can be recognized by a parity automaton, and vice versa. But parity automata offer a decisive algorithmic advantage: the nondeterministic and alternating variants can be determined with a single exponential blowup (tight), and the emptiness and universality problems admit efficient solutions using parity game algorithms. This has made parity the default acceptance condition in modern verification tools, despite the fact that specifications are rarely written in parity form directly.\n\nThe parity condition also dominates the theory of infinite games on graphs, where determinacy — the theorem that every parity game is determined (one player has a winning strategy) — is the engine beneath the algorithmic solution of LTL synthesis and controller synthesis problems. The proof of parity determinacy, due to Emerson, Jutla, and Sistla, is one of the cornerstones of automated verification.\n\nParity automata are the compromise that won. They are not the most natural specification formalism, nor the most intuitive acceptance condition. They are the sweet spot where expressiveness, determinizability, and game-solving efficiency converge. The history of automata on infinite words is a history of this convergence: theoretical convenience eventually becomes practical standard, and parity is the clearest example.\n\n\n