An Environment for Specifying and Model Checking Mobile Ring Robot Algorithms

  • Ha Thi Thu DoanEmail author
  • Adrián Riesco
  • Kazuhiro Ogata
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11914)


An environment for specifying and model checking mobile robot algorithms on rings (or mobile ring robot algorithms) is proposed. We have developed the Maude Ring Specification Enviaude RSE), a specification environment that explicitly supports ring-shaped networks. Maude RSE is implemented on top of Maude, a rewriting logic-based specification language. The underlying key behind the tool is pattern matching between ring patterns and ring instances, called “ring pattern matching.” Because rings are not commonly available data structures in any existing specification language, we encode ring patterns as sets of sequence patterns and simulate ring pattern matching by pattern matching between sets of sequence patterns and sequence instances, which is proven correct and transparent to Maude RSE users. The advantages of Maude RSE are demonstrated by case studies analyzing exploration and gathering algorithms.


Distributed mobile robot system Ring discrete model Specification environment Formal verification Model checking 


  1. 1.
    Balabonski, T., Delga, A., Rieg, L., Tixeuil, S., Urbain, X.: Synchronous gathering without multiplicity detection: a certified algorithm. In: Bonakdarpour, B., Petit, F. (eds.) SSS 2016. LNCS, vol. 10083, pp. 7–19. Springer, Cham (2016). Scholar
  2. 2.
    Barnat, J., Brim, L., Češka, M., Ročkai, P.: Divine: parallel distributed model checker. In: Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology. IEEE (2010)Google Scholar
  3. 3.
    Bérard, B., Lafourcade, P., Millet, L., Potop-Butucaru, M., Thierry-Mieg, Y., Tixeuil, S.: Formal verification of mobile robot protocols. Distrib. Comput. 29(6), 459–487 (2016)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Blin, L., Milani, A., Potop-Butucaru, M., Tixeuil, S.: Exclusive perpetual ring exploration without chirality. In: Lynch, N.A., Shvartsman, A.A. (eds.) DISC 2010. LNCS, vol. 6343, pp. 312–327. Springer, Heidelberg (2010). Scholar
  5. 5.
    Bonnet, F., Potop-Butucaru, M., Tixeuil, S.: Asynchronous gathering in rings with 4 robots. In: Mitton, N., Loscri, V., Mouradian, A. (eds.) ADHOC-NOW 2016. LNCS, vol. 9724, pp. 311–324. Springer, Cham (2016). Scholar
  6. 6.
    Bournat, M., Dubois, S., Petit, F.: Computability of perpetual exploration in highly dynamic rings. In: IEEE 37th International Conference on Distributed Computing Systems, pp. 794–804 (2017)Google Scholar
  7. 7.
    Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). Scholar
  8. 8.
    Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Certified universal gathering in \(\mathbb{R} ^2\) for oblivious mobile robots. In: Gavoille, C., Ilcinkas, D. (eds.) DISC 2016. LNCS, vol. 9888, pp. 187–200. Springer, Heidelberg (2016). Scholar
  9. 9.
    D’Angelo, G., Di Stefano, G., Navarra, A.: Gathering on rings under the look-compute-move model. Distrib. Comput. 27, 255–285 (2014)MathSciNetCrossRefGoogle Scholar
  10. 10.
    D’Angelo, G., Di Stefano, G., Navarra, A., Nisse, N., Suchan, K.: Computing on rings by oblivious robots: a unified approach for different tasks. Algorithmica 72(4), 1055–1096 (2015)MathSciNetCrossRefGoogle Scholar
  11. 11.
    D’Angelo, G., Navarra, A., Nisse, N.: A unified approach for gathering and exclusive searching on rings under weak assumptions. Distrib. Comput. 30(1), 17–48 (2017)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Datta, A.K., Lamani, A., Larmore, L.L., Petit, F.: Enabling ring exploration with myopic oblivious robots. In: IEEE International Parallel and Distributed Processing Symposium Workshop, Hyderabad, pp. 490–499 (2015)Google Scholar
  13. 13.
    Devismes, S.: Optimal exploration of small rings. In: Proceedings of the Third International Workshop on Reliability, Availability, and Security, pp. 91–96 (2010)Google Scholar
  14. 14.
    Devismes, S., Petit, F., Tixeuil, S.: Optimal probabilistic ring exploration by semi-synchronous oblivious robots. Theor. Comput. Sci. 498, 10–27 (2013). Scholar
  15. 15.
    Doan, H.T.T., Bonnet, F., Ogata, K.: Model checking of a mobile robots perpetual exploration algorithm. In: Liu, S., Duan, Z., Tian, C., Nagoya, F. (eds.) SOFL+MSVL 2016. LNCS, vol. 10189, pp. 201–219. Springer, Cham (2017). Scholar
  16. 16.
    Doan, H.T.T., Bonnet, F., Ogata, K.: Model checking of robot gathering. In: Proceedings of The 21th Conference on Principles of Distributed Systems, pp. 12:1–12:16 (2017)Google Scholar
  17. 17.
    Doan, H.T.T., Bonnet, F., Ogata, K.: 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, pp. 1586–1596 (2017)Google Scholar
  18. 18.
    Flocchini, P., Ilcinkas, D., Pelc, A., Santoro, N.: Computing without communicating: ring exploration by asynchronous oblivious robots. Algorithmica 65(3), 562–583 (2013)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Flocchini, P., Kranakis, E., Krizanc, D., Santoro, N., Sawchuk, C.: Multiple mobile agent rendezvous in a ring. In: Farach-Colton, M. (ed.) LATIN 2004. LNCS, vol. 2976, pp. 599–608. Springer, Heidelberg (2004). Scholar
  20. 20.
    Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Morgan & Claypool Publishers (2012)Google Scholar
  21. 21.
    Grov, J., Ölveczky, P.C.: Formal modeling and analysis of Google’s megastore in real-time maude. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 494–519. Springer, Heidelberg (2014). Scholar
  22. 22.
    Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2004)Google Scholar
  23. 23.
    Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2004)CrossRefGoogle Scholar
  24. 24.
    Izumi, T., Izumi, T., Kamei, S., Ooshita, F.: Mobile robots gathering algorithm with local weak multiplicity in rings. In: Patt-Shamir, B., Ekim, T. (eds.) SIROCCO 2010. LNCS, vol. 6058, pp. 101–113. Springer, Heidelberg (2010). Scholar
  25. 25.
    Kawamura, A., Kobayashi, Y.: Fence patrolling by mobile agents with distinct speeds. Distrib. Comput. 28(2), 147–154 (2015)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Klasing, R., Markou, E., Pelc, A.: Gathering asynchronous oblivious mobile robots in a ring. Theor. Comput. Sci. 390(1), 27–39 (2008)MathSciNetCrossRefGoogle Scholar
  27. 27.
    Lamani, A., Potop-Butucaru, M.G., Tixeuil, S.: Optimal deterministic ring exploration with oblivious asynchronous robots. In: Patt-Shamir, B., Ekim, T. (eds.) SIROCCO 2010. LNCS, vol. 6058, pp. 183–196. Springer, Heidelberg (2010). Scholar
  28. 28.
    Liu, S., Ölveczky, P.C., Wang, Q., Meseguer, J.: Formal modeling and analysis of the walter transactional data store. In: Rusu, V. (ed.) WRLA 2018. LNCS, vol. 11152, pp. 136–152. Springer, Cham (2018). site/siliunobi/walterCrossRefGoogle Scholar
  29. 29.
    Our Maude source files.
  30. 30.
    Millet, L., Potop-Butucaru, M., Sznajder, N., Tixeuil, S.: On the synthesis of mobile robots algorithms: the case of ring gathering. In: Felber, P., Garg, V. (eds.) SSS 2014. LNCS, vol. 8756, pp. 237–251. Springer, Cham (2014). Scholar
  31. 31.
    Ooshita, F., Tixeuil, S.: Ring exploration with myopic luminous robots. In: Izumi, T., Kuznetsov, P. (eds.) SSS 2018. LNCS, vol. 11201, pp. 301–316. Springer, Cham (2018). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Japan Advanced Institute of Science and TechnologyIshikawaJapan
  2. 2.Universidad Complutense de MadridMadridSpain

Personalised recommendations