通信状态机、高层消息序列图与多方会话类型的信道限制比较

通信状态机为分布式计算提供了形式化基础。遗憾的是，它们是图灵完备的，因而难以分析。本文对为规避验证问题的不可判定性而提出的信道限制进行了分类，比较了半双工通信、存在性 B 有界性以及 k 可同步性。这些限制并未阻止通信信道任意增长，但仍约束了模型的表达能力。每种限制都对应一组语言，因此对于每对限制，我们检验其一是否包含另一，或二者不可比较。我们在两种不同背景下考察其关系：其一是通信状态机，其二是使用高层消息序列图的通信协议规范。令人惊讶的是，这两种背景得出了不同结论。此外，我们将多方会话类型——另一种通信协议规约方法——纳入我们的分类，表明多方会话类型语言是半双工的、存在性 1 有界的以及 1 可同步的。为证明该结论，我们给出了多方会话类型到高层消息序列图的首个形式化嵌入。