Small Progress Measures for Solving Parity Games

Abstract. In this paper we develop a new algorithm for deciding the winner in parity games, and hence also for the modal -calculus model checking. The design and analysis of the algorithm is based on a notion of game progress measures: they are witnesses for winning strategies in par-ity games. We characterize game progress measures as pre-xed points of certain monotone operators on a complete lattice. As a result we get the existence of the least game progress measures and a straightforward way to compute them. The worst-case running time of our algorithm matches the best worst-case running time bounds known so far for the problem, achieved by the algorithms due to Browne et al., and Seidl. Our algo-rithm has better space complexity: it works in small polynomial space; the other two algorithms have exponential worst-case space complexity.