High-level Message Sequence Charts are a well-established formalism to specify scenarios of communications in telecommunication protocols. In order to deal with possibly unbounded specifications, we focus on star-connected HMSCs. We relate this subclass with recog-nizability and MSO-definability by means of a new connection with Mazurkiewicz traces. Our main result is that we can check effectively whether a star-connected HMSC is realizable by a finite system of communicating automata with possibly unbounded channels.
CITATION STYLE
Morin, R. (2002). Recognizable sets of message sequence charts. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2285, pp. 523–534). Springer Verlag. https://doi.org/10.1007/3-540-45841-7_43
Mendeley helps you to discover research relevant for your work.