Symbolically Bounding the Drift in Time-Constrained MSC-Graphs

Abstract : Verifying systems involving both time and concurrency rapidly leads to undecidability, and requires restrictions to become eff ective. This paper addresses the emptiness problem for time-constrained MSC-Graphs (TC-MSC graphs for short), that is, checking whether there is a timed execution compatible with a TC-MSC graph speci cation. This problem is known to be undecidable in general [11], and decidable for some regular speci cations [11]. We establish decidability of the emptiness problem under the condition that, for a given K, no path of the TC-MSC graph forces any node to take more than K time units to complete. We prove that this condition can be e ffectively checked. The proofs use a novel symbolic representation for runs, where time constraints are encoded as a system of inequalities. This allows us to handle non-regular speci cations and improve effi ciency w.r.t. using interleaved representations.
Type de document :
Communication dans un congrès
Abhik Roychoudhury and Meenakshi D'Souza. International Colloquium on Theoretical Aspects of Computing, Sep 2012, Bangalore, India. Springer, 7521, pp.1-15, 2012, LNCS
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00879831
Contributeur : Loic Helouet <>
Soumis le : mardi 5 novembre 2013 - 12:10:34
Dernière modification le : mercredi 16 mai 2018 - 11:24:06
Document(s) archivé(s) le : jeudi 6 février 2014 - 04:34:42

Fichier

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

Identifiants

  • HAL Id : hal-00879831, version 1

Citation

Sundararaman Akshay, Blaise Genest, Loic Helouet, Shaofa Yang. Symbolically Bounding the Drift in Time-Constrained MSC-Graphs. Abhik Roychoudhury and Meenakshi D'Souza. International Colloquium on Theoretical Aspects of Computing, Sep 2012, Bangalore, India. Springer, 7521, pp.1-15, 2012, LNCS. 〈hal-00879831〉

Partager

Métriques

Consultations de la notice

484

Téléchargements de fichiers

74