用认知μ-演算证明集一致任务的不可解性

Susumu Nishimura

用认知μ-演算证明集一致任务的不可解性

分布式、并行与集群计算 2022-05-16 v1 计算机科学中的逻辑

作者: Susumu Nishimura

摘要

本文在逻辑方法的框架内，通过构造一个合适的认知逻辑公式，证明了 $k$ -集一致任务的不可解性。 $k$ -集一致任务的不可解性是一个众所周知的事实，它是组合拓扑学经典结果Sperner引理的直接推论。然而，Sperner引理并未给出对不可解性的良好直观理解，而是将其隐藏在其组合陈述的优雅性背后。逻辑方法的长处在于它能通过一个具体公式解释不可解的原因，但迄今为止尚未给出针对 $k$ -集一致任务一般不可解结果的认知公式。我们采用认知 $\mu$ -演算的一个变体，它将标准认知逻辑用分布式知识算子和命题不动点进行扩展，作为逻辑的正式语言。借助这些扩展，我们可以提供一个提及高维连通性的认知 $\mu$ -演算公式，而这正是Sperner引理原始证明中的关键，从而表明 $k$ -集一致任务即便通过多轮协议也无法可解。此外，我们还展示了同一公式可用于确立 $k$ -并发性（一种2轮协议的子模型）的不可解性。

关键词

k-集一致认知μ-演算逻辑方法不可解性分布式知识多轮协议

引用

@article{arxiv.2205.06452,
  title  = {Proving Unsolvability of Set Agreement Task with Epistemic mu-Calculus},
  author = {Susumu Nishimura},
  journal= {arXiv preprint arXiv:2205.06452},
  year   = {2022}
}

用认知μ-演算证明集一致任务的不可解性

摘要

关键词

引用

相关论文