Visibly Pushdown Games

The class of visibly pushdown languages has been recently defined as a subclass of context-free languages with desirable closure properties and tractable decision problems. We study visibly pushdown games, which are games played on visibly pushdown systems where the winning condition is given by a visibly pushdown language. We establish that, unlike pushdown games with pushdown winning conditions, visibly pushdown games are decidable and are 2Exptime-complete. We also show that pushdown games against Ltl specifications and Caret specifications are 3Exptime-complete. Finally, we establish the topological complexity of visibly pushdown languages by showing that they are a subclass of Boolean combinations of Σ3 sets. This leads to an alternative proof that visibly pushdown automata are not determinizable and also shows that visibly pushdown games are determined.

• Type: Conference
• Year: 2004
• Where: FSTTCS
• Authors: Christof Löding, P. Madhusudan, Olivier Serre
• Keywords: FSTTCS 2004, Pushdown, Pushdown Games, Visibly Pushdown Languages