Asynchronous Control-State Choreographies

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.