环上分布式算法验证的自动机理论方法

我们引入一种自动机理论方法，用于验证运行在环网络上的分布式算法。在分布式算法中，任意数量的进程协作以实现共同目标（例如选举领导者）。进程拥有来自无限全序域的唯一标识符（pid）。算法以同步轮次推进，每轮允许进程执行有界动作序列，如发送或接收pid、将其存储于某寄存器、以及针对关联全序比较寄存器内容。算法应独立于进程数量而正确。为规约正确性属性，我们引入一种能对进程和pid进行推理的逻辑。以领导者选举为例，它可表述在执行的末尾每个进程在某专用寄存器中存储最大pid。由于分布式算法的验证是不可判定的，我们提出一种限定轮次数的欠近似技术。这是一种吸引人的方法，因为分布式算法结束所需轮次数常比进程数指数级小。我们提供自动机理论解，将模型检测归约为交替双向字自动机的空性。总体而言，我们证明环上分布式算法的轮次有界验证是PSPACE完全的。