Solving Mean Payoff Parity Games With Strategy Improvement

Two player games played on finite graphs have attracted much interest in the formal methods com-munity. It has been shown that the problem of model checking the modal µ-calculus is equivalent to the problem of solving a two player parity game [2]. In these games, each vertex is assigned an inte-ger priority and the two players attempt to ensure that the minimum priority occurring infinitely of-ten is either odd or even. Much effort has been expended in an attempt to find an algorithm which solves parity games in polynomial time. However, no such algorithm has been found. One approach that has attracted much attention is strategy im-provement [4]. Strategy improvement algorithms terminate in polynomial time for all known inpu