前进一步，后退一步：FLP风格证明和圆形规约技术对无颜色任务的应用
摘要：分布式计算中推导下界和不可能结果的两种通用技术进行了比较。第一种技术是通过速率加速定理（类似于Brandt, 2019）证明无等待无颜色算法的存在，旨在捕捉建立对于3色环的最小回合数的下界（Linial, 1992）的关键事实，并进行逆向归纳。第二种技术是考虑FLP风格的证明，旨在捕捉经典共识不可能性证明（Fischer, Lynch and Paterson, 1985）的关键事实，使用正向归纳。 我们展示了尽管这两种形式的证明的性质非常不同，它们之间有着密切的联系。特别地，我们证明对于每一个无颜色任务Pi，如果存在一个基于回合的证明证明了使用无等待无颜色算法解决$Pi$是不可能的，那么存在一个FLP风格的证明证明了相同的不可能性。对于一维无颜色任务（对于任意数量大于等于2的进程），我们证明了这两种证明技术具有完全相同的能力，而且更重要的是，两者都是完全的：如果一个一维无颜色任务不能被$n$个进程以无等待方式解决，则这个不可能性可以通过这两种证明技术来证明。此外，可以自动推导出一个基于回合的证明，并且可以从中生成一个FLP风格的证明。 最后，我们通过使用这两种技术来证实了任意维度的无颜色覆盖任务不能被无等待算法解决的不可能性。
作者：Hagit Attiya, Pierre Fraigniaud, Ami Paz, and Sergio Rajsbaum
论文ID：2308.04213
分类：Distributed, Parallel, and Cluster Computing
分类简称：cs.DC
提交时间：2023-08-09