On Regular Message Sequence Chart Languages and Relationships to Mazurkiewicz Trace Theory

Hierarchical Message Sequence Charts are a well-established formalism to specify telecommunication protocols. In this model, numerous undecidability results were obtained recently through algebraic approaches or relationships to Mazurkiewicz trace theory. We show how to check whether a rational language of MSCs requires only channels of finite capacity. In that case, we also provide an upper bound for the size of the channels. This enables us to prove our main result: one can decide whether the iteration of a given regular language of MSCs is regular if, and only if, the Star Problem in trace monoids (over some restricted independence alphabets) is decidable too. Message Sequence Charts (MSCs) are a popular model often used for the documentation of telecommunication protocols. They profit by a standartized visual and textual presentation (ITU-T recommendation Z.120 [20]) and are related to other formalisms such as sequence diagramms of UML [5] or message flow diagramms. An MSC gives...

• Type: Conference
• Year: 2001
• Where: FOSSACS
• Authors: Rémi Morin
• Keywords: FOSSACS 2001, Message Sequence Charts, MSCs, Software Engineering, Telecommunication Protocols