Impossibility of gathering, a certification
From MaRDI portal
Publication:483063
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
- scientific article; zbMATH DE number 3291623 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- 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
- 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
(19)- Synchronous gathering without multiplicity detection: a certified algorithm
- TuringMobile: a Turing machine of oblivious mobile robots with limited visibility and its applications
- Verification of agent navigation in partially-known environments
- Model checking of robot gathering
- The agreement power of disagreement
- Certified impossibility results and analyses in Coq of some randomised distributed algorithms
- Gathering on a circle with limited visibility by anonymous oblivious robots
- The Agreement Power of Disagreement
- Parameterized verification of algorithms for oblivious robots on a ring
- Embedded pattern formation by asynchronous robots without chirality
- Certified universal gathering in \(\mathbb {R}^2\) for oblivious mobile robots
- Gathering on a circle with limited visibility by anonymous oblivious robots
- Impossibility of gathering by a set of autonomous mobile robots
- Certification of an exact worst-case self-stabilization time
- Synchronous gathering without multiplicity detection: a certified algorithm
- Wait-free gathering without chirality
- Stand up indulgent gathering
- Stand up indulgent gathering
- TuringMobile: a Turing machine of oblivious mobile robots with limited visibility and its applications
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)
