[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Parameterized verification of algorithms for oblivious robots on a ring

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

A Preface to the special issue FMCAD 2017 to this article was published on 18 January 2021

Abstract

We study verification problems for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. In particular, we focus in this paper on the model proposed by Suzuki and Yamashita of anonymous robots evolving in a discrete space with a finite number of locations (here, a ring). A large number of algorithms have been proposed working for rings whose size is not a priori fixed and can be hence considered as a parameter. Handmade correctness proofs of these algorithms have been shown to be error-prone, and recent attention had been given to the application of formal methods to automatically prove those. Our work is the first to study the verification problem of such algorithms in the parameterized case. We show that safety and reachability problems are undecidable for robots evolving asynchronously. On the positive side, we show that safety properties are decidable in the synchronous case, as well as in the asynchronous case for a particular class of algorithms. Several other properties of the protocol can be decided as well. Decision procedures rely on an encoding in Presburger arithmetics formulae that can be verified by an SMT-solver. Feasibility of our approach is demonstrated by the encoding of several case studies.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

References

  1. Auger C, Bouzid Z, Courtieu P, Tixeuil S, Urbain X (2013) Certified impossibility results for byzantine-tolerant mobile robots. In: Proceedings of SSS’13, volume 8255 of LNCS. Springer, Berlin, pp 178–186

  2. Balabonski T, Delga A, Rieg L, Tixeuil S, Urbain X (2016) Synchronous gathering without multiplicity detection: a certified algorithm. In: Proceedings of SSS’16, volume 10083 of LNCS. Springer, Berlin, pp 7–19

  3. Bérard B, Courtieu P, Millet L, Potop-Butucaru M, Rieg L, Sznajder N, Tixeuil S, Urbain X (2015) Formal methods for mobile robots: current results and open problems. Int J Inf Soc 7(3):101–114

    Google Scholar 

  4. Bérard B, Lafourcade P, Millet L, Potop-Butucaru M, Thierry-Mieg Y, Tixeuil S (2016) Formal verification of mobile robot protocols. Distrib Comput 29:459–587

    Article  MathSciNet  Google Scholar 

  5. Blin L, Milani A, Potop-Butucaru M, Tixeuil S (2010) Exclusive perpetual ring exploration without chirality. In: Proceedings of DISC’10, volume 6343 of LNCS. Springer, Berlin, pp 312–327

  6. Bonnet F, Défago X, Petit F, Potop-Butucaru M, Tixeuil S (2014) Discovering and assessing fine-grained metrics in robot networks protocols. In: Proceedings of SRDS’14. IEEE Press, pp 50–59

  7. Borosh I, Treybig L (1976) Bounds on positive integral solutions of linear Diophantine equations. Am Math Soc 55:299–304

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  9. Courtieu P, Rieg L, Tixeuil S, Urbain X (2016) Certified universal gathering in \(\mathbb{R}^{2}\) for oblivious mobile robots. In: Proceedings of DISC’16, volume 9888 of LNCS. Springer, Berlin, pp 187–200

  10. D’Angelo G, Stefano GD, Navarra A, Nisse N, Suchan K (2013) A unified approach for different tasks on rings in robot-based computing systems. In Proceedings of IPDPSW’13. IEEE Press, pp 667–676

  11. de Moura LM, Bjørner N (2008) Z3: an efficient SMT solver. In: TACAS’08, volume 4963 of LNCS. Springer, Berlin, pp 337–340

  12. Devismes S, Lamani A, Petit F, Raymond P, Tixeuil S (2012) Optimal grid exploration by asynchronous oblivious robots. In: Proceedings of SSS’12, volume 7596 of LNCS. Springer, Berlin, pp 64–76

  13. Doan HTT, Bonnet F, Ogata K (2016) Model checking of a mobile robots perpetual exploration algorithm. In Proceedings of SOFL+MSVL, Revised Selected Papers, volume 10189 of LNCS, pp 201–219

  14. Flocchini P, Ilcinkas D, Pelc A, Santoro N (2013) Computing without communicating: ring exploration by asynchronous oblivious robots. Algorithmica 65(3):562–583

    Article  MathSciNet  Google Scholar 

  15. Flocchini P, Prencipe G, Santoro N (2012) Distributed computing by oblivious mobile robots. Synt. Lect. Distr. Comp. Th. Morgan & Claypool Publishers, San Rafael

    Google Scholar 

  16. Kranakis E, Krizanc D, Markou E (2010) The mobile agent rendezvous problem in the ring. Synt. Lect. Distr. Comp. Th. Morgan & Claypool Publishers, San Rafael

    Google Scholar 

  17. Mayr R (2003) Undecidable problems in unreliable computations. Theor Comput Sci 297(1–3):337–354

    Article  MathSciNet  Google Scholar 

  18. Millet L, Potop-Butucaru M, Sznajder N, Tixeuil S (2014) On the synthesis of mobile robots algorithms: the case of ring gathering. In: Proceedings of SSS’14, volume 8756 of LNCS. Springer, Berlin, pp 237–251

  19. Minsky ML (1967) Computation: finite and infinite machines. Prentice-Hall Inc, Upper Saddle River

    MATH  Google Scholar 

  20. Rubin S, Zuleger F, Murano A, Aminof B (2015) Verification of asynchronous mobile-robots in partially-known environments. In: Proceedings of PRIMA’15, volume 9387 of LNCS. Springer, Berlin, pp 185–200

  21. Sangnier A, Sznajder N, Potop-Butucaru M, Tixeuil S (2017) Parameterized verification of algorithms for oblivious robots on a ring. In: FMCAD’17. IEEE, pp 212–219

  22. SMT-LIB: The satisfiability modulo theory library. http://smtlib.cs.uiowa.edu/

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

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRIF - Univ Paris Diderot, Paris, France

    Arnaud Sangnier

  2. Sorbonne Universités, UPMC Univ Paris 06, UMR 7606, LIP6, 75005, Paris, France

    Nathalie Sznajder, Maria Potop-Butucaru & Sébastien Tixeuil

Authors
  1. Arnaud Sangnier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nathalie Sznajder
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Maria Potop-Butucaru
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Sébastien Tixeuil
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Arnaud Sangnier.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This work has been partly supported by the ANR research program ANR FREDDA (ANR-17-CE40-0013).

Appendix: Models for the algorithm with three robots

Appendix: Models for the algorithm with three robots

See Figs. 6, 7, 8, 9, 10 and 11.

Fig. 6
figure 6

Correct model for the algorithm with 3 robots

Full size image
Fig. 7
figure 7

Buggy model for the algorithm with 3 robots

Full size image
Fig. 8
figure 8

Model for the algorithm with 6 robots on ring of size 11

Full size image
Fig. 9
figure 9

Model for the algorithm with 7 robots on ring of size 12 (part I)

Full size image
Fig. 10
figure 10

Model for the algorithm with 7 robots on ring of size 12 (part II)

Full size image
Fig. 11
figure 11

Extract of the SMT-LIB code to check the absence of collision in the algorithm with 3 robots

Full size image

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Sangnier, A., Sznajder, N., Potop-Butucaru, M. et al. Parameterized verification of algorithms for oblivious robots on a ring. Form Methods Syst Des 56, 55–89 (2020). https://doi.org/10.1007/s10703-019-00335-y

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-019-00335-y

Keywords

Search

Navigation