 |
Conference papers
Certified Impossibility Results for Byzantine-Tolerant Mobile Robots
Cédric Auger 1
Author
Zohir Bouzid 2
Mail :
Author
Pierre Courtieu 3
Mail :
Author IdHAL : pierre-courtieu ORCID : https://orcid.org/0000-0001-8789-9781
Sébastien Tixeuil 4, 5, 2
Mail : Site :
Author IdHAL : tixeuil
Xavier Urbain 1, 6
Mail :
Author IdHAL : xavier-urbain
2
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)
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
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)
5
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)
6
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 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 :
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 : Wednesday, June 24, 2020 - 4:18:58 PM
Contributor : Sébastien Tixeuil <>
Submitted on : Tuesday, January 14, 2014 - 3:30:47 PM
Last modification on : Wednesday, June 24, 2020 - 4:18:58 PM
Links full text
Identifiers
- HAL Id : hal-00930267, version 1
- DOI : 10.1007/978-3-319-03089-0_13
Collections
CNRS | INRIA | INSTITUT-TELECOM | UPMC | LIP6 | UMR8623 | CNAM | LRI-VALS | UNIV-HESAM | SORBONNE-UNIVERSITE | CEDRIC-CNAM | SU-SCIENCES
Citation
Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil, Xavier Urbain. Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. International Symposium on Stabilization, Safety, and Security of Distributed Systems, Nov 2013, Osaka, Japan. pp.178-190, ⟨10.1007/978-3-319-03089-0_13⟩. ⟨hal-00930267⟩
Metrics
Record views
