MSO Decidability of Multi-Pushdown Systems via Split-Width

Aiswarya Cyriac 1, 2 Paul Gastin 1, 2 K. Narayan Kumar 3
1 LSV - Laboratoire Spécification et Vérification [Cachan]
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
3 Chennai Mathematical Institute [Inde]
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.
Document type :
Conference papers
Koutny, Maciej and Ulidowski, Irek. Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR'12), 2012, Newcastle, United Kingdom. Springer, 7454, pp.547-561, 2012, 〈10.1007/978-3-642-32940-1_38〉
Liste complète des métadonnées
https://hal.inria.fr/hal-00776596
Contributor : Benedikt Bollig <>
Submitted on : Tuesday, January 15, 2013 - 5:34:54 PM
Last modification on : Thursday, January 11, 2018 - 6:23:37 AM

Links full text

openaccess

Identifiers

Collections

INRIA | ENS-CACHAN

Citation

Aiswarya Cyriac, Paul Gastin, K. Narayan Kumar. MSO Decidability of Multi-Pushdown Systems via Split-Width. Koutny, Maciej and Ulidowski, Irek. Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR'12), 2012, Newcastle, United Kingdom. Springer, 7454, pp.547-561, 2012, 〈10.1007/978-3-642-32940-1_38〉. 〈hal-00776596〉

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

206

Contact


archive-ouverte@inria.fr