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.
Type de document :
Communication dans un congrès
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
Contributeur : Benedikt Bollig <>
Soumis le : mardi 15 janvier 2013 - 17:34:54
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Lien texte intégral

openaccess

Identifiants

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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

211

Contact


archive-ouverte@inria.fr