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.
This work was supported in part by the Digiteo Île-de-France project Pactole 2009-38HD. A preliminary version of this work appears as a 2-pages Brief Announcement in DISC 2013.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Agmon, N., Peleg, D.: Fault-tolerant gathering algorithms for autonomous mobile robots. SIAM Journal on Computing 36(1), 56–82 (2006)
Almeida, J.B., Barbosa, M., Bangerter, E., Barthe, G., Krenn, S., Béguelin, S.Z.: Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. In: Yu, T., Danezis, G., Gligor, V.D. (eds.) ACM Conference on Computer and Communications Security, pp. 488–500. ACM (2012)
Berard, B., Millet, L., Potop-Butucaru, M., Thierry-Mieg, Y., Tixeuil, S.: Formal verification of Mobile Robot Protocols. Technical report (May 2013)
Bezem, M., Bol, R., Groote, J.F.: Formalizing Process Algebraic Verifications in the Calculus of Constructions. Formal Aspects of Computing 9, 1–48 (1997)
Bonnet, F., Défago, X., Petit, F., Potop-Butucaru, M.G., Tixeuil, S.: Brief Announcement: Discovering and Assessing Fine-Grained Metrics in Robot Networks Protocols. In: Richa, A.W., Scheideler, C. (eds.) SSS 2012. LNCS, vol. 7596, pp. 282–284. Springer, Heidelberg (2012)
Bouzid, Z., Potop-Butucaru, M.G., Tixeuil, S.: Optimal Byzantine-Resilient Convergence in Uni-Dimensional Robot Networks. Theoretical Computer Science 411(34-36), 3154–3168 (2010)
Cadilhac, M., Hérault, T., Lassaigne, R., Peyronnet, S., Tixeuil, S.: Evaluating complex MAC protocols for sensor networks with APMC. Electronic Notes in Theoretical Computer Science 185, 33–46 (2007)
Cansell, D., Méry, D.: The Event-B Modelling Method: Concepts and Case Studies. In: Logics of Specification Languages, pp. 47–152. Springer (2007)
Castéran, P., Filou, V., Mosbah, M.: Certifying Distributed Algorithms by Embedding Local Computation Systems in the Coq Proof Assistant. In: Bouhoula, A., Ida, T. (eds.) Symbolic Computation in Software Science, SCSS 2009 (2009)
Chou, C.-T.: Mechanical Verification of Distributed Algorithms in Higher-Order Logic. The Computer Journal 38, 158–176 (1995)
Clément, J., Delporte-Gallet, C., Fauconnier, H., Sighireanu, M.: Guidelines for the verification of population protocols. In: ICDCS, Minneapolis, Minnesota, USA, pp. 215–224. IEEE Computer Society (June 2011)
Coquand, T., Paulin-Mohring, C.: Inductively Defined Types. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg (1990)
Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA + Proofs. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 147–154. Springer, Heidelberg (2012)
Deng, Y., Monin, J.-F.: Verifying Self-stabilizing Population Protocols with Coq. In: Chin, W.-N., Qin, S. (eds.) Third IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), Tianjin, China, pp. 201–208. IEEE Computer Society (July 2009)
Devismes, S., Lamani, A., Petit, F., Raymond, P., Tixeuil, S.: Optimal Grid Exploration by Asynchronous Oblivious Robots. In: Richa, A.W., Scheideler, C. (eds.) SSS 2012. LNCS, vol. 7596, pp. 64–76. Springer, Heidelberg (2012)
Dubois, S., Tixeuil, S.: A Taxonomy of Daemons in Self-stabilization. Technical Report 1110.0334, ArXiv eprint (October 2011)
Fellahi, N., Bonakdarpour, B., Tixeuil, S.: Rigorous performance evaluation of self-stabilization using probabilistic model checking. In: Proceedings of the International Conference on Reliable Distributed Systems (SRDS 2013), Braga, Portugal. IEEE Computer Society (September 2013)
Fischer, M.J., Lynch, N.A., Paterson, M.: Impossibility of Distributed Consensus with One Faulty Process. J. ACM 32(2), 374–382 (1985)
Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2012)
Fokkink, W.: Modelling Distributed Systems. EATCS Texts in Theoretical Computer Science. Springer (2007)
Gonthier, G.: Formal–Proof The Four-Color Theorem. Notices of the AMS 55, 1370 (2008)
Gonthier, G.: Engineering Mathematics: the Odd Order Theorem Proof. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 1–2. ACM (2013)
Küfner, P., Nestmann, U., Rickmann, C.: Formal Verification of Distributed Algorithms. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 209–224. Springer, Heidelberg (2012)
Lamport, L.: Byzantizing Paxos by Refinement. In: Peleg, D. (ed.) DISC 2001. LNCS, vol. 6950, pp. 211–224. Springer, Heidelberg (2011)
Lamport, L., Shostak, R., Pease, M.: The Byzantine Generals Problem. ACM Transactions on Programming Languages and Systems 4(3), 382–401 (1982)
Leroy, X.: A Formally Verified Compiler Back-End. Journal of Automated Reasoning 43(4), 363–446 (2009)
Litovsky, I., Métivier, Y., Sopena, É.: Graph Relabelling Systems and Distributed Algorithms. In: Ehrig, H., Kreowski, H.-J., Montanari, U., Rozenberg, G. (eds.) Handbook of Graph Grammars and Computing by Graph Transformation, vol. 3, pp. 1–56. World Scientific (1999)
Mccarthy, J., Painter, J.: Correctness of a Compiler for Arithmetic Expressions. In: Proceedings of Applied Mathematica. Mathematical Aspects of Computer Science, vol. 19, pp. 33–41. American Mathematical Society (1967)
Pease, M.C., Shostak, R.E., Lamport, L.: Reaching Agreement in the Presence of Faults. J. ACM 27(2), 228–234 (1980)
Suzuki, I., Yamashita, M.: Distributed Anonymous Mobile Robots: Formation of Geometric Patterns. SIAM Journal of Computing 28(4), 1347–1363 (1999)
Théry, L., Hanrot, G.: Primality Proving with Elliptic Curves. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 319–333. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Auger, C., Bouzid, Z., Courtieu, P., Tixeuil, S., Urbain, X. (2013). Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. In: Higashino, T., Katayama, Y., Masuzawa, T., Potop-Butucaru, M., Yamashita, M. (eds) Stabilization, Safety, and Security of Distributed Systems. SSS 2013. Lecture Notes in Computer Science, vol 8255. Springer, Cham. https://doi.org/10.1007/978-3-319-03089-0_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-03089-0_13
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03088-3
Online ISBN: 978-3-319-03089-0
eBook Packages: Computer ScienceComputer Science (R0)