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
V₀, V₁	—	Vertices	Player partitions
p	—	Priority	Parity function
Inf	—	Infinitely often	Recurring set
σ	U+03C3	Strategy	Move function

Metatheory. Positional determinacy. Quasipolynomial solvability. Fixed-point characterization. Zielonka's algorithm. Reduction from L_μ.

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

Limitations. Polynomial still open. Large games in practice. Priority representation. Extensions complex (e.g., imperfect information).