Winning regions of pushdown parity games: A saturation method

Abstract. We present a new algorithm for computing the winning region of a par-ity game played over the configuration graph of a pushdown system. Our method gives the first extension of the saturation technique to the parity condition. Fi-nite word automata are used to represent sets of pushdown configurations. Start-ing from an initial automaton, we perform a series of automaton transformations to compute a fixed-point characterisation of the winning region. We introduce notions of under-approximation (soundness) and over-approximation (complete-ness) that apply to automaton transitions rather than runs, and obtain a clean proof of correctness. Our algorithm is simple and direct, and it permits an optimisation that avoids an immediate exponential blow up.