Realisability of choreographies (Q2206787)

In this article the authors re-investigate the synchronisability problem for communication of finite state machines under the presence of a choreography that prescribes the rendez-vous synchronisation of the peers. Two necessary conditions on realisable choreographies are discovered and proved that these conditions together guarantee realisability. A consequence is decidability of realisability in the presence of a choreography. The authors claim that the new sufficient and necessary characterisation of realisability strengthens the theoretical underpinnings of this approach and removes unnecessary assumptions. For the entire collection see [Zbl 1435.68031].