Uniform Solution of Parity Games on Prefix-Recognizable Graphs

Thierry Cachat


Abstract

Walukiewicz 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.