Regular Set of Representatives for Time-Constrained MSC Graphs

Sundararaman Akshay 1 Blaise Genest 1 Loïc Hélouët 1 Shaofa Yang 2
1 DISTRIBCOM - Distributed and Iterative Algorithms for the Management of Telecommunications Systems
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Systems involving both time and concurrency are notoriously difficult to analyze. Existing decidability results apply in settings where clocks on different processes cannot be compared or where the set of timed executions is regular. We prove new decidability results for timed concurrent systems, requiring neither restriction. We consider the formalism of time-constrained MSC graphs (TC-MSC graphs for short), and study whether the set of timed executions generated by a TC-MSC graph is empty or not. This emptiness problem is known to be undecidable in general. Our approach for obtaining decidability consists of two steps: (i) find a subset R of representative timed executions, that is, for which every timed execution of the system has an equivalent, up to commutation, timed execution in R, and (ii) prove that R is regular. This allows us to solve the emptiness problem under the assumption that the TC-MSC graph G is well-formed. In particular, a well-formed TC-MSC graph is prohibited from forcing any basic scenario to take an arbitrarily long time to complete. Secondly, it is forbidden from enforcing unboundedly many events to occur within a single unit of time. We argue that these restrictions are indeed practically sensible.
Liste complète des métadonnées

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-00647720
Contributor : Akshay Sundararaman <>
Submitted on : Tuesday, December 6, 2011 - 3:38:53 PM
Last modification on : Friday, November 16, 2018 - 1:24:46 AM
Document(s) archivé(s) le : Monday, December 5, 2016 - 4:02:32 AM

File

RR-7823.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00647720, version 1

Citation

Sundararaman Akshay, Blaise Genest, Loïc Hélouët, Shaofa Yang. Regular Set of Representatives for Time-Constrained MSC Graphs. [Research Report] RR-7823, INRIA. 2011, 15 p. ⟨hal-00647720⟩

Share

Metrics

Record views

301

Files downloads

113