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
Contributor : Stefan Haar Connect in order to contact the contributor
Submitted on : Thursday, January 10, 2013 - 10:40:28 PM
Last modification on : Thursday, January 20, 2022 - 4:13:06 PM


  • HAL Id : hal-00772665, version 1


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⟩



Record views