Brief Announcement: Model Checking Rendezvous Algorithms for Robots with Lights in Euclidean Space

Authors Xavier Défago , Adam Heriban, Sébastien Tixeuil , Koichi Wada

Thumbnail PDF


  • Filesize: 298 kB
  • 3 pages

Document Identifiers

Author Details

Xavier Défago
  • School of Computing, Tokyo Institute of Technology, Japan
Adam Heriban
  • Sorbonne Université, CNRS, LIP6, Paris, France
Sébastien Tixeuil
  • Sorbonne Université, CNRS, LIP6, Paris, France
Koichi Wada
  • Faculty of Science and Engineering, Hosei University, Tokyo, Japan

Cite AsGet BibTex

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 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 41:1-41:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


This announces the first successful attempt at using model-checking techniques to verify the correctness of self-stabilizing distributed algorithms for robots evolving in a continuous environment. The study focuses on the problem of rendezvous of two robots with lights and presents a generic verification model for the SPIN model checker. It will be presented in full at an upcoming venue.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed algorithms
  • Theory of computation → Verification by model checking
  • Computer systems organization → Robotic autonomy
  • Theory of computation → Self-organization
  • Autonomous mobile robots
  • Rendezvous
  • Lights
  • Model Checking


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


  1. S. Das, P. Flocchini, G. Prencipe, N. Santoro, and M. Yamashita. Autonomous mobile robots with lights. Theor. Comput. Sci., 609:171-184, 2016. URL:
  2. X. Défago, A. Heriban, S. Tixeuil, and K. Wada. Using Model Checking to Formally Verify Rendezvous Algorithms for Robots with Lights in Euclidean Space. CoRR abs/1907.09871, arXiv, July 2019. URL:
  3. P. Flocchini, G. Prencipe, N. Santoro, and P. Widmayer. Gathering of asynchronous robots with limited visibility. Theor. Comput. Sci., 337(1-3):147-168, 2005. URL:
  4. P. Flocchini, N. Santoro, G. Viglietta, and M. Yamashita. Rendezvous with constant memory. Theor. Comput. Sci., 621:57-72, 2016. URL:
  5. A. Heriban, X. Défago, and S. Tixeuil. Optimally Gathering Two Robots. In Proc. ICDCN, pages 3:1-3:10, January 2018. URL:
  6. G. Holzmann. The SPIN Model Checker: Primer & Reference Manual. Addison-Wesley, 2004. Google Scholar
  7. T. Okumura, K. Wada, and X. Défago. Optimal Rendezvous ℒ-Algorithms for Asynchronous Mobile Robots with External-Lights. In Proc. OPODIS, pages 24:1-16, December 2018. URL:
  8. T. Okumura, K. Wada, and Y. Katayama. Brief Announcement: Optimal Asynchronous Rendezvous for Mobile Robots with Lights. In Proc. SSS, pages 484-488, November 2017. URL:
  9. I. Suzuki and M. Yamashita. Distributed Anonymous Mobile Robots: Formation of Geometric Patterns. SIAM J. Comput., 28(4):1347-1363, 1999. URL:
  10. G. Viglietta. Rendezvous of Two Robots with Visible Bits. In Proc. ALGOSENSORS, pages 291-306, September 2013. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail