Certified Gathering of Oblivious Mobile Robots: survey of recent results and open problems

Thibaut Balabonski 1, 2 Pierre Courtieu 3, 4 Lionel Rieg 5, 6 Sébastien Tixeuil 7, 8, 9 Xavier Urbain 10
1 Université Paris-Saclay
2 LRI - Laboratoire de Recherche en Informatique
3 CEDRIC - Centre d'études et de recherche en informatique et communications
4 GALLIUM - Langages de programmation, types, compilation et preuves
Inria de Paris
5 CdF - Collège de France
6 Yale University [New Haven]
7 NPA - Networks and Performance Analysis
LIP6 - Laboratoire d'Informatique de Paris 6
8 IUF - Institut Universitaire de France
9 LINCS - Laboratory of Information, Network and Communication Sciences
10 DRIM - Distribution, Recherche d'Information et Mobilité
LIRIS - Laboratoire d'InfoRmatique en Image et Systèmes d'information
Abstract : Swarms of mobile robots recently attracted the focus of the Distributed Computing community. One of the fundamental problems in this context is that of gathering the robots: the robots must joint a common location, not known beforehand. Despite its apparent simplicity, this problem proved quite hard to characterise fully, due to many model variants, leading to informal error-prone reasoning. Over the past few years, a significant effort permitted to set up a formal framework, relying on the Coq proof assistant, that was used to provide certified results related to the gathering problem. We survey the main abstractions that permit to reason about oblivious mobile robots that evolve in a bidirectional Euclidean space, the distributed executions they can perform, and the variants of the gathering problem they can solve, while certifying all obtained results. We also hint path the remaining steps to obtain a certified full characterisation of the problem.
Document type :
Conference papers
Complete list of metadatas
https://hal.sorbonne-universite.fr/hal-01549942
Contributor : Sébastien Tixeuil <>
Submitted on : Thursday, June 29, 2017 - 11:14:23 AM
Last modification on : Monday, February 10, 2020 - 6:14:07 PM

Identifiers

Collections

UPMC | CNRS | EC-LYON | CNAM | INSTITUT-TELECOM | UMR8623 | LIRIS | PSL | LIP6 | INRIA | UNIV-PARIS-SACLAY | INSA-LYON | UNIV-LYON1 | LRI-VALS | UNIV-HESAM | INSA-GROUPE | SORBONNE-UNIVERSITE | CEDRIC-CNAM | UNIV-LYON2 | SU-SCIENCES | UDL

Citation

Thibaut Balabonski, Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. Certified Gathering of Oblivious Mobile Robots: survey of recent results and open problems. Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems (FMICS/AVOCS), Sep 2017, Turin, Italy. pp.165-181, ⟨10.1007/978-3-319-67113-0_11⟩. ⟨hal-01549942⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

1289

Contact

Informations

CCSD