Abstract
The paper presents ongoing work aiming at understanding the nature of specifications given by High Level Message Sequence Charts and the ways in which they can be put into effective use. Contrarily to some authors, we do not set finite state restrictions on HMSCs as we feel such restrictions do not fit in with the type of distributed systems encountered today in the field of telecommunications. The talk presents first a series of undecidability results about general HMSCs following from corresponding undecidability results on rational sets in product monoids. These negative results which with one exception do not appear yet in the literature on HMSCs do indicate that the sole way in which general HMSCs may be usefully handed as behavioural specifications is to interpret their linear extensions as minimal languages, to be approximated from above in any realization. The problem is then to investigate frameworks in which these incomplete specifications may be given a meaning by a closure operation. The second part of the paper presents a closure operation relative to Petri net languages. This closure operation is an effective procedure that relies on semilinear properties of HMSCs languages. We finally present some decidability results for the distribution and verification of HMSCs transformed into Petri nets.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Yannakakis, M.: Model Checking of Message Sequence Charts. Proc. Concur, LNCS 1664 (1999) 114–129
Badouel, E., Caillaud, B., Darondeau, Ph.: Distributing Finite Automata through Petri Net Synthesis. (draft available from the authors)
Berstel, J.: Transductions and Context-Free Languages. Teubner Studienbücher, Stuttgart (1979)
Caillaud, B.: Bounded Petri Net Synthesis Techniques and their Applications to the Distribution of Reactive Automata. JESA 9-10 no.33 (1999) 925–942
Damm, W., Harel, D.: LCSs: Breathing Life into Message Sequence Charts. Report CS98/09, Weizmann Institute of Technology (1998)
Darondeau, Ph.: Deriving Unbounded Petri Nets from Formal Languages. Proc. Concur, LNCS 1466 (1998) 533–548
Darondeau, Ph.: Region Based Synthesis of P/T-Nets and its Potential Applications. Proc. ICATPN, LNCS 1825 (2000) 16–23
Diekert, V., Métivier, Y.: Partial Commutation and Traces. Research report 1996/02, Universität Stuttgart Fakultät Informatik (1996)
Diekert, V., Rozenberg, G. (editors): The Book of Traces. World Scientific, Singapore (1995)
Eilenberg, S., Schützenberger, M.: Rational Sets in Commutative Monoids. Journal of Algebra 13 (1969) 173–191
Esparza, J.: On the Decidability of Model-checking for several mu-calculi and Petri Nets. Proc. Caap, LNCS 787 (1994) 115–129
Fischer, P.C., Rosenberg, A.L.: Multitape One-Way Nonwriting Automata. JCSS 2 (1968) 88–101
Harel, D., Kugler, H.: Synthesizing State-Based Object Systems from LSC Specifications. Report MCS99/20, Weizmann Institute of Technology (1999)
Henriksen, J.G., Mukund, M., Narayan Kumar, K., Thiagarajan, P.S.: On Message Sequence Graphs and Finitely Generated Regular MSC Languages. Proc. Icalp, LNCS 1853 (2000) 675–686
Henriksen, J.G., Mukund, M., Narayan Kumar, K., Thiagarajan, P.S.: Regular Collections of Message Sequence Charts. Proc. MFCS, LNCS 1893 (2000) 405–414
TU-TS Recommendation Z.120: Message Sequence Chart 1996 (MSC96). Technical Report, ITU-TS, Geneva (1996)
Jancar, P., Moeller, F.: Checking Regular Properties of Petri Nets, Proc. Concur, LNCS 962 (1995) 348–362
Mauw, S., Reniers, M.A., High-Level Message Sequence Charts. Proc. Eighth SDL Forum, Elsevier Science Publishers B.V. (1997) 291–306
Mayr, E.: An Algorithm for the General Petri Net Reachability Problem. SIAM Journal on Computing 13 (1984) 441–460
Mukund, M., Narayan Kumar, K., Sohoni, M.: Synthesizing distributed finite-state systems from MSCs. Proc. Concur, LNCS 1877 (2000) 521–535
Muscholl, A., Peled, D., Su, Z.: Deciding Properties for Message Sequence Charts. Proc. Fossacs, LNCS 1378 (1998) 226–242
Pelz, E.: Closure Properties of Deterministic Petri Nets. Proc. Stacs, LNCS 247 (1987) 373–382
Peterson, J.L.: Computation Sequence Sets. JCSS 13 (1976) 1–24
van Glabbeek, R.J., Weijland, W.P.: Branching Time and Abstraction in Bisimulation Semantics. Proc. IFIP Congress, North Holland / IFIP (1989) 613–618
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Caillaud, B., Darondeau, P., Hélouët, L., Lesventes, G. (2001). HMSCs as Partial Specifications...with PNs as Completions. In: Cassez, F., Jard, C., Rozoy, B., Ryan, M.D. (eds) Modeling and Verification of Parallel Processes. MOVEP 2000. Lecture Notes in Computer Science, vol 2067. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45510-8_5
Download citation
DOI: https://doi.org/10.1007/3-540-45510-8_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42787-2
Online ISBN: 978-3-540-45510-3
eBook Packages: Springer Book Archive