Reachability and boundedness in time-constrained MSC graphs

Paul Gastin 1 Madhavan Mukund K. Narayan Kumar
1 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : Channel boundedness is a necessary condition for a message-passing system to exhibit regular, finite-state behaviour at the global level. For Message Sequence Graphs (MSGs), the most basic form of High-level Message Sequence Charts (HMSCs), channel boundedness can be characterized in terms of structural conditions on the underlying graph. We consider MSGs enriched with timing constraints between events. These constraints restrict the global behaviour and can impose channel boundedness even when it is not guaranteed by the graph structure of the MSG. We show that we can use MSGs with timing constraints to simulate computations of a two-counter machine. As a consequence, even the more fundamental problem of reachability, which is trivial for untimed MSGs, becomes undecidable when we add timing constraints. Different forms of channel boundedness also then turn out to be undecidable, using reductions from the reachability problem.
Type de document :
Chapitre d'ouvrage
Lodaya, Kamal and Mukund, Madhavan and Ramanujam, R. Perspectives in Concurrency Theory, Universities Press, pp.157-183, 2009
Liste complète des métadonnées
https://hal.inria.fr/hal-00772665
Contributeur : Stefan Haar <>
Soumis le : jeudi 10 janvier 2013 - 22:40:28
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Identifiants

  • HAL Id : hal-00772665, version 1

Collections

INRIA | ENS-CACHAN

Citation

Paul Gastin, Madhavan Mukund, K. Narayan Kumar. Reachability and boundedness in time-constrained MSC graphs. Lodaya, Kamal and Mukund, Madhavan and Ramanujam, R. Perspectives in Concurrency Theory, Universities Press, pp.157-183, 2009. 〈hal-00772665〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

103

Contact


archive-ouverte@inria.fr