conference paper published yes Martin Chmelik author 3624234E-F248-11E8-B48F-1D18A9856A87 Vojtěch Řehák author KrCh department MEMICS: Mathematical and Engineering Methods in Computer Science Modern Graph Algorithmic Techniques in Formal Verification project Game Theory project Quantitative Graph Games: Theory and Applications project Microsoft Research Faculty Fellowship project 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. Springer2013Znojmo, Czech Republic eng 1209.449910.1007/978-3-642-36046-6_12 7721118 - 130 Chmelik, Martin, and Vojtěch Řehák. <i>Controllable-Choice Message Sequence Graphs</i>. Vol. 7721, Springer, 2013, pp. 118–30, doi:<a href="https://doi.org/10.1007/978-3-642-36046-6_12">10.1007/978-3-642-36046-6_12</a>. Chmelik M, Řehák V. 2013. Controllable-choice message sequence graphs. 7721, 118–130. Chmelik, M., &#38; Řehák, V. (2013). Controllable-choice message sequence graphs. Presented at the MEMICS: Mathematical and Engineering Methods in Computer Science, Znojmo, Czech Republic: Springer. <a href="https://doi.org/10.1007/978-3-642-36046-6_12">https://doi.org/10.1007/978-3-642-36046-6_12</a> Chmelik, Martin, and Vojtěch Řehák. “Controllable-Choice Message Sequence Graphs.” Lecture Notes in Computer Science. Springer, 2013. <a href="https://doi.org/10.1007/978-3-642-36046-6_12">https://doi.org/10.1007/978-3-642-36046-6_12</a>. Chmelik M, Řehák V. Controllable-choice message sequence graphs. 2013;7721:118-130. doi:<a href="https://doi.org/10.1007/978-3-642-36046-6_12">10.1007/978-3-642-36046-6_12</a> M. Chmelik, V. Řehák, 7721 (2013) 118–130. M. Chmelik and V. Řehák, “Controllable-choice message sequence graphs,” vol. 7721. Springer, pp. 118–130, 2013. 28862018-12-11T12:00:09Z2025-06-11T08:05:09Z