Synchronous Gathering Without Multiplicity Detection: A Certified Algorithm

Abstract : In mobile robotic swarms, the gathering problem consists in coordinating all the robots so that in finite time they occupy the same location, not known beforehand. Multiplicity detection refers to the ability to detect that more than one robot can occupy a given position. When the robotic swarm operates synchronously, a well-known result by Cohen and Peleg permits to achieve gathering, provided robots are capable of multiplicity detection. We present a new algorithm for synchronous gathering, that does not assume that robots are capable of multiplicity detection, nor make any other extra assumption. Unlike previous approaches, our proof correctness is certified in the model where the protocol is defined, using the Coq proof assistant.
Type de document :
Communication dans un congrès
International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2016), Nov 2016, Lyon, France. Springer, International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2016), 10083, pp.7-19, 2016, Lecture Notes in COmputer Science. 〈10.1007/978-3-319-49259-9_2〉
Liste complète des métadonnées

http://hal.upmc.fr/hal-01491813
Contributeur : Sébastien Tixeuil <>
Soumis le : vendredi 17 mars 2017 - 14:03:56
Dernière modification le : mardi 24 avril 2018 - 13:36:16

Identifiants

Citation

Thibaut Balabonski, Amélie Delga, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. Synchronous Gathering Without Multiplicity Detection: A Certified Algorithm. International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2016), Nov 2016, Lyon, France. Springer, International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2016), 10083, pp.7-19, 2016, Lecture Notes in COmputer Science. 〈10.1007/978-3-319-49259-9_2〉. 〈hal-01491813〉

Partager

Métriques

Consultations de la notice

316