不可能收集，证明
Impossibility of Gathering, a Certification
摘要：
分布式计算的最新进展突出了自主移动机器人群的模型和算法，这些机器人自组织和合作来解决全局目标。到目前为止，绝大多数作品都考虑手工算法和正确性证明。本文建立在以前提出的正式框架，以证明分布式算法，致力于自主移动机器人在连续空间中发展的不可能性结果的正确性。作为一个案例研究，我们考虑的问题，收集所有机器人在一个特定的位置，事先不知道。一个基本的（但尚未正式认证）结果，由于铃木和山下，指出这个简单的任务是不可能的两个机器人执行确定性代码，并最初位于不同的位置。我们不仅获得了原始不可能性结果的认证证明，而且还得到了更一般的不可能性，即当任何两个机器人最初可能处于相同的确切位置时，偶数个机器人聚集在一起。
英文摘要：
Recent advances in Distributed Computing highlight models and algorithms for autonomous swarms of mobile robots that self-organise and cooperate to solve global objectives. The overwhelming majority of works so far considers handmade algorithms and proofs of correctness. This paper builds upon a previously proposed formal framework to certify the correctness of impossibility results regarding distributed algorithms that are dedicated to autonomous mobile robots evolving in a continuous space. As a case study, we consider the problem of gathering all robots at a particular location, not known beforehand. A fundamental (but not yet formally certified) result, due to Suzuki and Yamashita, states that this simple task is impossible for two robots executing deterministic code and initially located at distinct positions. Not only do we obtain a certified proof of the original impossibility result, we also get the more general impossibility of gathering with an even number of robots, when any two robots are possibly initially at the same exact location.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
