分布式计算的弱模型及其与模态逻辑的联系

本文提出了分布式计算的弱模型分类。我们专注于确定性分布式算法，并研究比广泛研究的端口编号模型更弱的计算模型。在端口编号模型中，度为d的节点通过d个输入端口接收消息，并通过d个输出端口发送消息，两者都编号为1,2,...,d。在本文中，VVc是可以在标准端口编号模型中解决的所有图问题的类。我们研究VVc的以下子类：VV：输入端口i和输出端口i不一定连接到同一个邻居。MV：输入端口未编号；算法接收消息的多重集。SV：输入端口未编号；算法接收消息的集合。VB：输出端口未编号；算法向所有输出端口发送相同的消息。MB：MV和VB的组合。SB：SV和VB的组合。现在我们有许多平凡的包含关系，例如SB ⊆ MB ⊆ VB ⊆ VV ⊆ VVc，但例如VB ⊆ SV或SV ⊆ VB是否成立并不明显。然而，事实证明我们可以识别这些类上的一个线性序。我们证明SB ⊂neq MB = VB ⊂neq SV = MV = VV ⊂neq VVc。这些类的常数时间版本也是如此。我们还表明这些类的常数时间变体可以用相应的模态逻辑来刻画。因此，本文中识别的线性序对模态逻辑的表达性研究有直接影响。反之，可以使用模态逻辑的工具来研究这些类。