Parity game

Parity game is a two-player infinite game played on a finite directed graph, where each vertex is labeled with a natural number priority. The existential player wins if the highest priority visited infinitely often is even; the universal player wins if it is odd. Parity games are the central algorithmic problem in model checking for modal mu-calculus: a formula is satisfied if and only if the existential player wins the associated parity game.

Despite decades of research, the exact complexity of solving parity games remains unknown. The problem is in NP and co-NP, and recent quasi-polynomial algorithms have narrowed the gap, but a polynomial-time algorithm remains elusive. This mysterious tractability makes parity games a test case for the broader question of whether the alternation between existential and universal choice can be resolved efficiently.