Uniform Solution of Parity Games on Prefix-Recognizable Graphs

AbstractWalukiewicz gave in 1996 a solution for parity games on pushdown graphs: he proved the existence of pushdown strategies and determined the winner with an EXPTIME procedure. We give a new presentation and a new algorithmic proof of these results, obtain a uniform solution for parity games (independent of their initial configuration), and extend the results to prefix-recognizable graphs. The winning regions of the players are proved to be effectively regular, and winning strategies are computed