Certified Gathering of Oblivious Mobile Robots: survey of recent results and open problems - Sorbonne Université Accéder directement au contenu
Communication Dans Un Congrès Année : 2017

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

Résumé

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.
Fichier non déposé

Dates et versions

hal-01549942 , version 1 (29-06-2017)

Identifiants

Citer

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⟩
903 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More