A Discrete Strategy Improvement Algorithm for Solving Parity Games
Jens Vöge, Marcin Jurdzinski
A discrete strategy improvement algorithm is given for
constructing winning strategies in parity games, thereby
providing also a new solution of the model-checking problem
for the modal $\mu$-calculus. Known strategy improvement
algorithms, as proposed for stochastic games by Hoffman
and Karp in 1966 and for discounted payoff games and parity
games by Puri in 1995, work with real numbers and require
the solution of linear programming instances involving
high precision arithmetic. In the present algorithm these
difficulties are avoided, by means of a discrete vertex
valuation in which information about the relevance of vertices
and certain distances is coded. Another advantage of the
present approach is that it provides a better conceptual
understanding and easier analysis of strategy improvement
algorithms for parity games. However, so far we could not
settle the question whether the present algorithm works in
polynomial time; thus the long standing problem whether parity
games can be solved in polynomial time remains open.
We also provide some evidence for superiority of the strategy
improvement algorithm over other known algorithms for parity
games. In particular, we have verified that the algorithm
needs only linear number of strategy improvement steps on some
families of difficult examples, which make other algorithms
work in exponential time.