Reachability and boundedness in time-constrained MSC graphs - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Chapitre D'ouvrage Année : 2009

Reachability and boundedness in time-constrained MSC graphs

Résumé

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.

Domaines

Autre [cs.OH]
Fichier non déposé

Dates et versions

hal-00772665 , version 1 (10-01-2013)

Identifiants

  • HAL Id : hal-00772665 , version 1

Citer

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⟩
61 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More