Publication details

Controllable-choice Message Sequence Graphs


CHMELÍK Martin ŘEHÁK Vojtěch

Year of publication 2013
Type Article in Proceedings
Conference Proceedings of Mathematical and Engineering Methods in Computer Science, 8th Doctoral Workshop (MEMICS 2012), Selected Papers
MU Faculty or unit

Faculty of Informatics

Field Informatics
Keywords message sequence charts; realizability; local choice
Attached files
Description We focus on the realizability problem of Message Sequence Graphs (MSG), i.e. the problem whether a given MSG specification is correctly distributable among parallel components communicating via messages. This fundamental problem of MSG is known to be undecidable. We introduce a well motivated restricted class of MSG, so called controllable-choice MSG, and show that all its models are realizable and moreover it is decidable whether a given MSG model is a member of this class. In more detail, this class of MSG specifications admits a deadlock-free realization by overloading existing messages with additional bounded control data. We also show that the presented class is the largest known subclass of MSG that allows for deadlock-free realization.
Related projects: