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>1n>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.

Ordered multi-stack visibly pushdown automata

PERON, ADRIANO
2016-01-01

Abstract

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>1n>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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11368/3029523
 Avviso

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 6
social impact