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.