Skip to main content
SpringerLink
Log in
Book cover

International Conference on Networked Systems

NETYS 2019: Networked Systems pp 93–109Cite as

Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCCN,volume 11704))

Abstract

Oblivious Mobile Robots have been studied both in continuous Euclidean spaces, and discrete spaces (that is, graphs). However the obtained literature forms distinct sets of results for the two settings. In our view, the continuous model reflects well the physicality of robots operating in some real environment, while the discrete model reflects well the digital nature of autonomous robots, whose sensors and computing capabilities are inherently finite.

We explore the possibility of bridging results between the two models. Our approach is certified using the Coq proof assistant and the Pactole framework, which we extend to the most general asynchronous model without compromising its genericity. Our extended framework is then used to formally prove the equivalence between atomic moves in a discrete space (the classical “robots on graphs” model) and non-atomic moves in a continuous unidimensional space when robot vision sensors are discrete (robots move in straigth lines between positions, but their observations are at source and destination positions only), irrespective of the problem being solved. Our effort consolidates the integration between the model, the problem specification, and its proof that is advocated by the Pactole framework.

A preliminary brief announcement of this work appears in SSS 2018 [2].

This work was partially supported by Project CoPRAH of the Fédération Informatique de Lyon, and the CNRS peps ins2i project DiDASCaL.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Notes

  1. 1.

    https://pactole.liris.cnrs.fr.

References

  1. Auger, C., Bouzid, Z., Courtieu, P., Tixeuil, S., Urbain, X.: Certified impossibility results for byzantine-tolerant mobile robots. In: Higashino, T., Katayama, Y., Masuzawa, T., Potop-Butucaru, M., Yamashita, M. (eds.) SSS 2013. LNCS, vol. 8255, pp. 178–190. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03089-0_13

    Chapter  Google Scholar 

  2. Balabonski, T., Courtieu, P., Pelle, R., Rieg, L., Tixeuil, S., Urbain, X.: Brief announcement continuous vs. discrete asynchronous moves: a certified approach for mobile robots. In: Izumi, T., Kuznetsov, P. (eds.) SSS 2018. LNCS, vol. 11201, pp. 404–408. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03232-6_29

    Chapter  Google Scholar 

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

  4. Balabonski, T., Pelle, R., Rieg, L., Tixeuil, S.: A foundational framework for certified impossibility results with mobile robots on graphs. In: Bellavista, P., Garg, V.K., (eds.) Proceedings of the 19th International Conference on Distributed Computing and Networking, ICDCN 2018, Varanasi, India, 4–7 January 2018, pp. 5:1–5:10. ACM (2018)

    Google Scholar 

  5. Baldoni, R., Bonnet, F., Milani, A., Raynal, M.: Anonymous graph exploration without collision by mobile robots. Inf. Process. Lett. 109(2), 98–103 (2008)

    Article  MathSciNet  Google Scholar 

  6. Bérard, B., et al.: Formal methods for mobile robots: current results and open problems. Int. J. Inform. Soc. 7(3), 101–114 (2015). Invited Paper

    Google Scholar 

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

  8. Blin, L., Burman, J., Nisse, N.: Exclusive graph searching. Algorithmica 77(3), 942–969 (2017)

    Article  MathSciNet  Google Scholar 

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

  10. Bonnet, F., Défago, X., Petit, F., Potop-Butucaru, M., Tixeuil, S.: Discovering and assessing fine-grained metrics in robot networks protocols. In 33rd IEEE International Symposium on Reliable Distributed Systems Workshops, SRDS Workshops 2014, Nara, Japan, 6–9 October 2014, pp. 50–59. IEEE (2014)

    Google Scholar 

  11. Bonnet, F., Milani, A., Potop-Butucaru, M., Tixeuil, S.: Asynchronous exclusive perpetual grid exploration without sense of direction. In: Fernàndez Anta, A., Lipari, G., Roy, M. (eds.) OPODIS 2011. LNCS, vol. 7109, pp. 251–265. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25873-2_18

    Chapter  Google Scholar 

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

  13. Bouzid, Z., Dolev, S., Potop-Butucaru, M., Tixeuil, S.: RoboCast: asynchronous communication in robot networks. In: Lu, C., Masuzawa, T., Mosbah, M. (eds.) OPODIS 2010. LNCS, vol. 6490, pp. 16–31. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17653-1_2

    Chapter  Google Scholar 

  14. Caron, G., Mouaddib, E.M., Marchand, É.: 3D model based tracking for omnidirectional vision: a new spherical approach. Robot. Auton. Syst. 60(8), 1056–1068 (2012)

    Article  Google Scholar 

  15. Chalopin, J., Flocchini, P., Mans, B., Santoro, N.: Network exploration by silent and oblivious robots. In: Thilikos, D.M. (ed.) WG 2010. LNCS, vol. 6410, pp. 208–219. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16926-7_20

    Chapter  Google Scholar 

  16. Cieliebak, M., Flocchini, P., Prencipe, G., Santoro, N.: Distributed computing by mobile robots: gathering. SIAM J. Comput. 41(4), 829–879 (2012)

    Article  MathSciNet  Google Scholar 

  17. Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Impossibility of gathering, a certification. Inf. Process. Lett. 115, 447–452 (2015)

    Article  MathSciNet  Google Scholar 

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

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

  20. D’Angelo, G., Stefano, G.D., 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 

  21. Devismes, S., Lamani, A., Petit, F., Raymond, P., Tixeuil, S.: Optimal grid exploration by asynchronous oblivious robots. In: Richa, A.W., Scheideler, C. (eds.) SSS 2012. LNCS, vol. 7596, pp. 64–76. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33536-5_7

    Chapter  Google Scholar 

  22. Devismes, S., Lamani, A., Petit, F., Tixeuil, S.: Optimal torus exploration by oblivious robots. In: Bouajjani, A., Fauconnier, H. (eds.) NETYS 2015. LNCS, vol. 9466, pp. 183–199. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26850-7_13

    Chapter  Google Scholar 

  23. Devismes, S., Petit, F., Tixeuil, S.: Optimal probabilistic ring exploration by semi-synchronous oblivious robots. Theoret. Comput. Sci. 498, 10–27 (2013)

    Article  MathSciNet  Google Scholar 

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

  25. Doan, H.T.T., Bonnet, F., Ogata, K.: Model checking of robot gathering. In: Aspnes, J., Felber, P. (edS.) Principles of Distributed Systems - 21th International Conference (OPODIS 2017), Leibniz International Proceedings in Informatics (LIPIcs), Lisbon, Portugal, December 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik

    Google Scholar 

  26. Flocchini, P., Ilcinkas, D., Pelc, A., Santoro, N.: Remembering without memory: tree exploration by asynchronous oblivious robots. Theoret. Comput. Sci. 411(14–15), 1583–1598 (2010)

    Article  MathSciNet  Google Scholar 

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

  28. Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, California (2012)

    Book  Google Scholar 

  29. Flocchini, P., Prencipe, G., Santoro, N., Widmayer, P.: Arbitrary pattern formation by asynchronous, anonymous, oblivious robots. Theoret. Comput. Sci. 407(1–3), 412–447 (2008)

    Article  MathSciNet  Google Scholar 

  30. Fujinaga, N., Yamauchi, Y., Kijima, S., Yamashita, M.: Asynchronous pattern formation by anonymous oblivious mobile robots. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol. 7611, pp. 312–325. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33651-5_22

    Chapter  Google Scholar 

  31. Izumi, T., Bouzid, Z., Tixeuil, S., Wada, K.: Brief announcement: the BG-simulation for Byzantine mobile robots. In: Peleg, D. (ed.) DISC 2011. LNCS, vol. 6950, pp. 330–331. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24100-0_32

    Chapter  Google Scholar 

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

  33. Kamei, S., Lamani, A., Ooshita, F., Tixeuil, S.: Asynchronous mobile robot gathering from symmetric configurations without global multiplicity detection. In: Kosowski, A., Yamashita, M. (eds.) SIROCCO 2011. LNCS, vol. 6796, pp. 150–161. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22212-2_14

    Chapter  Google Scholar 

  34. Kamei, S., Lamani, A., Ooshita, F., Tixeuil, S.: Gathering an even number of robots in an odd ring without global multiplicity detection. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 542–553. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32589-2_48

    Chapter  MATH  Google Scholar 

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

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

  37. Prencipe, G.: Impossibility of gathering by a set of autonomous mobile robots. Theoret. Comput. Sci. 384(2–3), 222–231 (2007)

    Article  MathSciNet  Google Scholar 

  38. Aminof, B., Murano, A., Rubin, S., Zuleger, F.: Verification of asynchronous mobile-robots in partially-known environments. In: Chen, Q., Torroni, P., Villata, S., Hsu, J., Omicini, A. (eds.) PRIMA 2015. LNCS (LNAI), vol. 9387, pp. 185–200. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25524-8_12

    Chapter  Google Scholar 

  39. Sangnier, A., Sznajder, N., Potop-Butucaru, M., Tixeuil, S.: Parameterized verification of algorithms for oblivious robots on a ring. In: Formal Methods in Computer Aided Design, Vienna, Austria, October 2017

    Google Scholar 

  40. Suzuki, I., Yamashita, M.: Distributed anonymous mobile robots: formation of geometric patterns. SIAM J. Comput. 28(4), 1347–1363 (1999)

    Article  MathSciNet  Google Scholar 

  41. Tomita, Y., Yamauchi, Y., Kijima, S., Yamashita, M.: Plane formation by synchronous mobile robots without chirality. In: Aspnes, J., Bessani, A., Felber, P., Leitão, J. (eds.) 21st International Conference on Principles of Distributed Systems, OPODIS 2017. LIPIcs, vol. 95, Lisbon, Portugal, 18–20 December 2017, pp. 13:1–13:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)

    Google Scholar 

  42. Yamashita, M., Suzuki, I.: Characterizing geometric patterns formable by oblivious anonymous mobile robots. Theoret. Comput. Sci. 411(26–28), 2433–2453 (2010)

    Article  MathSciNet  Google Scholar 

  43. Yamauchi, Y., Uehara, T., Kijima, S., Yamashita, M.: Plane formation by synchronous mobile robots in the three-dimensional Euclidean space. J. ACM 64(3), 16:1–16:43 (2017)

    Article  MathSciNet  Google Scholar 

  44. Yamauchi, Y., Uehara, T., Yamashita, T.: Brief announcement: pattern formation problem for synchronous mobile robots in the three dimensional euclidean space. In: Giakkoupis, G. (ed.) Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing, PODC 2016, Chicago, IL, USA, 25–28 July 2016, pp. 447–449. ACM (2016)

    Google Scholar 

  45. Yamauchi, Y., Yamashita, M.: Pattern formation by mobile robots with limited visibility. In: Moscibroda, T., Rescigno, A.A. (eds.) SIROCCO 2013. LNCS, vol. 8179, pp. 201–212. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03578-9_17

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LRI, CNRS UMR 8623, Université Paris-Sud, Université Paris-Saclay, Orsay, France

    Thibaut Balabonski & Robin Pelle

  2. CÉDRIC – Conservatoire national des arts et métiers, Paris, France

    Pierre Courtieu

  3. Université Grenoble Alpes, Grenoble INP, VERIMAG, 38401, Saint Martin d’Hères, France

    Lionel Rieg

  4. Sorbonne Université, CNRS, LIP6, 75005, Paris, France

    Sébastien Tixeuil

  5. Université Claude Bernard Lyon-1, LIRIS CNRS UMR 5205, Université de Lyon, Lyon, France

    Xavier Urbain

Authors
  1. Thibaut Balabonski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pierre Courtieu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Robin Pelle
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Lionel Rieg
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Sébastien Tixeuil
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Xavier Urbain
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Xavier Urbain .

Editor information

Editors and Affiliations

  1. Uppsala University, Uppsala, Uppsala Län, Sweden

    Mohamed Faouzi Atig

  2. Augusta University, Augusta, GA, USA

    Alexander A. Schwarzmann

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

Balabonski, T., Courtieu, P., Pelle, R., Rieg, L., Tixeuil, S., Urbain, X. (2019). Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. In: Atig, M., Schwarzmann, A. (eds) Networked Systems. NETYS 2019. Lecture Notes in Computer Science(), vol 11704. Springer, Cham. https://doi.org/10.1007/978-3-030-31277-0_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-31277-0_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-31276-3

  • Online ISBN: 978-3-030-31277-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation