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

https://hal.inria.fr/hal-00879353
Contributor : Loic Helouet <>
Submitted on : Saturday, November 2, 2013 - 9:41:47 PM
Last modification on : Monday, February 15, 2021 - 10:48:04 AM
Long-term archiving on: : Monday, February 3, 2014 - 4:26:45 AM

File

lata2013.pdf
Files produced by the author(s)

Identifiers

  • 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. LATA 2013, Apr 2013, bilbao, Spain. pp.177-189. ⟨hal-00879353⟩

Share

Metrics

Record views

1001

Files downloads

612