Parity Games

Origin. Emerson and Jutla (1991). Two-player infinite games on graphs. Parity condition on infinite plays. Decides μ-calculus satisfiability. Positional strategies suffice.

Models. Game graph with priorities. Players Even and Odd. Infinite play: highest priority seen infinitely often determines winner. Even wins if this priority is even.

Formalism.

Parity game: G = (V, V₀, V₁, E, p) where:

V = V₀ ⊎ V₁ (vertices partitioned by player)
E ⊆ V × V (edges)
p: V → {0, 1, ..., d} (priority function)

Play: π = v₀v₁v₂... infinite path. At vᵢ ∈ V₀: Even chooses next vertex. At vᵢ ∈ V₁: Odd chooses next vertex.

Winning condition: Inf(π) = priorities appearing infinitely often. Even wins iff max(Inf(π)) is even.

Strategy: σ: V* → V function choosing moves. Positional: σ: V → V depends only on current vertex.

Positional determinacy: Every parity game is determined. Winner has positional (memoryless) winning strategy.

Complexity: In NP ∩ co-NP. Quasipolynomial algorithms (2017). Polynomial: open problem.

μ-calculus connection: Model checking L_μ reduces to parity games. Alternation depth ↔ priority range.

Symbols.

Symbol	Unicode	Name	Meaning
G	—	Game	The tuple (V, V₀, V₁, E, p)
V	—	Vertex set	Positions of the game graph
V₀, V₁	—	Player partitions	Vertices owned by Even and by Odd
E	—	Edge relation	E ⊆ V × V, the available moves
p	—	Priority function	p : V → {0, …, d}
d	—	Priority bound	Largest priority; matches μ-calculus alternation depth
⊎	U+228E	Multiset union / Disjoint union	V = V₀ ⊎ V₁, the ownership partition
⊆	U+2286	Subset of or equal to	E ⊆ V × V
×	U+00D7	Multiplication sign / Cartesian product	Forms V × V
∈	U+2208	Element of	vᵢ ∈ V₀, whose turn it is
→	U+2192	Rightwards arrow / Function arrow	Domain and codomain of p and σ
π	U+03C0	Pi / Play	The infinite path v₀v₁v₂…
σ	U+03C3	Sigma / Strategy	V* → V, or V → V when positional
V*	—	Kleene star	Finite histories, the domain of a general strategy
Inf	—	Infinity set	Priorities occurring infinitely often along π
max	—	Maximum	Highest priority in Inf(π); its parity decides the winner
L_μ	—	Modal μ-calculus	Its model checking reduces to these games

Metatheory. The foundational result is positional determinacy: every vertex is winning for exactly one player, and the winner has a strategy depending only on the current vertex, not on the history. Emerson and Jutla (1991) and Mostowski proved it independently; it is a strengthening of Martin's Borel determinacy in the special case of the parity condition, and it is what makes the games finitely presentable and the μ-calculus decidable, since alternation depth corresponds exactly to the range of the priority function. Positionality also fixes the complexity: a positional strategy is a polynomial-size certificate checkable in polynomial time, so the problem lies in NP, and by symmetry of the parity condition under swapping players in co-NP as well — indeed in UP ∩ co-UP (Jurdziński 1998). Whether it is in P was open from 1991 until Calude, Jain, Khoussainov, Li, and Stephan (2017) gave a quasi-polynomial algorithm, n^O(log d); this is still not polynomial, and the question remains open. Zielonka's recursive algorithm remains competitive in practice despite an exponential worst case.

Applies to. Modal μ-calculus. Automata emptiness. LTL synthesis. Controller synthesis. Infinite games.

Limitations. No polynomial algorithm is known, and the problem's membership in UP ∩ co-UP is evidence that it is not NP-complete, so the usual hardness route to explaining the difficulty is unavailable — the quasi-polynomial bound n^O(log d) is superpolynomial whenever the number of priorities grows with the graph. Positional determinacy is fragile: it holds for the parity condition and fails for the natural generalizations, so Muller conditions need memory of size factorial in the number of priorities, and mean-payoff and energy conditions require separate arguments. The games are perfect-information and finite; with imperfect information the winning problem becomes ExpTime-complete and positional strategies no longer suffice, and concurrent moves destroy determinacy altogether, leaving only limit-values rather than winners. Reduction from μ-calculus model checking is exponential in the formula when the transition system is itself given symbolically, so the games solved in practice are constructed rather than given.