Impossibility of Gathering, a Certification
Pierre Courtieu (CEDRIC), Lionel Rieg (CEDRIC, ENSIIE), Xavier Urbain, (CEDRIC, ENSIIE, LRI), S\'ebastien Tixeuil (LIP6, LINCS, IUF)

TL;DR
This paper provides a formal certification of the impossibility of gathering autonomous robots in certain conditions, extending previous results and ensuring correctness of these fundamental limitations in distributed robotics.
Contribution
It introduces a formal framework to certify impossibility results in autonomous robot gathering, including a proof of the Suzuki and Yamashita impossibility theorem and its generalization.
Findings
Certified proof of the impossibility of gathering for two robots.
Extended impossibility result for an even number of robots with potential initial overlaps.
Formal verification of fundamental limitations in autonomous robot coordination.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsOptimization and Search Problems · Distributed systems and fault tolerance · Logic, Reasoning, and Knowledge
