Controllable-choice Message Sequence Graphs
Martin Chmel\'ik, Vojt\v{e}ch \v{R}eh\'ak

TL;DR
This paper introduces controllable-choice Message Sequence Graphs, a restricted class ensuring realizability and deadlock-free execution, addressing the undecidable general case of MSG realizability.
Contribution
It defines a new subclass of MSG, controllable-choice MSG, that guarantees realizability and deadlock-freedom, and proves its maximality among known subclasses.
Findings
All models of controllable-choice MSG are realizable.
Decidability of membership in the controllable-choice class.
Largest known subclass of MSG with deadlock-free realization.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDistributed systems and fault tolerance · Formal Methods in Verification · Embedded Systems Design Techniques
