Document Open Access Logo

Deciding the Existence of Cut-Off in Parameterized Rendez-Vous Networks

Authors Florian Horn, Arnaud Sangnier

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.46.pdf
  • Filesize: 0.58 MB
  • 16 pages

Document Identifiers

Author Details

Florian Horn
  • Université de Paris, IRIF, CNRS, France
Arnaud Sangnier
  • Université de Paris, IRIF, CNRS, France

Funding

Partly supported by ANR FREDDA (ANR-17-CE40-0013).

Cite AsGet BibTex

Florian Horn and Arnaud Sangnier. Deciding the Existence of Cut-Off in Parameterized Rendez-Vous Networks. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 46:1-46:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.46

Abstract

We study networks of processes which all execute the same finite-state protocol and communicate thanks to a rendez-vous mechanism. Given a protocol, we are interested in checking whether there exists a number, called a cut-off, such that in any networks with a bigger number of participants, there is an execution where all the entities end in some final states. We provide decidability and complexity results of this problem under various assumptions, such as absence/presence of a leader or symmetric/asymmetric rendez-vous.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
Keywords
  • Parameterized networks
  • Verification
  • Cut-offs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Holík. Parameterized verification through view abstraction. STTT, 18(5):495-516, 2016. Google Scholar
  2. Benjamin Aminof, Swen Jacobs, Ayrat Khalimov, and Sasha Rubin. Parametrized model checking of token-passing systems. In VMCAI'14, volume 8318 of LNCS, pages 262-281. Springer-Verlag, 2014. Google Scholar
  3. Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, and Helmut Veith. Parameterized model checking of rendezvous systems. Distributed Computing, 31(3):187-222, 2018. Google Scholar
  4. Benjamin Aminof, Sasha Rubin, and Florian Zuleger. On the expressive power of communication primitives in parameterised systems. In LPAR'15, volume 9450 of LNCS, pages 313-328. Springer-Verlag, 2015. Google Scholar
  5. Dana Angluin, James Aspnes, David Eisenstat, and Eric Ruppert. The computational power of population protocols. Distributed Computing, 20(4):279-304, 2007. Google Scholar
  6. Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Reconfiguration and message losses in parameterized broadcast networks. In CONCUR'19, volume 140 of LIPIcs, pages 32:1-32:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  7. Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, Hugo Gimbert, and Adwait Amit Godbole. Controlling a population. Logical Methods in Computer Science, 15(3), 2019. Google Scholar
  8. Michael Blondin, Javier Esparza, and Stefan Jaax. Peregrine: A tool for the analysis of population protocols. In CAV'18, volume 10981 of LNCS, pages 604-611. Springer, 2018. Google Scholar
  9. Michael Blondin, Javier Esparza, and Stefan Jaax. Expressive power of broadcast consensus protocols. In CONCUR'19, volume 140 of LIPIcs, pages 31:1-31:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  10. Benedikt Bollig, Paul Gastin, and Len Schubert. Parameterized verification of communicating automata under context bounds. In RP'14, volume 8762 of LNCS, pages 45-57. Springer-Verlag, 2014. Google Scholar
  11. Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, and Helmut Veith. Verification by network decomposition. In CONCUR'04, volume 3170 of LNCS, pages 276-291. Springer-Verlag, 2004. Google Scholar
  12. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for petri nets is not elementary. In STOC'19, pages 24-33. ACM, 2019. Google Scholar
  13. Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Parameterized verification of ad hoc networks. In CONCUR'10, volume 6269 of LNCS, pages 313-327. Springer-Verlag, 2010. Google Scholar
  14. Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, and Rupak Majumdar. Model checking parameterized asynchronous shared-memory systems. Formal Methods in System Design, 50(2-3):140-167, 2017. Google Scholar
  15. Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In STACS'14, volume 25 of LIPIcs, pages 1-10. Leibniz-Zentrum für Informatik, 2014. Google Scholar
  16. Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In LICS'99, pages 352-359. IEEE Comp. Soc. Press, July 1999. Google Scholar
  17. Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of population protocols. Acta Inf., 54(2):191-215, 2017. Google Scholar
  18. Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV'13, volume 8044 of LNCS, pages 124-140. Springer-Verlag, 2013. Google Scholar
  19. Alain Finkel and Jérôme Leroux. How to compose presburger-accelerations: Applications to broadcast protocols. In FST TCS'02, volume 2556 of LNCS, pages 145-156. Springer, 2002. Google Scholar
  20. Laurent Fribourg. Petri nets, flat languages and linear arithmetic. In WFLP'00, pages 344-365, 2000. Google Scholar
  21. Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675-735, 1992. Google Scholar
  22. Seymour Ginsburg and Edwin H. Spanier. Semigroups, presburger formulas, and languages. Pacific Journal of Mathematics, 16(2):285-296, 1966. Google Scholar
  23. Florian Horn and Arnaud Sangnier. Deciding the existence of cut-off in parameterized rendez-vous networks. CoRR, abs/2007.05789, 2020. URL: http://arxiv.org/abs/2007.05789.
  24. Petr Jancar, Jérôme Leroux, and Grégoire Sutre. Co-finiteness and co-emptiness of reachability sets in vector addition systems with states. In PETRI NETS'18, volume 10877 of LNCS, pages 184-203. Springer, 2018. Google Scholar
  25. Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Dynamic cutoff detection in parameterized concurrent programs. In CAV'10, volume 6174 of LNCS, pages 645-659. Springer, 2010. Google Scholar
  26. Hans Kleine Büning, Theodor Lettmann, and Ernst W. Mayr. Projections of vector addition system reachability sets are semilinear. Theor. Comput. Sci., 64(3):343-350, 1989. Google Scholar
  27. S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In STOC'82, pages 267-281. ACM, 1982. Google Scholar
  28. Jean-Luc Lambert. A structure to decide reachability in petri nets. Theor. Comput. Sci., 99(1):79-104, 1992. Google Scholar
  29. Jérôme Leroux. Vector addition system reachability problem: a short self-contained proof. In POPL'11, pages 307-316. ACM, 2011. Google Scholar
  30. Jérôme Leroux. Presburger vector addition systems. In LICS'13, pages 23-32. IEEE Computer Society, 2013. Google Scholar
  31. Jérôme Leroux. Vector addition system reversible reachability problem. Logical Methods in Computer Science, 9(1), 2013. Google Scholar
  32. Ernst W. Mayr. An algorithm for the general petri net reachability problem. SIAM J. Comput., 13(3):441-460, 1984. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact