Dynamic Communicating Automata and Branching High-Level MSCs

Benedikt Bollig 1 Aiswarya Cyriac 1, 2 Loic Helouet 3 Ahmet Kara 4 Thomas Schwentick 4
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 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We study dynamic communicating automata (DCA), an extension of classical communicating finite-state machines that allows for dynamic creation of processes. The behavior of a DCA can be described as a set of message sequence charts (MSCs). While DCA serve as a model of an implementation, we propose branching high-level MSCs (bHMSCs) on the speci fication side. Our focus is on the implementability problem: given a bHMSC, can one construct an equivalent DCA? As this problem is undecidable, we introduce the notion of executability, a decidable necessary criterion for implementability. We show that executability of bHMSCs is EXPTIME-complete. We then identify a class of bHMSCs for which executability eff ectively implies implementability.
Type de document :
Communication dans un congrès
Horia Dediu, Adrian and Martín-Vide, Carlos and Truthe, Bianca. LATA 2013, Apr 2013, bilbao, Spain. Springer, 7810, pp.177-189, 2013, LNCS
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00879353
Contributeur : Loic Helouet <>
Soumis le : samedi 2 novembre 2013 - 21:41:47
Dernière modification le : mardi 16 janvier 2018 - 15:54:22
Document(s) archivé(s) le : lundi 3 février 2014 - 04:26:45

Fichier

lata2013.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00879353, version 1

Citation

Benedikt Bollig, Aiswarya Cyriac, Loic Helouet, Ahmet Kara, Thomas Schwentick. Dynamic Communicating Automata and Branching High-Level MSCs. Horia Dediu, Adrian and Martín-Vide, Carlos and Truthe, Bianca. LATA 2013, Apr 2013, bilbao, Spain. Springer, 7810, pp.177-189, 2013, LNCS. 〈hal-00879353〉

Partager

Métriques

Consultations de la notice

467

Téléchargements de fichiers

367