 |
Conference papers
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
10
DRIM - Distribution, Recherche d'Information et Mobilité
LIRIS - Laboratoire d'InfoRmatique en Image et Systèmes d'information
Thibaut Balabonski 1, 2
Author IdHAL : thibaut-balabonski
Pierre Courtieu 3, 4
Author IdHAL : pierre-courtieu ORCID : https://orcid.org/0000-0001-8789-9781
Lionel Rieg 5, 6
Author IdHAL : lionel-rieg
Sébastien Tixeuil 7, 8, 9
Author IdHAL : tixeuil ORCID : https://orcid.org/0000-0002-0948-7172
Xavier Urbain 10
Author IdHAL : xavier-urbain
1
Université Paris-Saclay (Espace Technologique, Bat. Discovery - RD 128 - 2e ét., 91190 Saint-Aubin - France)
2
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)
3
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
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)
5
Yale University [New Haven] (157 Church Street, New Haven, CT 06510-2100 - United States)
6
Chaire Algorithmes, machines et langages (11 place Marcelin Berthelot
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)
- IMT - Institut Mines-Télécom [Paris] (37-39 Rue Dareau, 75014 Paris - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
- UPMC - Université Pierre et Marie Curie - Paris 6 (4 place Jussieu - 75005 Paris - France)
10
DRIM - Distribution, Recherche d'Information et Mobilité (France)
- LIRIS - Laboratoire d'InfoRmatique en Image et Systèmes d'information (Bâtiment Blaise Pascal - 20, avenue Albert Einstein - 69621 Villeurbanne cedex - France)
- UL2 - Université Lumière - Lyon 2 (86, rue Pasteur - 69007 Lyon - France)
- ECL - École Centrale de Lyon (36 avenue Guy de Collongue - 69134 Ecully cedex - France)
- Université de Lyon (92 rue Pasteur - CS 30122, 69361 Lyon Cedex 07 - France)
- UCBL - Université Claude Bernard Lyon 1 (43, boulevard du 11 novembre 1918, 69622 Villeurbanne cedex - France)
- Université de Lyon (92 rue Pasteur - CS 30122, 69361 Lyon Cedex 07 - France)
- CNRS - Centre National de la Recherche Scientifique : UMR5205 (France)
- INSA Lyon - Institut National des Sciences Appliquées de Lyon (20 Avenue Albert Einstein,
69621 Villeurbanne cedex - France)
- Université de Lyon (92 rue Pasteur - CS 30122, 69361 Lyon Cedex 07 - France)
- INSA - Institut National des Sciences Appliquées (France)
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
Domain :
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 : Friday, January 8, 2021 - 5:38:04 PM
Contributor : Sébastien Tixeuil <>
Submitted on : Thursday, June 29, 2017 - 11:14:23 AM
Last modification on : Friday, January 8, 2021 - 5:38:04 PM
Identifiers
- HAL Id : hal-01549942, version 1
- DOI : 10.1007/978-3-319-67113-0_11
Collections
UPMC | CNRS | EC-LYON | CNAM | INSTITUT-TELECOM | CDF | UMR8623 | LIRIS | LIP6 | INRIA | INSA-LYON | UNIV-LYON1 | LRI-VALS | UNIV-HESAM | INSA-GROUPE | SORBONNE-UNIVERSITE | CEDRIC-CNAM | UNIV-LYON2 | SU-SCIENCES | UDL | PSL
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⟩
Metrics
Record views