 |
Reports
Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots
Thibaut Balabonski
1, 2
Pierre Courtieu
3
Robin Pelle
2
Lionel Rieg
4
Sébastien Tixeuil
5, 6, 7
Xavier Urbain
8
2
VALS - LRI - Vérification d'Algorithmes, Langages et Systèmes (LRI)
LRI - Laboratoire de Recherche en Informatique
8
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
Author IdHAL : pierre-courtieu ORCID : https://orcid.org/0000-0001-8789-9781
Robin Pelle 2
Author IdHAL : robin-pelle ORCID : https://orcid.org/0000-0001-6837-2108
Lionel Rieg 4
Author IdHAL : lionel-rieg
Sébastien Tixeuil 5, 6, 7
Author
Xavier Urbain 8
Author IdHAL : xavier-urbain
1
Université Paris-Saclay (Espace Technologique, Bat. Discovery - RD 128 - 2e ét., 91190 Saint-Aubin - France)
2
VALS - LRI - Vérification d'Algorithmes, Langages et Systèmes (LRI) (Université Paris Sud
Bat. 650 - Lovelace
91405 Orsay Cedex - France)
- LRI - Laboratoire de Recherche en Informatique (LRI - Bâtiments 650-660 Université Paris-Sud 91405 Orsay Cedex - France)
- CentraleSupélec (3, rue Joliot Curie, Plateau de Moulon, 91192 GIF-SUR-YVETTE Cedex - France)
- UP11 - Université Paris-Sud - Paris 11 (Bâtiment 300 - 91405 Orsay 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
YALE - Department of Computer Science (Yale University PO BOX 208285 New Haven, 06520-8285 - United States)
- Yale University [New Haven] (157 Church Street, New Haven, CT 06510-2100 - United States)
5
NPA - Networks and Performance Analysis (France)
- LIP6 (4 Place JUSSIEU 75252 PARIS CEDEX 05 - France)
- SU - Sorbonne Université (21 rue de l’École de médecine - 75006 Paris - France)
- CNRS - Centre National de la Recherche Scientifique : UMR7606 (France)
6
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)
7
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)
8
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 : Oblivious Mobile Robots have been studied both in continuous Euclidean spaces, and discrete spaces (that is, graphs). However the obtained literature forms distinct sets of results for the two settings. In this paper, we explore the possibility of transforming results obtained in one model into results for the other one. Our approach focuses on certified results using the COQ proof assistant.
Document type :
Reports
Domain :
Complete list of metadatas
https://hal.sorbonne-universite.fr/hal-01762962
Contributor : Sébastien Tixeuil <>
Submitted on : Tuesday, April 10, 2018 - 3:24:52 PM
Last modification on : Wednesday, September 16, 2020 - 5:48:15 PM
Contributor : Sébastien Tixeuil <>
Submitted on : Tuesday, April 10, 2018 - 3:24:52 PM
Last modification on : Wednesday, September 16, 2020 - 5:48:15 PM
Files
main_tr.pdf
Files produced by the author(s)
Identifiers
- HAL Id : hal-01762962, version 1
Collections
CNRS | EC-LYON | CNAM | INSTITUT-TELECOM | LARA | CENTRALESUPELEC | UNIV-LYON1 | INSA-LYON | INRIA | UMR8623 | LIRIS | LRI-VALS | UNIV-PARIS-SACLAY | UNIV-HESAM | INSA-GROUPE | SORBONNE-UNIVERSITE | CEDRIC-CNAM | LIP6 | UNIV-LYON2 | SU-SCIENCES | UDL
Citation
Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, et al.. Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots. [Research Report] Sorbonne Université, CNRS, Laboratoire d’Informatique de Paris 6, LIP6, F-75005 Paris, France. 2018, pp.1-12. ⟨hal-01762962⟩
Metrics
Record views
719
Files downloads