Document Open Access Logo

Swarms of Mobile Robots: Towards Versatility with Safety

Authors Pierre Courtieu , Lionel Rieg, Sébastien Tixeuil , Xavier Urbain

PDF
Thumbnail PDF

File

LITES.8.2.2.pdf
  • Filesize: 0.82 MB
  • 36 pages

Document Identifiers

Author Details

Pierre Courtieu
  • Conservatoire des arts et métiers, Cédric EA 4629, Paris, France
Lionel Rieg
  • VERIMAG, Grenoble INP - UGA, CNRS UMR 5104, Université Grenoble-Alpes, Saint Martin d'Hères, France
Sébastien Tixeuil
  • Sorbonne University, CNRS, LIP6, Paris, France
Xavier Urbain
  • Université de Lyon, Université Claude Bernard Lyon 1, CNRS, INSA Lyon, LIRIS, UMR 5205, F-69622 Villeurbanne, France

Cite AsGet BibTex

Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Swarms of Mobile Robots: Towards Versatility with Safety. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 02:1-02:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LITES.8.2.2

Abstract

We present Pactole, a formal framework to design and prove the correctness of protocols (or the impossibility of their existence) that target mobile robotic swarms. Unlike previous approaches, our methodology unifies in a single formalism the execution model, the problem specification, the protocol, and its proof of correctness. The Pactole framework makes use of the Coq proof assistant, and is specially targeted at protocol designers and problem specifiers, so that a common unambiguous language is used from the very early stages of protocol development. We stress the underlying framework design principles to enable high expressivity and modularity, and provide concrete examples about how the Pactole framework can be used to tackle actual problems, some previously addressed by the Distributed Computing community, but also new problems, while being certified correct.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Theory of computation → Self-organization
  • Theory of computation → Program reasoning
  • Theory of computation → Logic
  • Software and its engineering → Formal methods
Keywords
  • distributed algorithm
  • mobile autonomous robots
  • formal proof

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jordan Adamek, Mikhail Nesterenko, and Sébastien Tixeuil. Evaluating and optimizing stabilizing dining philosophers. In 11th European Dependable Computing Conference, EDCC 2015, Paris, France, September 7-11, 2015, pages 233-244. IEEE, 2015. Google Scholar
  2. José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, and Santiago Zanella Béguelin. Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. In ACM Conference on Computer and Communications Security, pages 488-500, 2012. Google Scholar
  3. Karine Altisen, Pierre Corbineau, and Stéphane Devismes. A framework for certified self-stabilization. In Elvira Albert and Ivan Lanese, editors, Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings, volume 9688 of Lecture Notes in Computer Science, pages 36-51. Springer-Verlag, 2016. Google Scholar
  4. Krzysztof R. Apt and Dexter C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22(6):307-309, 1986. Google Scholar
  5. The Coq Proof Assistant. scriptsizehttps://coq.inria.fr/.
  6. Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil, and Xavier Urbain. Certified Impossibility Results for Byzantine-Tolerant Mobile Robots. In Teruo Higashino, Yoshiaki Katayama, Toshimitsu Masuzawa, Maria Potop-Butucaru, and Masafumi Yamashita, editors, Stabilization, Safety, and Security of Distributed Systems - 15th International Symposium (SSS 2013), volume 8255 of Lecture Notes in Computer Science, pages 178-186, Osaka, Japan, November 2013. Springer-Verlag. Google Scholar
  7. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Continuous vs. discrete asynchronous moves: A certified approach for mobile robots. In Mohamed Faouzi Atig and Alexander A. Schwarzmann, editors, Networked Systems - 7th International Conference, (NETYS 2019), Revised Selected Papers, volume 11704 of Lecture Notes in Computer Science, pages 93-109, Marrakech, Morocco, June 2019. Springer-Verlag. Google Scholar
  8. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Brief Announcement: Computer Aided Formal Design of Swarm Robotics Algorithms. In Colette Johnen and Stefan Schmid, editors, Stabilization, Safety, and Security of Distributed Systems - 23th International Symposium, (SSS 2021), Virtual conference, November 2021. Google Scholar
  9. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Computer aided formal design of swarm robotics algorithms. CoRR, abs/2101.06966, 2021. Google Scholar
  10. Thibaut Balabonski, Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Certified gathering of oblivious mobile robots: Survey of recent results and open problems. In Laure Petrucci, Cristina Seceleanu, and Ana Cavalcanti, editors, Critical Systems: Formal Methods and Automated Verification - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems - and - 17th International Workshop on Automated Verification of Critical Systems, (FMICS-AVoCS 2017), volume 10471 of Lecture Notes in Computer Science, pages 165-181, Turin, Italy, September 2017. Springer-Verlag. Google Scholar
  11. Thibaut Balabonski, Amélie Delga, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Synchronous gathering without multiplicity detection: A certified algorithm. Theory of Computing Systems, pages 200-218, 2019. scriptsizehttps://doi.org/10.1007/s00224-017-9828-z.
  12. Thibaut Balabonski, Robin Pelle, Lionel Rieg, and Sébastien Tixeuil. A foundational framework for certified impossibility results with mobile robots on graphs. In Paolo Bellavista and Vijay K. Garg, editors, Proceedings of the 19th International Conference on Distributed Computing and Networking, ICDCN 2018, Varanasi, India, January 4-7, 2018, pages 5:1-5:10. ACM, 2018. Google Scholar
  13. Andrej Bauer. How to review formalized mathematics. scriptsizehttp://math.andrej.com/2013/08/19/how-to-review-formalized-mathematics/, August 2013.
  14. Béatrice Bérard, Pascal Lafourcade, Laure Millet, Maria Potop-Butucaru, Yann Thierry-Mieg, and Sébastien Tixeuil. Formal verification of mobile robot protocols. Distributed Computing, 29(6):459-487, 2016. Google Scholar
  15. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer-Verlag, 2004. Google Scholar
  16. François Bonnet, Xavier Défago, Franck Petit, Maria Potop-Butucaru, and Sébastien Tixeuil. Discovering and assessing fine-grained metrics in robot networks protocols. In 33rd IEEE International Symposium on Reliable Distributed Systems Workshops, SRDS Workshops 2014, Nara, Japan, October 6-9, 2014, pages 50-59. IEEE, 2014. Google Scholar
  17. Quentin Bramas and Sébastien Tixeuil. Brief Announcement: Probabilistic Asynchronous Arbitrary Pattern Formation. In George Giakkoupis, editor, 35^th ACM Symposium on Principles of Distributed Computing (PODC 2016), pages 443-445, Chicago, IL, USA, July 2016. ACM. Google Scholar
  18. Quentin Bramas and Sébastien Tixeuil. The Random Bit Complexity of Mobile Robots Scattering. International Journal of Foundations of Computer Science, 28(2):111-134, 2017. Google Scholar
  19. Pierre Castéran, Vincent Filou, and Mohamed Mosbah. Certifying Distributed Algorithms by Embedding Local Computation Systems in the Coq Proof Assistant. In Adel Bouhoula and Tetsuo Ida, editors, Symbolic Computation in Software Science (SCSS'09), 2009. Google Scholar
  20. Reuven Cohen and David Peleg. Robot Convergence via Center-of-Gravity Algorithms. In Rastislav Kralovic and Ondrej Sýkora, editors, Structural Information and Communication Complexity - 11th International Colloquium (SIROCCO 2004), volume 3104 of Lecture Notes in Computer Science, pages 79-88, Smolenice Castle, Slowakia, June 2004. Springer-Verlag. Google Scholar
  21. Reuven Cohen and David Peleg. Convergence Properties of the Gravitational Algorithm in Asynchronous Robot Systems. SIAM Journal of Computing, 34(6):1516-1528, 2005. Google Scholar
  22. Thierry Coquand and Christine Paulin-Mohring. Inductively Defined Types. In Per Martin-Löf and Grigori Mints, editors, International Conference on Computer Logic (Colog'88), volume 417 of Lecture Notes in Computer Science, pages 50-66. Springer-Verlag, 1990. Google Scholar
  23. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Impossibility of Gathering, a Certification. Information Processing Letters, 115:447-452, 2015. Google Scholar
  24. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Certified universal gathering algorithm in ℝ² for oblivious mobile robots. In Cyril Gavoille and David Ilcinkas, editors, Distributed Computing - 30th International Symposium, (DISC 2016), volume 9888 of Lecture Notes in Computer Science, pages 187-200, Paris, France, September 2016. Springer-Verlag. Google Scholar
  25. Shantanu Das, Paola Flocchini, Giuseppe Prencipe, and Nicola Santoro. Forming sequences of patterns with luminous robots. IEEE Access, 8:90577-90597, 2020. Google Scholar
  26. Shantanu Das, Paola Flocchini, Giuseppe Prencipe, Nicola Santoro, and Masafumi Yamashita. Autonomous mobile robots with lights. Theor. Comput. Sci., 609:171-184, 2016. Google Scholar
  27. Xavier Défago, Adam Heriban, Sébastien Tixeuil, and Koichi Wada. Brief announcement: Model checking rendezvous algorithms for robots with lights in euclidean space. In Jukka Suomela, editor, 33rd International Symposium on Distributed Computing, DISC 2019, October 14-18, 2019, Budapest, Hungary, volume 146 of LIPIcs, pages 41:1-41:3. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  28. Xavier Défago, Adam Heriban, Sébastien Tixeuil, and Koichi Wada. Using model checking to formally verify rendezvous algorithms for robots with lights in euclidean space. In International Symposium on Reliable Distributed Systems, SRDS 2020, Shanghai, China, September 21-24, 2020, pages 113-122. IEEE, 2020. Google Scholar
  29. Xavier Défago, Maria Potop-Butucaru, and Sébastien Tixeuil. Fault-tolerant mobile robots. In Paola Flocchini, Giuseppe Prencipe, and Nicola Santoro, editors, Distributed Computing by Mobile Entities, Current Research in Moving and Computing, volume 11340 of Lecture Notes in Computer Science, pages 234-251. Springer, 2019. Google Scholar
  30. Xavier Défago and Samia Souissi. Non-uniform circle formation algorithm for oblivious mobile robots with convergence toward uniformity. Theor. Comput. Sci., 396(1-3):97-112, 2008. Google Scholar
  31. Carole Delporte-Gallet, Hugues Fauconnier, Yan Jurski, François Laroussinie, and Arnaud Sangnier. Towards synthesis of distributed algorithms with SMT solvers. In Mohamed Faouzi Atig and Alexander A. Schwarzmann, editors, Networked Systems - 7th International Conference, NETYS 2019, Marrakech, Morocco, June 19-21, 2019, Revised Selected Papers, volume 11704 of Lecture Notes in Computer Science, pages 200-216. Springer, 2019. Google Scholar
  32. Ha Thi Thu Doan, François Bonnet, and Kazuhiro Ogata. Model checking of a mobile robots perpetual exploration algorithm. In Shaoying Liu, Zhenhua Duan, Cong Tian, and Fumiko Nagoya, editors, Structured Object-Oriented Formal Language and Method - 6th International Workshop, SOFL+MSVL 2016, Tokyo, Japan, November 15, 2016, Revised Selected Papers, volume 10189 of Lecture Notes in Computer Science, pages 201-219, 2016. Google Scholar
  33. Ha Thi Thu Doan, François Bonnet, and Kazuhiro Ogata. Model checking of robot gathering. In James Aspnes and Pascal Felber, editors, Principles of Distributed Systems - 21th International Conference (OPODIS 2017), Leibniz International Proceedings in Informatics (LIPIcs), Lisbon, Portugal, December 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  34. Ha Thi Thu Doan, Kazuhiro Ogata, and François Bonnet. Specifying a distributed snapshot algorithm as a meta-program and model checking it at meta-level. In Kisung Lee and Ling Liu, editors, 37th IEEE International Conference on Distributed Computing Systems, ICDCS 2017, Atlanta, GA, USA, June 5-8, 2017, pages 1586-1596. IEEE Computer Society, 2017. Google Scholar
  35. Ha Thi Thu Doan, Adrián Riesco, and Kazuhiro Ogata. An environment for specifying and model checking mobile ring robot algorithms. In Mohsen Ghaffari, Mikhail Nesterenko, Sébastien Tixeuil, Sara Tucci, and Yukiko Yamauchi, editors, Stabilization, Safety, and Security of Distributed Systems - 21st International Symposium, SSS 2019, Pisa, Italy, October 22-25, 2019, Proceedings, volume 11914 of Lecture Notes in Computer Science, pages 111-126. Springer, 2019. Google Scholar
  36. Fathiyeh Faghih, Borzoo Bonakdarpour, Sébastien Tixeuil, and Sandeep S. Kulkarni. Automated synthesis of distributed self-stabilizing protocols. Logical Methods in Computer Science, 14(1), 2018. Google Scholar
  37. Paola Flocchini, Giuseppe Prencipe, and Nicola Santoro, editors. Distributed Computing by Mobile Entities, volume 11340 of Lecture Notes in Computer Science, Theoretical Computer Science and General Issues. Springer Nature, 2019. Google Scholar
  38. Paola Flocchini, Giuseppe Prencipe, Nicola Santoro, and Peter Widmayer. Gathering of asynchronous oblivious robots with limited visibility. In Afonso Ferreira and Horst Reichel, editors, STACS 2001, 18th Annual Symposium on Theoretical Aspects of Computer Science, Dresden, Germany, February 15-17, 2001, Proceedings, volume 2010 of Lecture Notes in Computer Science, pages 247-258. Springer, 2001. Google Scholar
  39. Paola Flocchini, Giuseppe Prencipe, Nicola Santoro, and Peter Widmayer. Pattern formation by anonymous robots without chirality. In Francesc Comellas, Josep Fàbrega, and Pierre Fraigniaud, editors, SIROCCO 8, Proceedings of the 8th International Colloquium on Structural Information and Communication Complexity, Vall de Núria, Girona-Barcelona, Catalonia, Spain, 27-29 June, 2001, volume 8 of Proceedings in Informatics, pages 147-162. Carleton Scientific, 2001. Google Scholar
  40. Paola Flocchini, Giuseppe Prencipe, Nicola Santoro, and Peter Widmayer. Arbitrary pattern formation by asynchronous, anonymous, oblivious robots. Theoretical Computer Science, 407(1-3):412-447, 2008. Google Scholar
  41. Georges Gonthier. Formal Proof—The Four-Color Theorem. Notices of the AMS, 55(11):1382-1393, December 2008. Google Scholar
  42. Georges Gonthier. Engineering Mathematics: the Odd Order Theorem Proof. In Roberto Giacobazzi and Radhia Cousot, editors, POPL, pages 1-2. ACM, 2013. Google Scholar
  43. Rachid Guerraoui, Thomas A. Henzinger, Barbara Jobstmann, and Vasu Singh. Model checking transactional memories. In Rajiv Gupta and Saman P. Amarasinghe, editors, Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, pages 372-382. ACM, 2008. Google Scholar
  44. Adam Heriban, Xavier Défago, and Sébastien Tixeuil. Optimally gathering two robots. In Paolo Bellavista and Vijay K. Garg, editors, Proceedings of the 19th International Conference on Distributed Computing and Networking, ICDCN 2018, Varanasi, India, January 4-7, 2018, pages 3:1-3:10. ACM, 2018. Google Scholar
  45. Adam Heriban and Sébastien Tixeuil. Mobile robots with uncertain visibility sensors. In Keren Censor-Hillel and Michele Flammini, editors, Structural Information and Communication Complexity - 26th International Colloquium, (SIROCCO 2019), volume 11639 of Lecture Notes in Computer Science, pages 349-352, L'Aquila, Italy, July 2019. Springer-Verlag. Google Scholar
  46. Taisuke Izumi, Tomoko Izumi, Sayaka Kamei, and Fukuhito Ooshita. Randomized gathering of mobile robots with local-multiplicity detection. In Rachid Guerraoui and Franck Petit, editors, Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, SSS 2009, Lyon, France, November 3-6, 2009. Proceedings, volume 5873 of Lecture Notes in Computer Science, pages 384-398. Springer, 2009. Google Scholar
  47. Tomoko Izumi, Taisuke Izumi, Sayaka Kamei, and Fukuhito Ooshita. Mobile robots gathering algorithm with local weak multiplicity in rings. In Boaz Patt-Shamir and Tínaz Ekim, editors, Structural Information and Communication Complexity, 17th International Colloquium, SIROCCO 2010, Sirince, Turkey, June 7-11, 2010. Proceedings, volume 6058 of Lecture Notes in Computer Science, pages 101-113. Springer, 2010. Google Scholar
  48. Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an operating system kernel. Communications of the ACM, 53(6):107-115, 2010. Google Scholar
  49. Igor Konnov, Helmut Veith, and Josef Widder. Who is afraid of model checking distributed algorithms? Unpublished to: CAV Workshop (EC)², July 2012. Google Scholar
  50. Philipp Küfner, Uwe Nestmann, and Christina Rickmann. Formal Verification of Distributed Algorithms - From Pseudo Code to Checked Proofs. In Jos C. M. Baeten, Thomas Ball, and Frank S. de Boer, editors, IFIP TCS, volume 7604 of Lecture Notes in Computer Science, pages 209-224, Amsterdam, The Netherlands, September 2012. Springer-Verlag. Google Scholar
  51. Sandeep S. Kulkarni, Borzoo Bonakdarpour, and Ali Ebnenasir. Mechanical verification of automatic synthesis of fault-tolerant programs. In Sandro Etalle, editor, Logic Based Program Synthesis and Transformation, 14th International Symposium, LOPSTR 2004, Verona, Italy, August 26-28, 2004, Revised Selected Papers, volume 3573 of Lecture Notes in Computer Science, pages 36-52. Springer, 2004. Google Scholar
  52. Leslie Lamport. On interprocess communication. part I: basic formalism. Distributed Comput., 1(2):77-85, 1986. Google Scholar
  53. Leslie Lamport. On interprocess communication. part II: algorithms. Distributed Comput., 1(2):86-101, 1986. Google Scholar
  54. Leslie Lamport and Stephan Merz. Specifying and verifying fault-tolerant systems. In Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer Science, pages 41-76. Springer-Verlag, 1994. Google Scholar
  55. Xavier Leroy. A Formally Verified Compiler Back-End. Journal of Automated Reasoning, 43(4):363-446, 2009. Google Scholar
  56. Assia Mahboubi. Checking machine-checked proofs. scriptsizehttps://project.inria.fr/coqexchange/checking-machine-checked-proofs/, July 2017.
  57. Vincent Rahli Mark Bickford, Robert L. Constable. Logic of events, a framework to reason about distributed systems. In 2012 Languages for Distributed Algorithms Workshop, Philadelphia, PA, 2012. Google Scholar
  58. Kenneth L. McMillan and Oded Padon. Ivy: A multi-modal verification tool for distributed algorithms. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, volume 12225 of Lecture Notes in Computer Science, pages 190-202. Springer, 2020. Google Scholar
  59. Laure Millet, Maria Potop-Butucaru, Nathalie Sznajder, and Sébastien Tixeuil. On the synthesis of mobile robots algorithms: The case of ring gathering. In Pascal Felber and Vijay K. Garg, editors, Stabilization, Safety, and Security of Distributed Systems - 16th International Symposium, (SSS 2014), volume 8756 of Lecture Notes in Computer Science, pages 237-251, Paderborn, Germany, September 2014. Springer-Verlag. Google Scholar
  60. Takashi Okumura, Koichi Wada, and Xavier Défago. Optimal rendezvous l-algorithms for asynchronous mobile robots with external-lights. In Jiannong Cao, Faith Ellen, Luis Rodrigues, and Bernardo Ferreira, editors, 22nd International Conference on Principles of Distributed Systems, OPODIS 2018, December 17-19, 2018, Hong Kong, China, volume 125 of LIPIcs, pages 24:1-24:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  61. Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. Ivy: safety verification by interactive generalization. In Chandra Krintz and Emery Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 614-630. ACM, 2016. Google Scholar
  62. Maria Potop-Butucaru, Nathalie Sznajder, Sébastien Tixeuil, and Xavier Urbain. Formal methods for mobile robots. In Paola Flocchini, Giuseppe Prencipe, and Nicola Santoro, editors, Distributed Computing by Mobile Entities, Current Research in Moving and Computing, volume 11340 of Lecture Notes in Computer Science, pages 278-313. Springer, 2019. Google Scholar
  63. Giuseppe Prencipe. Impossibility of gathering by a set of autonomous mobile robots. Theoretical Computer Science, 384(2-3):222-231, 2007. Google Scholar
  64. Arnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru, and Sébastien Tixeuil. Parameterized verification of algorithms for oblivious robots on a ring. Formal Methods Syst. Des., 56(1):55-89, 2020. Google Scholar
  65. Ichiro Suzuki and Masafumi Yamashita. Distributed Anonymous Mobile Robots: Formation of Geometric Patterns. SIAM Journal of Computing, 28(4):1347-1363, 1999. Google Scholar
  66. Giovanni Viglietta. Rendezvous of two robots with visible bits. In Paola Flocchini, Jie Gao, Evangelos Kranakis, and Friedhelm Meyer auf der Heide, editors, Algorithms for Sensor Systems - 9th International Symposium on Algorithms and Experiments for Sensor Systems, Wireless Networks and Distributed Robotics, ALGOSENSORS 2013, Sophia Antipolis, France, September 5-6, 2013, Revised Selected Papers, volume 8243 of Lecture Notes in Computer Science, pages 291-306. Springer-Verlag, 2013. Google Scholar
  67. Vladimir Voevodsky. An experimental library of formalized mathematics based on the univalent foundations. Mathematical Structures in Computer Science, 25(5):1278-1294, 2015. Google Scholar
  68. Yukiko Yamauchi and Masafumi Yamashita. Randomized Pattern Formation Algorithm for Asynchronous Oblivious Mobile Robots. In Fabian Kuhn, editor, Distributed Computing - 28th International Symposium, (DISC 2014), volume 8784 of Lecture Notes in Computer Science, pages 137-151, Austin, USA, October 2014. Springer-Verlag. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact