Document Open Access Logo

Model Checking of Robot Gathering

Authors Ha Thi Thu Doan, François Bonnet, Kazuhiro Ogata

PDF
Thumbnail PDF

File

LIPIcs.OPODIS.2017.12.pdf
  • Filesize: 0.58 MB
  • 16 pages

Document Identifiers

Author Details

Ha Thi Thu Doan
François Bonnet
Kazuhiro Ogata

Cite As Get BibTex

Ha Thi Thu Doan, François Bonnet, and Kazuhiro Ogata. Model Checking of Robot Gathering. In 21st International Conference on Principles of Distributed Systems (OPODIS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 95, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.OPODIS.2017.12

Abstract

Recent advances in distributed computing highlight models and algorithms for autonomous mo- bile robots that self-organize and cooperate together in order to solve a global objective. As results, a large number of algorithms have been proposed. These algorithms are given together with proofs to assess their correctness. However, those proofs are informal, which are error prone. This paper presents our study on formal verification of mobile robot algorithms. We first propose a formal model for mobile robot algorithms on anonymous ring shape network under multiplicity and asynchrony assumptions. We specify this formal model in Maude, a specification and pro- gramming language based on rewriting logic. We then use its model checker to formally verify an algorithm for robot gathering problem on ring enjoys some desired properties. As the result of the model checking, counterexamples have been found. We detect the sources of some unforeseen design errors. We, furthermore, give our interpretations of these errors.

Subject Classification

Keywords
  • Mobile Robot
  • Robot Gathering
  • Formal Verification
  • Model Checking
  • Maude

Metrics

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

References

  1. Our Maude source files. URL: https://figshare.com/s/3c0a6fdb0e4fec3b0b08.
  2. T. Balabonski, A. Delga, L. Rieg, S. Tixeuil, and X. Urbain. Synchronous gathering without multiplicity detection: A certified algorithm. In Proceedings of the 18th International Symposium on Stabilization, Safety, and Security of Distributed Systems, volume 10083 of LNCS, pages 7-19. Springer, 2016. Google Scholar
  3. B. Bérard, P. Lafourcade, L. Millet, M. Potop-Butucaru, Y. Thierry-Mieg, and S. Tixeuil. Formal verification of mobile robot protocols. Distributed Computing, 29(6):459-487, 2016. Google Scholar
  4. L. Blin, A. Milani, M. Potop-Butucaru, and S. Tixeuil. Exclusive perpetual ring exploration without chirality. In Proceedings of the 24th International Symposium on Distributed Computing, volume 6343 of LNCS, pages 312-327. Springer, 2010. Google Scholar
  5. F. Bonnet, M. Potop-Butucaru, and S. Tixeuil. Asynchronous gathering in rings with 4 robots. In Proceedings of the 15th International Conference on Ad-hoc, Mobile, and Wireless Networks, volume 9724 of LNCS, pages 311-324. Springer, 2016. Google Scholar
  6. M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott. All About Maude, volume 4350 of LNCS. Springer, 2007. Google Scholar
  7. P Courtieu, L. Rieg, S Tixeuil, and X. Urbain. Certified universal gathering in r² for oblivious mobile robots. In Proceedings of the 30th International Symposium on Distributed Computing, volume 9888 of LNCS, pages 187-200. Springer, 2016. Google Scholar
  8. G. D'Angelo, G. Di Stefano, and A. Navarra. Gathering on rings under the look-compute-move model. Distributed Computing, 27:255-285, March 2014. Google Scholar
  9. G. D'Angelo, G. Di Stefano, A. Navarra, N. Nisse, and K. Suchan. Computing on rings by oblivious robots: A unified approach for different tasks. Algorithmica, 72(4):1055-1096, 2015. Google Scholar
  10. G. D'Angelo, A. Navarra, and N. Nisse. A unified approach for gathering and exclusive searching on rings under weak assumptions. Distributed Computing, 28(1):17-48, 2017. Google Scholar
  11. H. T. T. Doan, F. Bonnet, and K. Ogata. Model checking of a mobile robots perpetual exploration algorithm. In Proceedings of the 6th International Workshop on Structured Object-Oriented Formal Language and Method (SOFL+MSVL 2016), volume 10189 of LNCS, pages 201-219. Springer, 2017. Google Scholar
  12. H. T. T. Doan, F. Bonnet, and K. Ogata. Specifying a distributed snapshot algorithm as a meta-program and model checking it at meta-level. In Proceedings of The 37th IEEE International Conference on Distributed Computing Systems (ICDCS 2017), pages 1586-1596, 2017. Google Scholar
  13. H. T. T. Doan, W. Zhang, M. Zhang, and K. Ogata. Model checking chandy-lamport distributed snapshot algorithm revisited. In Proceedings of the 2nd International Symposium on Dependable Computing and Internet of Things, pages 7-19, 2015. Google Scholar
  14. P. Flocchini, D. Ilcinkas, A. Pelc, and N. Santoro. Computing without communicating: Ring exploration by asynchronous oblivious robots. Algorithmica, 65(3):562-583, 2013. Google Scholar
  15. P. Flocchini, G. Prencipe, and N. Santoro. Distributed Computing by Oblivious Mobile Robots. Morgan & Claypool Publishers, 2012. Google Scholar
  16. Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004. Google Scholar
  17. I. Konnov, H. Veith, and J. Widder. On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Information and Computation, 252:95-109, 2017. Google Scholar
  18. I. Suzuki and M. Yamashita. Distributed anonymous mobile robots: Formation of geometric patterns. SIAM Journal on Computing, 28(4):1347-1363, 1999. Google Scholar
  19. T. Tsuchiya and A. Schiper. Verification of consensus algorithms using satisfiability solving. Distributed Computing, 23(5):341-358, 2011. 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 About DROPS Imprint Privacy Contact