Regular Set of Representatives for Time-Constrained MSC Graphs

Abstract : 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.
Type de document :
Article dans une revue
Information Processing Letters, Elsevier, 2012, 112 (14-15), pp.592-598
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00879825
Contributeur : Loic Helouet <>
Soumis le : mardi 5 novembre 2013 - 12:17:11
Dernière modification le : mercredi 11 avril 2018 - 01:51:08
Document(s) archivé(s) le : jeudi 6 février 2014 - 04:34:41

Fichier

AGHY11.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00879825, version 1

Citation

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

Partager

Métriques

Consultations de la notice

617

Téléchargements de fichiers

154