Symbolic strategy synthesis for games on pushdown graphs

Abstract

We consider infinite two-player games on pushdown graphs, the reachability game where the first player must reach a given set of vertices to win, and the Büchi game where he must reach this set infinitely often. We provide an automata theoretic approach to compute uniformly the winning region of a player and corresponding winning strategies, if the goal set is regular. Two kinds of strategies are computed: positional ones which however require linear execution time in each step, and strategies with pushdown memory where a step can be executed in constant time. © 2002 Springer-Verlag Berlin Heidelberg.