Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Akshay Sundararaman Connect in order to contact the contributor
Submitted on : Tuesday, December 6, 2011 - 3:38:53 PM
Last modification on : Thursday, October 27, 2022 - 3:44:43 AM
Long-term archiving on: : Monday, December 5, 2016 - 4:02:32 AM


Files produced by the author(s)


  • HAL Id : hal-00647720, version 1


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⟩



Record views


Files downloads