Impossibility of gathering, a certification
From MaRDI portal
Publication:483063
DOI10.1016/J.IPL.2014.11.001zbMATH Open1317.68264arXiv1405.5902OpenAlexW2082183470MaRDI QIDQ483063FDOQ483063
Authors: Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain 
Publication date: 15 December 2014
Published in: Information Processing Letters (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1405.5902
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
Analysis of algorithms (68W40) Computer graphics; computational geometry (digital and algorithmic aspects) (68U05) Artificial intelligence for robotics (68T40) Distributed algorithms (68W15)
Cites Work
- Distributed computing by mobile robots: gathering
- Distributed Anonymous Mobile Robots: Formation of Geometric Patterns
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Formal proof - the four color theorem
- Introduction to bisimulation and coinduction
- Title not available (Why is that?)
- Title not available (Why is that?)
- A formally verified compiler back-end
- Engineering mathematics: the odd order theorem proof
Cited In (20)
- Synchronous gathering without multiplicity detection: a certified algorithm
- TuringMobile: a Turing machine of oblivious mobile robots with limited visibility and its applications
- Certified universal gathering in \(\mathbb {R}^2\) for oblivious mobile robots
- Synchronous gathering without multiplicity detection: a certified algorithm
- Wait-free gathering without chirality
- The agreement power of disagreement
- TuringMobile: a Turing machine of oblivious mobile robots with limited visibility and its applications
- Verification of agent navigation in partially-known environments
- Stand up indulgent gathering
- Stand up indulgent gathering
- Embedded pattern formation by asynchronous robots without chirality
- Gathering on a circle with limited visibility by anonymous oblivious robots
- Parameterized verification of algorithms for oblivious robots on a ring
- Gathering on a circle with limited visibility by anonymous oblivious robots
- Certification of an exact worst-case self-stabilization time
- A Framework for Certified Self-Stabilization
- Impossibility of gathering by a set of autonomous mobile robots
- Model checking of robot gathering
- Certified impossibility results and analyses in Coq of some randomised distributed algorithms
- The Agreement Power of Disagreement
Uses Software
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)
