We define a new class of languages defined by multi-stack automata that forms a robust subclass of context-sensitive languages, with decidable emptiness and closure under boolean operations. This class, called multi-stack visibly pushdown languages (MVPLs), is defined using multi-stack pushdown automata with two restrictions: (a) the pushdown automaton is visible, i.e. the input letter determines the operation on the stacks, and (b) any computation of the machine can be split into k stages, where in each stage, there is at most one stack that is popped. MVPLs are an extension of visibly pushdown languages that captures noncontext free behaviors, and has applications in analyzing abstractions of multithreaded recursive programs, signifi- cantly enlarging the search space that can be explored for them. We show that MVPLs are closed under boolean operations, and problems such as emptiness and inclusion are decidable. We characterize MVPLs using monadic second-order logic over appropriate structures, and exhibit a Parikh theorem for them.

A Robust Class of Context-Sensitive Languages

LA TORRE, Salvatore;PARLATO, GENNARO
2007

Abstract

We define a new class of languages defined by multi-stack automata that forms a robust subclass of context-sensitive languages, with decidable emptiness and closure under boolean operations. This class, called multi-stack visibly pushdown languages (MVPLs), is defined using multi-stack pushdown automata with two restrictions: (a) the pushdown automaton is visible, i.e. the input letter determines the operation on the stacks, and (b) any computation of the machine can be split into k stages, where in each stage, there is at most one stack that is popped. MVPLs are an extension of visibly pushdown languages that captures noncontext free behaviors, and has applications in analyzing abstractions of multithreaded recursive programs, signifi- cantly enlarging the search space that can be explored for them. We show that MVPLs are closed under boolean operations, and problems such as emptiness and inclusion are decidable. We characterize MVPLs using monadic second-order logic over appropriate structures, and exhibit a Parikh theorem for them.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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: http://hdl.handle.net/11386/3125677
 Attenzione

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

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 112
  • ???jsp.display-item.citation.isi??? 72
social impact