Advertisement

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)

Abstract

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.

Keywords

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

References

  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).  https://doi.org/10.1007/978-3-319-49259-9_2CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-15763-9_29CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-40509-4_22CrossRefGoogle 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).  https://doi.org/10.1007/978-3-540-71999-1CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-662-53426-7_14CrossRefGoogle 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).  https://doi.org/10.1016/j.tcs.2013.05.031MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-319-57708-1_12CrossRefGoogle 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).  https://doi.org/10.1007/978-3-540-24698-5_62CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-54624-2_25CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-13284-1_9CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-13284-1_15CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-99840-4_8. https://sites.google.com/ site/siliunobi/walterCrossRefGoogle Scholar
  29. 29.
    Our Maude source files. https://goo.gl/6AnwHE
  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).  https://doi.org/10.1007/978-3-319-11764-5_17CrossRefGoogle 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).  https://doi.org/10.1007/978-3-030-03232-6_20CrossRefGoogle 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