Ordered multi-stack 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 multiple stacks, namely n-VPA, with n>1. These automata introduce a useful model to effectively describe concurrent pushdown systems using a simple communication mechanism between stacks. We show that n-VPA are strictly more expressive than VPA. Indeed, n-VPA accept some context-sensitive languages that are not context-free and some context-free languages that are not accepted by any VPA. Nevertheless, we show that the class of languages accepted by n-VPA is closed under union and intersection. On the contrary, this class turns out to be neither closed under complementation nor determinizable. Moreover, we show that the emptiness problem for n-VPA is undecidable. By adding an ordering constraint on stacks (n-OVPA), decidability of emptiness can be recovered, as well as the closure under complementation. Using these properties along with the automata-theoretic approach, one can prove that the model checking problem over n-OVPA models against n-OVPA specifications is decidable.