Asynchronous Control-State Choreographies

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 synchronisability. These results are used to characterise realisability of control-state choreographies. As for the case of FSM-based choreographies we prove two necessary conditions: a sequence condition and a choice condition. Then we also show that these two conditions together are sufficient for the realisability of control-state choreographies.