Impossibility of gathering, a certification
From MaRDI portal
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 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.
Recommendations
- Impossibility of gathering by a set of autonomous mobile robots
- The impossibility of coherence
- Impossibility in belief merging
- Certifying inexpressibility
- An impossibility theorem for verisimilitude
- Impossibility results with resoluteness
- The impossible problem
- scientific article; zbMATH DE number 4061191
Cites work
- A formally verified compiler back-end
- Distributed Anonymous Mobile Robots: Formation of Geometric Patterns
- Distributed computing by mobile robots: gathering
- Engineering mathematics: the odd order theorem proof
- Formal proof - the four color theorem
- scientific article; zbMATH DE number 3291623 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Introduction to bisimulation and coinduction
Cited in
(20)- Certified universal gathering in \(\mathbb {R}^2\) for oblivious mobile robots
- TuringMobile: a Turing machine of oblivious mobile robots with limited visibility and its applications
- Verification of agent navigation in partially-known environments
- Parameterized verification of algorithms for oblivious robots on a ring
- Embedded pattern formation by asynchronous robots without chirality
- Impossibility of gathering by a set of autonomous mobile robots
- Certification of an exact worst-case self-stabilization time
- The agreement power of disagreement
- Certified impossibility results and analyses in Coq of some randomised distributed algorithms
- Model checking of robot gathering
- Wait-free gathering without chirality
- TuringMobile: a Turing machine of oblivious mobile robots with limited visibility and its applications
- Synchronous gathering without multiplicity detection: a certified algorithm
- Stand up indulgent gathering
- Stand up indulgent gathering
- Synchronous gathering without multiplicity detection: a certified algorithm
- The Agreement Power of Disagreement
- Gathering on a circle with limited visibility by anonymous oblivious robots
- Gathering on a circle with limited visibility by anonymous oblivious robots
- Deterministic color-optimal self-stabilizing semi-synchronous gathering: two certified algorithms
This page was built for publication: Impossibility of gathering, a certification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q483063)
