TY - GEN

T1 - A robust class of context-sensitive languages

AU - La Torre, Salvatore

AU - Madhusudan, P.

AU - Parlato, Gennaro

PY - 2007

Y1 - 2007

N2 - 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 non-context free behaviors, and has applications in analyzing abstractions of multithreaded recursive programs, significantly 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.

AB - 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 non-context free behaviors, and has applications in analyzing abstractions of multithreaded recursive programs, significantly 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.

UR - http://www.scopus.com/inward/record.url?scp=82755165825&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=82755165825&partnerID=8YFLogxK

U2 - 10.1109/LICS.2007.9

DO - 10.1109/LICS.2007.9

M3 - Conference contribution

AN - SCOPUS:82755165825

SN - 0769529089

SN - 9780769529080

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 161

EP - 170

BT - Proceedings - 22nd Annual IEEE Symposiumon Logic in Computer Science, LICS 2007

T2 - 22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007

Y2 - 10 July 2007 through 14 July 2007

ER -