Regular Set of Representatives for Time-Constrained MSC Graphs - Université de Rennes Accéder directement au contenu
Article Dans Une Revue Information Processing Letters Année : 2012

Regular Set of Representatives for Time-Constrained MSC Graphs

Résumé

Systems involving both time and concurrency are notoriously di fficult to analyze. Existing decidability results apply when clocks on di fferent processes cannot be compared or when 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) introduced in [1], and study if the set of timed executions generated by a TC-MSC graph is empty. This emptiness problem is known to be undecidable in general [9]. Our approach consists of finding a regular set R of representative timed executions, i.e., such that every timed execution of the system has an equivalent, up to commutation, timed execution in R. This allows us to solve the emptiness problem under the assumption that the TC-MSC graph is prohibited from (1) forcing any basic scenario to take an arbitrarily long time to complete and (2) enforcing unboundedly many events to occur within one unit of time.
Fichier principal
Vignette du fichier
AGHY11.pdf (195.01 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00879825 , version 1 (05-11-2013)

Identifiants

  • HAL Id : hal-00879825 , version 1

Citer

Sundararaman Akshay, Blaise Genest, Loïc Hélouët, Shaofa Yang. Regular Set of Representatives for Time-Constrained MSC Graphs. Information Processing Letters, 2012, 112 (14-15), pp.592-598. ⟨hal-00879825⟩
268 Consultations
112 Téléchargements

Partager

Gmail Facebook X LinkedIn More