In: LNCS 2067: Modeling and Verification of Parallel Processes, pages 125-pp. 4th Summer School, MOVEP 2000, Nantes, France, June 19-23, 2000. Revised Tutorial Lectures / F. Cassez, C. Jard, B. Rozoy, M. Dermot (Eds.) --- Springer Verlag, 2001.
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.
Back to the Petri Nets Bibliography