Pushdown Games with Unboundedness and Regular Conditions

摘要

We consider infinitary two-player perfect information games defined over graphs of configurations of a pushdown automaton. We show how to solve such games when winning conditions are Boolean combinations of a Buechi condition and a new condition that we call unbound-edness. An infinite play satisfies the unboundedness condition if there is no bound on the size of the stack during the play. We show that the problem of deciding a winner in such games is EXPTIME-complete.