Uniform Solution of Parity Games on Prefix-Recognizable Graphs

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.

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Thierry Cachat
• Keywords: ENTCS 2002, Parity Games, Pushdown, Pushdown Strategies