论文标题
证明与认知MU-Calculus的设定协议任务无法解释性
Proving Unsolvability of Set Agreement Task with Epistemic mu-Calculus
论文作者
论文摘要
本文在逻辑方法的框架内表明，通过设计合适的认识论逻辑公式，$ k $ sets任务的不可分解性。 $ k $ set协议任务的无法解释是一个众所周知的事实，这是Sperner's Lemma的直接结果，这是组合拓扑结构的经典结果。但是，Sperner的引理并不能为无法解决性提供良好的直觉，将其隐藏在其组合陈述的优雅背后。逻辑方法的优点是，它可以解释混凝土公式无法解决的原因，但是到目前为止，还没有针对$ k $ set协议任务的一般性不明确性结果的认知公式。 我们采用了一种认知$μ$ calculus的变体，它通过分布式知识运算符和命题固定点扩展了标准的认知逻辑，作为逻辑的形式语言。通过这些扩展，我们可以提供一种认知的$μ$ calculus公式，该公式提到了更高的连通性，这对于Sperner的引理的原始证明至关重要，从而表明$ K $ -SET协议任务即使是由多轮协议也无法解决的。此外，我们还表明，相同的公式适用于建立$ k $ concurrency（2轮协议的子模型）的不可分解性。
This paper shows, in the framework of the logical method,the unsolvability of $k$-set agreement task by devising a suitable formula of epistemic logic. The unsolvability of $k$-set agreement task is a well-known fact, which is a direct consequence of Sperner's lemma, a classic result from combinatorial topology. However, Sperner's lemma does not provide a good intuition for the unsolvability,hiding it behind the elegance of its combinatorial statement. The logical method has a merit that it can account for the reason of unsolvability by a concrete formula, but no epistemic formula for the general unsolvability result for $k$-set agreement task has been presented so far. We employ a variant of epistemic $μ$-calculus, which extends the standard epistemic logic with distributed knowledge operators and propositional fixpoints, as the formal language of logic. With these extensions, we can provide an epistemic $μ$-calculus formula that mentions higher-dimensional connectivity, which is essential in the original proof of Sperner's lemma, and thereby show that $k$-set agreement tasks are not solvable even by multi-round protocols. Furthermore, we also show that the same formula applies to establish the unsolvability for $k$-concurrency, a submodel of the 2-round protocol.
