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
Résumé : Il est notoirement difficile d'analyser les comportements de systémes décrits par des modèles qui comportent à la fois du temps et de la concurrence. Des résultats de décidabilité existent pour des modèles dans lesquels les valeurs des horloges sur différents processus ne peuvent pas être comparées, ou lorsque les modèles ont des ensembles d'exécutions temporisés réguliers. Dans ce travail, nous montrons de nouveaux résultats de décidabilité pour des modèles temporisés et concurrents, qui ne s'appuient sur aucune de ces restrictions. Nous étudions le formalisme des time-constrained MSC graphs (TC-MSC graphs), initalement proposés, et le problème qui consiste à savoir si l'ensemble des exécutions temporisées d'un modèle est vide ou non. Ce problème a été prouvé indécidable en général pour les TC-MSC graphs. Notre approche pour obtenir une procédure de décision comporte deux étapes : (i) trouver un sous-ensemble R d'exécutions temporisées appelé ensemble des représentants : pour toute exécution temporisée du système, on doit pouvoir trouver une exécution équivalente dans R modulo commutation, (ii) prouver que R est régulier. L'existence d'un ensemble de représentants régulier permet de résoudre le problème de la vacuité de l'ensemble des exécutions d'un TC-MSC graph. Nous proposons une restriction aux TC-MSC graphs, que nous appelons TC-MSC Graph bien formés. Dans un TC-MSC graph bien formé, on ne peut forcer le système à exécuter un nombre arbitrairement grand d'événements en un laps de temps fini. Il est également interdit qu'un MSC prenne obligatoirement un temps arbitrairement long pour être entièrement exécuté. Les restrictions imposées aux TC-MSC graph bien formés réduisent peu la puissance d'expression du langage, et permettent de garantir l'existence d'un ensemble régulier de représentants.
Type de document :
Rapport
[Research Report] RR-7823, INRIA. 2011, 15 p
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-00647720
Contributeur : Akshay Sundararaman <>
Soumis le : mardi 6 décembre 2011 - 15:38:53
Dernière modification le : mercredi 16 mai 2018 - 11:23:02
Document(s) archivé(s) le : lundi 5 décembre 2016 - 04:02:32

Fichier

RR-7823.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

289

Téléchargements de fichiers

95