Skip to Main content Skip to Navigation
Conference papers

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], Inria Saclay - Ile de France
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.
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Loic Helouet Connect in order to contact the contributor
Submitted on : Saturday, November 2, 2013 - 9:41:47 PM
Last modification on : Wednesday, February 2, 2022 - 3:50:48 PM
Long-term archiving on: : Monday, February 3, 2014 - 4:26:45 AM


Files produced by the author(s)


  • HAL Id : hal-00879353, version 1


Benedikt Bollig, Aiswarya Cyriac, Loic Helouet, Ahmet Kara, Thomas Schwentick. Dynamic Communicating Automata and Branching High-Level MSCs. LATA 2013, Apr 2013, bilbao, Spain. pp.177-189. ⟨hal-00879353⟩



Record views


Files downloads