比较通信状态机、高级消息序列图和多方会话类型的通道限制。
摘要：通信状态机为分布式计算提供了形式化的基础。然而，它们是图灵完备的，因此很难进行分析。在本文中，我们对已经提出的限制通道的分类进行了讨论，以解决验证问题的不可决问题。我们比较了半双工通信、存在性B-有界性和k-同步能力。这些限制并不能阻止通信通道的任意增长，但仍然限制了模型的能力。每个限制都产生了一组语言，因此对于每对限制，我们检查其中一个是否包含另一个，或者它们是否不可比较。我们在两个不同的背景下研究了它们的关系：第一个是通信状态机的背景，第二个是使用高级消息序列图进行通信协议规范的背景。令人惊讶的是，这两个背景得出了不同的结论。此外，我们还将多方会话类型（另一种指定通信协议的方法）整合到我们的分类中。我们证明了多方会话类型语言是半双工的，存在性1-有界的和1-同步的。为了证明这一结果，我们首次将多方会话类型正式嵌入到高级消息序列图中。
作者：Felix Stutz (MPI-SWS), Damien Zufferey (MPI-SWS)
论文ID：2209.10328
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2022-09-22