28/11/2002
Marcin Jurdzinski (Liafa)
Algorithms for solving parity games

The study of the computational complexity of parity games has two main motivations. One is its polynomial time equivalence to the model checking problem for the modal mu-calculus, the other its intriguing status from the point of view of structural complexity theory. While it is known to be in NP and co-NP and hence very unlikely to be NP-complete, no polynomial time algorithm has been found despite substantial effort of the automata- and complexity-theoretic and verification communities. After early results on the model checking problem for the modal mu-calculus, the game theoretic formulation yielded several complexity improvements and novel approaches in the last few years.

A few recent algorithms for solving parity games are surveyed. First we present a very simple algorithm with the best provable running time and space tradeoff known so far, based on computation of certain local witnesses for winning strategies. Then we sketch a strategy improvement algorithm due to Voege and J., inspired by an old algorithm for stochastic games by Hoffman and Karp. It is an intriguing long-standing open problem whether this algorithm terminates in polynomial time. Finally, we discuss a randomized subexponential algorithm due to Bjorklund, Petersson, Sandberg, and Vorobyov. Time permitting, we will mention a recent technique to speed-up a value iteration algorithm for simple stochastic games due to Somla. The relation of parity games to mean-payoff and simple stochastic games will also be mentioned.