Solving Mean Payo Parity Games With Strategy Improvement
John Fearnley · 2008
Two player games played on finite graphs have attracted much interest in the formal methods community. 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 integer priority and the two players attempt to ensure that the minimum priority occurring infinitely often 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 improvement [4]. Strategy improvement algorithms terminate in polynomial time for all known input instances. However, no one has yet been able to prove that they terminate in polynomial time for all parity games.