2-Visibly Pushdown Automata

Visibly Pushdown Automata (VPA) are a special case of pushdown machines where the stack operations are driven by the input. In this paper, we consider VPA with two stacks, namely 2-VPA. These automata introduce a useful model to effectively describe concurrent pushdown systems using a simple communication mechanism between stacks. We show that 2-VPA are strictly more expressive than VPA. Indeed, 2-VPA accept some context-sensitive languages that are not context-free and some context-free languages that are not accepted by any VPA. Nevertheless, the class of languages accepted by 2-VPA is closed under all boolean operations and determinizable in ExpTime, but does not preserve decidability of emptiness problem. By adding an ordering constraint on stacks (2-OVPA), decidability of emptiness can be recovered (preserving desirable closure properties) and solved in PTime. Using these properties along with the automata-theoretic approach, we prove that the model checking problem over 2-OVPA m...

• Type: Conference
• Year: 2007
• Where: DLT
• Authors: Dario Carotenuto, Aniello Murano, Adriano Peron
• Keywords: Concurrent Pushdown Systems, DLT 2007, Pushdown, Pushdown Automata, Theoretical Computer Science