LIPIcs.DISC.2019.41.pdf
- Filesize: 298 kB
- 3 pages
Document
Brief Announcement: Model Checking Rendezvous Algorithms for Robots with Lights in Euclidean Space
Authors
Xavier Défago 
,
Sébastien Tixeuil ,
Koichi Wada
-
Part of:
Volume:
33rd International Symposium on Distributed Computing (DISC 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Symposium on Distributed Computing (DISC) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2019-10-08
File
Document Identifiers
Author Details
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)
https://doi.org/10.4230/LIPIcs.DISC.2019.41
https://doi.org/10.4230/LIPIcs.DISC.2019.41
Abstract
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
Keywords
- Autonomous mobile robots
- Rendezvous
- Lights
- Model Checking
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- S. Das, P. Flocchini, G. Prencipe, N. Santoro, and M. Yamashita. Autonomous mobile robots with lights. Theor. Comput. Sci., 609:171-184, 2016. URL: https://doi.org/10.1016/j.tcs.2015.09.018.
- 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: http://arxiv.org/abs/1907.09871.
- 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: https://doi.org/10.1016/j.tcs.2005.01.001.
- P. Flocchini, N. Santoro, G. Viglietta, and M. Yamashita. Rendezvous with constant memory. Theor. Comput. Sci., 621:57-72, 2016. URL: https://doi.org/10.1016/j.tcs.2016.01.025.
- A. Heriban, X. Défago, and S. Tixeuil. Optimally Gathering Two Robots. In Proc. ICDCN, pages 3:1-3:10, January 2018. URL: https://doi.org/10.1145/3154273.3154323.
-
G. Holzmann. The SPIN Model Checker: Primer & Reference Manual. Addison-Wesley, 2004.
- 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: https://doi.org/10.4230/LIPIcs.OPODIS.2018.24.
- 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: https://doi.org/10.1007/978-3-319-69084-1_36.
- I. Suzuki and M. Yamashita. Distributed Anonymous Mobile Robots: Formation of Geometric Patterns. SIAM J. Comput., 28(4):1347-1363, 1999. URL: https://doi.org/10.1137/S009753979628292X.
- G. Viglietta. Rendezvous of Two Robots with Visible Bits. In Proc. ALGOSENSORS, pages 291-306, September 2013. URL: https://doi.org/10.1007/978-3-642-45346-5_21.