Skip to main content
SpringerLink
Log in

An Environment for Specifying and Model Checking Mobile Ring Robot Algorithms

  • Conference paper
  • First Online:
Stabilization, Safety, and Security of Distributed Systems (SSS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11914))

  • 449 Accesses

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.

This research was partially supported by JSPS KAKENHI Grant Number JP19H04082, Comunidad de Madrid project BLOQUES-CM (S2018/TCS-4339) co-funded by EIE Funds of the European Union, and MINECO project TRACES (TIN2015-67522-C3-3-R).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In the actual specification, we need an operator enclosing the sequence, such as {_} to avoid rewriting sub-sequences. However, to make the explanation as close as possible to mathematical description, we omit it here.

References

  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_2

    Chapter  Google Scholar 

  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. 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)

    Article  MathSciNet  Google Scholar 

  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_29

    Chapter  Google Scholar 

  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_22

    Chapter  Google Scholar 

  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. 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-1

    Book  MATH  Google Scholar 

  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_14

    Chapter  Google Scholar 

  9. D’Angelo, G., Di Stefano, G., Navarra, A.: Gathering on rings under the look-compute-move model. Distrib. Comput. 27, 255–285 (2014)

    Article  MathSciNet  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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. 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. 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.031

    Article  MathSciNet  MATH  Google Scholar 

  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_12

    Chapter  Google Scholar 

  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. 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. Flocchini, P., Ilcinkas, D., Pelc, A., Santoro, N.: Computing without communicating: ring exploration by asynchronous oblivious robots. Algorithmica 65(3), 562–583 (2013)

    Article  MathSciNet  Google Scholar 

  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_62

    Chapter  Google Scholar 

  20. Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Morgan & Claypool Publishers (2012)

    Google Scholar 

  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_25

    Chapter  Google Scholar 

  22. Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2004)

    Google Scholar 

  23. Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2004)

    Book  Google Scholar 

  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_9

    Chapter  Google Scholar 

  25. Kawamura, A., Kobayashi, Y.: Fence patrolling by mobile agents with distinct speeds. Distrib. Comput. 28(2), 147–154 (2015)

    Article  MathSciNet  Google Scholar 

  26. Klasing, R., Markou, E., Pelc, A.: Gathering asynchronous oblivious mobile robots in a ring. Theor. Comput. Sci. 390(1), 27–39 (2008)

    Article  MathSciNet  Google Scholar 

  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_15

    Chapter  Google Scholar 

  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/walter

    Chapter  Google Scholar 

  29. Our Maude source files. https://goo.gl/6AnwHE

  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_17

    Chapter  Google Scholar 

  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_20

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Japan Advanced Institute of Science and Technology, Ishikawa, Japan

    Ha Thi Thu Doan & Kazuhiro Ogata

  2. Universidad Complutense de Madrid, Madrid, Spain

    Adrián Riesco

Authors
  1. Ha Thi Thu Doan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Adrián Riesco
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kazuhiro Ogata
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ha Thi Thu Doan .

Editor information

Editors and Affiliations

  1. ETH Zurich, Zurich, Switzerland

    Mohsen Ghaffari

  2. Kent State University, Kent, OH, USA

    Mikhail Nesterenko

  3. Sorbonne University, Paris, France

    Sébastien Tixeuil

  4. CEA LIST, Gif-sur-Yvette, France

    Sara Tucci

  5. Kyushu University, Fukuoka, Japan

    Yukiko Yamauchi

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Doan, H.T.T., Riesco, A., Ogata, K. (2019). An Environment for Specifying and Model Checking Mobile Ring Robot Algorithms. In: Ghaffari, M., Nesterenko, M., Tixeuil, S., Tucci, S., Yamauchi, Y. (eds) Stabilization, Safety, and Security of Distributed Systems. SSS 2019. Lecture Notes in Computer Science(), vol 11914. Springer, Cham. https://doi.org/10.1007/978-3-030-34992-9_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-34992-9_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-34991-2

  • Online ISBN: 978-3-030-34992-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation