分布式任务可解性中逻辑障碍存在性的判定

为研究分布式任务可解性,Goubault、Ledent与Rajsbaum设计了一种动态认知逻辑模型,其等价于分布式计算拓扑模型。在该逻辑模型中,特定分布式任务的不可解性可通过寻找称为逻辑障碍的公式来证明。该逻辑方法极具吸引力,因为阻止任务求解的具体公式将对不可解性具有直观因素的隐含意义。然而,逻辑障碍何时存在以及如何系统构造具体逻辑障碍公式(若存在)尚缺乏充分研究。此外,已证明存在某些可解但不容许逻辑障碍的任务。本文中,我们基于模拟技术提出一种证明分布式任务可解性无逻辑障碍的方法。进而,我们给出判定有限协议与有限任务是否存在逻辑障碍的方法,若存在则构造具体障碍。利用该方法,我们证明不含分布式知识的标认知逻辑语言不容许k-集一致任务可解性的逻辑障碍。我们还表明,即使在含分布式知识的认知逻辑语言中,多轮即时快照也不存在逻辑障碍。此外,对于全知模型,我们提供了表明k-集一致任务不可解性的具体障碍公式。