Polynomial-time parity-game solving

Two players move a token along arrows in a finite diagram, forever. Each location belongs to a player who chooses the next arrow, and carries a nonnegative whole-number priority. Ignore priorities seen only finitely often: the largest priority that recurs forever decides the winner, with even numbers favoring Even and odd numbers favoring Odd. A play that sees 7 once and then alternates between 2 and 4 forever is won by Even. The question is whether a fixed algorithm can find which player can force a win in every such game, using time bounded by a fixed power of the written game size.[1]

Can the winner of every explicitly given finite parity game be decided in polynomial time? A vertex’s owner chooses an outgoing edge, and no vertex is a dead end. Priorities are binary-encoded nonnegative integers. Even wins precisely when the largest priority recurring infinitely often is even; priorities appearing only in a finite prefix do not count. In the illustrative game, an Even-owned priority-7 start leads either to a forced 2–4 cycle or a forced 2–3 cycle. The first has recurring maximum 4 and the second 3, so the winning choice is the first. A strategy prescribes choices against every possible continuation by the other player. Such games admit winning strategies whose choices depend only on the current vertex. If N is the total encoded input length, the target is a bound $CN^k$ for fixed C and k. Quasipolynomial bounds can instead have an exponent growing like a fixed power of $\log N$; the proved bound does not imply the sought fixed-power bound.[1]

A general algorithm gives a time bound whose power increases slowly with game size instead of staying fixed. Such a bound is called quasipolynomial time. The open target is one fixed power for all games.[1] [2]

Winning strategies for either player can serve as certificates that are checked in polynomial time; this is the containment called $\mathrm{NP}\cap\mathrm{coNP}$. Efficiently checking a supplied certificate does not supply an efficient procedure for finding the winner. Quasipolynomial solvability likewise does not establish polynomial-time solvability.[1] [2]

A continuing system must sometimes keep meeting requirements, such as responding whenever requests keep arriving. Watching a finite number of steps cannot establish that behavior forever. These games turn recurring conditions and opposing choices into a finite mathematical input, so solving them helps determine whether a strategy can enforce a continuing requirement.[1]

The infinite-play rule compresses recurring behavior into a finite strategic problem. A controller may need to keep meeting a requirement despite an environment that chooses its own actions. Solving the corresponding game decides whether the modeled controller has a strategy that enforces the requirement, rather than merely one favorable execution. This is the connection to logic and synthesis. Polynomial-time solving would improve that finite decision step; it would not remove specification-to-game translation costs or make every problem with efficiently checkable certificates on both sides easy.[1]