Certified Impossibility Results for Byzantine-Tolerant Mobile Robots

Cédric Auger; Zohir Bouzid; Pierre Courtieu; Sébastien Tixeuil; Xavier Urbain

Certified Impossibility Results for Byzantine-Tolerant Mobile Robots

Cédric Auger ¹ Zohir Bouzid ² Pierre Courtieu ³ Sébastien Tixeuil ^{4, 5, 2} Xavier Urbain ^{1, 6}

1 ENSIIE - Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise

2 NPA - Networks and Performance Analysis

LIP6 - Laboratoire d'Informatique de Paris 6

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

4 IUF - Institut Universitaire de France

5 LINCS - Laboratory of Information, Network and Communication Sciences

6 LRI - Laboratoire de Recherche en Informatique

Abstract : We propose a framework to build formal developments for robot networks using the Coq proof assistant, to state and prove formally various properties. We focus in this paper on impossibility proofs, as it is natural to take advantage of the Coq higher order calculus to reason about algorithms as abstract objects. We present in particular formal proofs of two impossibility results for convergence of oblivious mobile robots if respectively more than one half and more than one third of the robots exhibit Byzantine failures, starting from the original theorems by Bouzid et al.. Thanks to our formalisation, the corresponding Coq developments are quite compact. To our knowledge, these are the first certified (in the sense of formally proved) impossibility results for robot networks.

Document type :

Conference papers

Domain :

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

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

Computer Science [cs] / Mobile Computing

Computer Science [cs] / Performance [cs.PF]

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

Computer Science [cs] / Networking and Internet Architecture [cs.NI]

Complete list of metadatas

https://hal.sorbonne-universite.fr/hal-00930267
Contributor : Sébastien Tixeuil <>
Submitted on : Tuesday, January 14, 2014 - 3:30:47 PM
Last modification on : Tuesday, May 14, 2019 - 10:13:46 AM

Certified Impossibility Results for Byzantine-Tolerant Mobile Robots

Links full text

Identifiers

Collections

Citation

Export

Metrics

590

Contact

Certified Impossibility Results for Byzantine-Tolerant Mobile Robots

Links full text

Identifiers

Collections

Citation

Export

Share

Metrics

590

Contact