12.00 noon
MSO Decidability of Multi-Pushdown Systems via Split-Width
Aiswarya Cyriac
LSV, ENS Cachan, France.
17-01-13

---

Abstract

Multi-threaded programs with recursion are naturally modeled as multi-pushdown systems. The behaviors are represented as multiply nested words (MNWs), which are words enriched with additional binary relations for each stack matching a push operation with the corresponding pop operation. Any MNW can be decomposed by two basic and natural operations: shuffle of two sequences of factors and merge of consecutive factors of a sequence. We say that the split-width of a MNW is *k* if it admits a decomposition where the number of factors in each sequence is at most *k*. The MSO theory of MNWs with split-width *k* is decidable. We introduce two very general classes of MNWs that strictly generalize known decidable classes and prove their MSO decidability via their split-width and obtain comparable or better bounds of tree-width of known classes.

This is a joint work with Paul Gastin and K. Narayan Kumar.