Steen Vester: Winning Cores in Parity Games

Whether parity games can be solved by a polynomial-time algorithm is a well-studied problem in theoretical computer science which has not yet been resolved. In this talk we propose a new direction for approaching this problem based on the novel notion of a winning core.

We give two different, but equivalent, definitions of a winning core and show a number of interesting properties about them. This includes showing that winning cores can be computed in polynomial time if and only if parity games can be solved in polynomial time implying that computation of winning cores is in the intersection of NP and coNP.

We also present a deterministic polynomial-time approximation algorithm for solving parity games based on computing winning cores. It runs in time \(O(d * n^2 * m)\) where d is the number of colors, n is the number of states and m is the number of transitions. The algorithm returns under-approximations of the winning regions in parity games. It works remarkably well in practice as it solves all benchmark games from the PGSolver framework in our experiments completely and outperforms existing algorithms in most cases in our experiments. In addition, correctness of the output of the algorithm can be checked efficiently.