Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots

Thibaut Balabonski; Pierre Courtieu; Robin Pelle; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain

Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots

Thibaut Balabonski ^{1, 2} Pierre Courtieu ³ Robin Pelle ² Lionel Rieg ⁴ Sébastien Tixeuil ^{5, 6, 7} Xavier Urbain ⁸

1 Université Paris-Saclay

2 VALS - LRI - Vérification d'Algorithmes, Langages et Systèmes (LRI)

LRI - Laboratoire de Recherche en Informatique

3 CEDRIC - Centre d'études et de recherche en informatique et communications

4 YALE - Department of Computer Science

5 NPA - Networks and Performance Analysis

LIP6 - Laboratoire d'Informatique de Paris 6

6 LINCS - Laboratory of Information, Network and Communication Sciences

7 IUF - Institut Universitaire de France

8 DRIM - Distribution, Recherche d'Information et Mobilité

LIRIS - Laboratoire d'InfoRmatique en Image et Systèmes d'information

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 :

Computer Science [cs] / Distributed, Parallel, and Cluster Computing [cs.DC]

Computer Science [cs] / Computational Geometry [cs.CG]

Computer Science [cs] / Data Structures and Algorithms [cs.DS]

Computer Science [cs] / Ubiquitous Computing

Computer Science [cs] / Mobile Computing

Computer Science [cs] / Robotics [cs.RO]

Complete list of metadatas

Cited literature [44 references] Display Hide Download

https://hal.sorbonne-universite.fr/hal-01762962
Contributor : Sébastien Tixeuil <>
Submitted on : Tuesday, April 10, 2018 - 3:24:52 PM
Last modification on : Tuesday, May 14, 2019 - 10:12:50 AM

main_tr.pdf

Files produced by the author(s)

Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots

Files

Identifiers

Collections

Citation

Export

Metrics

555

76

Contact

Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots

Files

Identifiers

Collections

Citation

Export

Share

Metrics

555

76

Contact