Skip to Main content Skip to Navigation
Book sections

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], Inria Saclay - Ile de France
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.
Document type :
Book sections
Complete list of metadata
https://hal.inria.fr/hal-00772665
Contributor : Stefan Haar <>
Submitted on : Thursday, January 10, 2013 - 10:40:28 PM
Last modification on : Monday, February 15, 2021 - 10:49:07 AM

Identifiers

  • HAL Id : hal-00772665, version 1

Collections

CNRS | INRIA | ENS-CACHAN | ENS-PARIS-SACLAY

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

144

 

Contact                    Legal Notice                    Personal Data