Attractors Is All You Need: Parity Games In Polynomial Time

TL;DR

The paper addresses the longstanding open problem of solving parity games in polynomial time and introduces a novel attractor-type operator $A(G, d)$ that guarantees inclusion of a dominion. By starting from $U_d(G)$ and iteratively refining via attractors, the method computes a $\bigcirc$-dominion and is applied at the maximal priorities for both players ($\hat{d}$ and $\overline{d}$) to peel off minimal dominions, repeating until the graph is exhausted. The authors prove that $A(G, d)$ yields a dominion and that the overall algorithm runs in $O(n^{2}\cdot(n+m))$ time, with at most $n$ iterations. This establishes the first full polynomial-time solver for general parity games and has immediate implications for related formalisms such as the modal $\mu$-calculus and parity-accepting automata, while also noting practical considerations and avenues for future optimization.

Abstract

This paper provides a polynomial-time algorithm for solving parity games that runs in $\mathcal{O}(n^{2}\cdot(n + m))$ time-ending a search that has taken decades. Unlike previous attractor-based algorithms, the presented algorithm only removes regions with a determined winner. The paper introduces a new type of attractor that can guarantee finding the minimal dominion of a parity game. The attractor runs in polynomial time and can peel the graph empty.

Figures (2)

• Figure 1: An example of a parity game.
• Figure 2: An overview of the memoryless strategy of $\Box$ for the parity game of \ref{['fig:parity-game-example']}.

Theorems & Definitions (16)

• Lemma 1: zielonka_infinite_1998
• Theorem 2
• proof
• Remark
• Lemma 3
• proof
• Lemma 4
• proof
• Theorem 5
• proof