Asynchronous Control-State Choreographies
Klaus-Dieter Schewe, Yamine Ait-Ameur, Sarah Benyagoub

TL;DR
This paper extends the concept of choreographies to control-state choreographies, enabling parallelism, and provides necessary and sufficient conditions for their realisability in asynchronous communication systems.
Contribution
It generalizes choreographies to control-state models, establishing equivalence with rendez-vous compositions and characterizing realisability with new conditions.
Findings
Control-state choreographies enable parallelism in communication protocols.
Necessary conditions for realisability include sequence and choice conditions.
These conditions are also sufficient for realisability.
Abstract
Choreographies prescribe the rendez-vous synchronisation of messages in a system of communicating finite state machines. Such a system is called realisable, if the traces of the prescribed communication coincide with those of the asynchronous system of peers, where the communication channels either use FIFO queues or multiset mailboxes. In a recent article realisability was characterised by two necessary conditions that together are sufficient. A simple consequence is that realisability in the presence of a choreography becomes decidable. In this article we extend this work by generalising choreographies to control-state choreographies, which enable parallelism. We redefine P2P systems on grounds of control-state machines and show that a control-state choreography is equivalent to the rendez-vous compositions of its peers and that language-synchronisability coincides with…
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 · Access Control and Trust · Peer-to-Peer Network Technologies
