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 B¨uchi condition and a new condition that we call unboundedness. 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.

• Type: Conference
• Year: 2003
• Where: FSTTCS
• Authors: Alexis-Julien Bouquet, Olivier Serre, Igor Walukiewicz
• Keywords: B¨uchi Condition, FSTTCS 2003, Pushdown Automaton, Two-player Perfect Information