论文标题
异步控制状态编舞
Asynchronous Control-State Choreographies
论文作者
论文摘要
编舞在通信有限状态机的系统中规定消息的Rendez-Vous同步。如果规定的通信的痕迹与同步的同行系统相吻合，则这种系统称为可实现，如果通信渠道使用FIFO队列或多发邮箱。在最近的文章中，可实现的特征是两个必要条件在一起就足够了。一个简单的结果是，在编舞的存在下，可实现的性能是可以决定的。在本文中，我们通过将编排概括为控制状态编排，扩展了这项工作，这使得可以并行。我们以控制状态机器为由重新定义P2P系统，并表明控制状态编排等同于其同龄人的列德兹空分组成，并且语言同步性与同步性相吻合。这些结果用于表征控制状态编排的可变性。至于基于FSM的编排，我们证明了两个必要的条件：序列条件和选择条件。然后，我们还表明，这两个条件在一起就足以实现控制状态编舞的真实性。
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.
