Higher order pushdown automata, the Caucal hierarchy of graphs and parity games

Abstract

We consider two-player parity games played on transition graphs of higher order pushdown automata. They are "game-equivalent" to a kind of model-checking game played on graphs of the infinite hierarchy introduced recently by Caucal. Then in this hierarchy we show how to reduce a game to a graph of lower level. This leads to an effective solution and a construction of the winning strategies. © Springer-Verlag Berlin Heidelberg 2003.