论文标题
比较通信状态计算机，高级消息序列图和多方会话类型的频道限制
Comparing Channel Restrictions of Communicating State Machines, High-level Message Sequence Charts, and Multiparty Session Types
论文作者
论文摘要
通信状态机为分布式计算提供了正式的基础。不幸的是，他们是图灵完整的，因此在分析方面具有挑战性。在本文中，我们对渠道的限制进行了分类，这些渠道已提议围绕验证问题的不可确定性进行。我们比较半封面的通信，存在的B结合性和K-Synchronisisa。这些限制并不能阻止沟通渠道任意增长，但仍然限制了模型的力量。每个限制都会产生一组语言，因此，对于每对限制，我们检查一个语言是否包含另一个或无与伦比。我们在两种不同的情况下研究了它们的关系：首先是通信状态计算机之一，其次是使用高级消息序列图表的通信协议规范之一。令人惊讶的是，这两种情况得出了不同的结论。此外，我们将多方会话类型集成到我们的分类中。我们证明多方会话类型的语言是半双链，存在的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.
