比较通信状态机、高级消息序列图和多方会话类型的通道限制
Comparing Channel Restrictions of Communicating State Machines, High-level Message Sequence Charts, and Multiparty Session Types
摘要：
通信状态机为分布式计算提供了形式化的基础。不幸的是，它们是图灵完备的，因此很难分析。在本文中，我们分类的通道，已提出的工作围绕验证问题的不可判定性的限制。我们比较半双工通信，存在B-有界性，和k-同步性。这些限制并不能阻止通信信道任意增长，但仍然限制了模型的能力。每个限制都会产生一组语言，因此，对于每一对限制，我们检查一个是否包含另一个，或者它们是否不可比。我们调查他们的关系在两个不同的上下文中：第一，一个通信状态机，和，第二，一个通信协议规范使用高层次的消息序列图。令人惊讶的是，这两种情况产生了不同的结论。此外，我们将多方会话类型，另一种方法来指定通信协议，到我们的分类。我们表明，多方会话类型的语言是半双工的，存在1-有界的，1-同步。为了显示这一结果，我们提供了第一个正式的嵌入到高层次的消息序列图的多方会话类型。
英文摘要：
Communicating state machines provide a formal foundation for distributed computation. Unfortunately, they are Turing-complete and, thus, challenging to analyse. In this paper, we classify restrictions on channels which have been proposed to work around the undecidability of verification questions. We compare half-duplex communication, existential B-boundedness, and k-synchronisability. These restrictions do not prevent the communication channels from growing arbitrarily large but still restrict the power of the model. Each restriction gives rise to a set of languages so, for every pair of restrictions, we check whether one subsumes the other or if they are incomparable. We investigate their relationship in two different contexts: first, the one of communicating state machines, and, second, the one of communication protocol specifications using high-level message sequence charts. Surprisingly, these two contexts yield different conclusions. In addition, we integrate multiparty session types, another approach to specify communication protocols, into our classification. We show that multiparty session type languages are half-duplex, existentially 1-bounded, and 1-synchronisable. To show this result, we provide the first formal embedding of multiparty session types into high-level message sequence charts.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
