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

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.
Type de document :
Communication dans un congrès
Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems (FMICS/AVOCS), Sep 2017, Turin, Italy. Springer, Proceedings of AVOCS 2017, 10471, pp.165-181, 2017, Lecture Notes in Computer Science. 〈https://easychair.org/cfp/FMICS-AVoCS2017〉. 〈10.1007/978-3-319-67113-0_11〉
Liste complète des métadonnées

http://hal.upmc.fr/hal-01549942
Contributeur : Sébastien Tixeuil <>
Soumis le : jeudi 29 juin 2017 - 11:14:23
Dernière modification le : jeudi 19 avril 2018 - 14:38:05

Identifiants

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. Springer, Proceedings of AVOCS 2017, 10471, pp.165-181, 2017, Lecture Notes in Computer Science. 〈https://easychair.org/cfp/FMICS-AVoCS2017〉. 〈10.1007/978-3-319-67113-0_11〉. 〈hal-01549942〉

Partager

Métriques

Consultations de la notice

684