 |
Conference papers
A Certified Universal Gathering Algorithm for Oblivious Mobile Robots
Pierre Courtieu
1, 2, 3
Lionel Rieg
4
Sébastien Tixeuil
5, 6, 7, 8, 9
Xavier Urbain
10, 11
3
CEDRIC - SYS - CEDRIC. Systèmes sûrs
CEDRIC - Centre d'études et de recherche en informatique et communications
Pierre Courtieu 1, 2, 3
Author IdHAL : pierre-courtieu ORCID : https://orcid.org/0000-0001-8789-9781
Lionel Rieg 4
Author IdHAL : lionel-rieg
Sébastien Tixeuil 5, 6, 7, 8, 9
Author
Xavier Urbain 10, 11
Author IdHAL : xavier-urbain
1
GALLIUM - Langages de programmation, types, compilation et preuves (France)
- Inria de Paris (2 rue Simone Iff -
CS 42112 -
75589 Paris Cedex 12 - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
2
CEDRIC - Centre d'études et de recherche en informatique et communications (292 rue Saint-Martin
75141 PARIS Cedex 03
Case courrier 2D4P30 - France)
- ENSIIE - Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise : EA4629 (France)
- CNAM - Conservatoire National des Arts et Métiers [CNAM] : EA4629 (France)
3
CEDRIC - SYS - CEDRIC. Systèmes sûrs
- CEDRIC - Centre d'études et de recherche en informatique et communications (292 rue Saint-Martin
75141 PARIS Cedex 03
Case courrier 2D4P30 - France)
- ENSIIE - Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise : EA4629 (France)
- CNAM - Conservatoire National des Arts et Métiers [CNAM] : EA4629 (France)
4
Chaire Algorithmes, machines et langages (11 place Marcelin Berthelot
75005 PARIS - France)
5
LIP6 - Laboratoire d'Informatique de Paris 6 (4 Place JUSSIEU 75252 PARIS CEDEX 05 - France)
- UPMC - Université Pierre et Marie Curie - Paris 6 (4 place Jussieu - 75005 Paris - France)
- CNRS - Centre National de la Recherche Scientifique : UMR7606 (France)
6
UPMC - Université Pierre et Marie Curie - Paris 6 (4 place Jussieu - 75005 Paris - France)
7
NPA - Networks and Performance Analysis (France)
- LIP6 - Laboratoire d'Informatique de Paris 6 (4 Place JUSSIEU 75252 PARIS CEDEX 05 - France)
- UPMC - Université Pierre et Marie Curie - Paris 6 (4 place Jussieu - 75005 Paris - France)
- CNRS - Centre National de la Recherche Scientifique : UMR7606 (France)
8
IUF - Institut Universitaire de France (Maison des Universités 103 Boulevard Saint-Michel 75005 Paris - France)
- M.E.N.E.S.R. - Ministère de l'Education nationale, de l’Enseignement supérieur et de la Recherche (1 rue Descartes - 75231 Paris cedex 05 - France)
9
LINCS - Laboratory of Information, Network and Communication Sciences (23 avenue d'Italie 75013 Paris - France)
- UPMC - Université Pierre et Marie Curie - Paris 6 (4 place Jussieu - 75005 Paris - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
- IMT - Institut Mines-Télécom [Paris] (37-39 Rue Dareau, 75014 Paris - France)
10
LRI - Laboratoire de Recherche en Informatique (LRI - Bâtiments 650-660 Université Paris-Sud 91405 Orsay Cedex - France)
- UP11 - Université Paris-Sud - Paris 11 (Bâtiment 300 - 91405 Orsay cedex - France)
- CentraleSupélec (3, rue Joliot Curie, Plateau de Moulon, 91192 GIF-SUR-YVETTE Cedex - France)
- CNRS - Centre National de la Recherche Scientifique : UMR8623 (France)
Abstract : We present a new algorithm for the problem of universal gathering mobile oblivious robots (that is, starting from any initial configuration that is not bivalent, using any number of robots, the robot reach in a finite number of steps the same position, not known beforehand) without relying on a common chirality.
We give very strong guaranties on the correctness of our algorithm by proving formally that it is correct, using the Coq proof assistant.
To our knowledge, this is the first certified positive (and constructive) result in the context of oblivious mobile robots. It demonstrates both the effectiveness of the approach to obtain new algorithms that are truly generic, and its manageability since the amount of developed code remains human readable.
Document type :
Conference papers
Domain :
Complete list of metadata
https://hal.sorbonne-universite.fr/hal-01349061
Contributor : Sébastien Tixeuil <>
Submitted on : Tuesday, July 26, 2016 - 3:53:10 PM
Last modification on : Thursday, March 4, 2021 - 4:16:19 PM
Contributor : Sébastien Tixeuil <>
Submitted on : Tuesday, July 26, 2016 - 3:53:10 PM
Last modification on : Thursday, March 4, 2021 - 4:16:19 PM
Identifiers
- HAL Id : hal-01349061, version 1
Collections
UPMC | CNRS | CNAM | INSTITUT-TELECOM | CDF | UMR8623 | LIP6 | INRIA | TDS-MACS | CENTRALESUPELEC | LRI-VALS | UNIV-HESAM | SORBONNE-UNIVERSITE | CEDRIC-CNAM | SU-SCIENCES | PSL
Citation
Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. A Certified Universal Gathering Algorithm for Oblivious Mobile Robots. Distributed Computing (DISC), Sep 2016, Paris, France. ⟨hal-01349061⟩
Metrics
Record views