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.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...