Document Open Access Logo

Complexity of Coverability in Bounded Path Broadcast Networks

Author A. R. Balasubramanian

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2021.35.pdf
  • Filesize: 1 MB
  • 16 pages

Document Identifiers

Author Details

A. R. Balasubramanian
  • Technische Universität München, Germany

Funding

  • Balasubramanian, A. R.: Supported by funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS).

Cite AsGet BibTex

A. R. Balasubramanian. Complexity of Coverability in Bounded Path Broadcast Networks. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSTTCS.2021.35

Abstract

Broadcast networks are a formalism of distributed computation that allow one to model networks of identical nodes communicating through message broadcasts over a communication topology that does not change over the course of executions. The parameterized verification problem for these networks amounts to proving correctness of a property for any number of nodes, and on all executions. Dually speaking, this problem asks for the existence of an execution of the broadcast network that violates a given property. One specific instance of parameterized verification is the coverability problem which asks whether there is an execution of the network in which some node reaches a given state of the broadcast protocol. This problem was proven to be undecidable by Delzanno, Sangnier and Zavattaro (CONCUR 2010). In the same paper, the authors also prove that, if we additionally assume that the underlying communication topology has a bound on the longest path, then the coverability problem becomes decidable. In this paper, we provide complexity results for the above problem and prove that the coverability problem for bounded-path topologies is 𝐅_ε₀-complete, where 𝐅_ε₀ is a class in the fast-growing hierarchy of complexity classes. This solves an open problem of Hasse, Schmitz and Schnoebelen (LMCS, Vol 10, Issue 4).

Subject Classification

ACM Subject Classification
  • Theory of computation → Problems, reductions and completeness
  • Theory of computation → Distributed computing models
Keywords
  • Parameterized verification
  • Bounded path networks
  • Fast-growing complexity classes

Metrics

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

References

  1. Sergio Abriola, Santiago Figueira, and Gabriel Senno. Linearizing well quasi-orders and bounding the length of bad sequences. Theor. Comput. Sci., 603:3-22, 2015. URL: https://doi.org/10.1016/j.tcs.2015.07.012.
  2. Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Reconfiguration and message losses in parameterized broadcast networks. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7280.
  3. Michael Blondin. The abcs of petri net reachability relaxations. ACM SIGLOG News, 7(3):29-43, 2020. URL: https://doi.org/10.1145/3436980.3436984.
  4. Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. The logical view on continuous petri nets. ACM Trans. Comput. Log., 18(3):24:1-24:28, 2017. URL: https://doi.org/10.1145/3105908.
  5. Michael Blondin and Christoph Haase. Logics for continuous reachability in petri nets and vector addition systems with states. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005068.
  6. Pierre Chambart and Philippe Schnoebelen. The ordinal recursive complexity of lossy channel systems. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 205-216, 2008. URL: https://doi.org/10.1109/LICS.2008.47.
  7. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for petri nets is not elementary. In Moses Charikar and Edith Cohen, editors, Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019, pages 24-33. ACM, 2019. URL: https://doi.org/10.1145/3313276.3316369.
  8. Normann Decker and Daniel Thoma. On freeze LTL with ordered attributes. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9634 of Lecture Notes in Computer Science, pages 269-284. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_16.
  9. Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Parameterized verification of ad hoc networks. In CONCUR 2010 - Concurrency Theory, 21th International Conference,, pages 313-327, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_22.
  10. Guoli Ding. Subgraphs and well-quasi-ordering. Journal of Graph Theory, 16(5):489-502, 1992. URL: https://doi.org/10.1002/jgt.3190160509.
  11. Jacob Elgaard, Nils Klarlund, and Anders Møller. Mona 1.x: New techniques for ws1s and ws2s. In Alan J. Hu and Moshe Y. Vardi, editors, Computer Aided Verification, pages 516-520, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. Google Scholar
  12. Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, and Filip Niksic. An smt-based approach to coverability analysis. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 603-619. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_40.
  13. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and primitive-recursive bounds with dickson’s lemma. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, pages 269-278, 2011. URL: https://doi.org/10.1109/LICS.2011.39.
  14. Estíbaliz Fraca and Serge Haddad. Complexity analysis of continuous petri nets. Fundam. Informaticae, 137(1):1-28, 2015. URL: https://doi.org/10.3233/FI-2015-1168.
  15. Christoph Haase and Simon Halfon. Integer vector addition systems with states. In Joël Ouaknine, Igor Potapov, and James Worrell, editors, Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings, volume 8762 of Lecture Notes in Computer Science, pages 112-124. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11439-2_9.
  16. Christoph Haase, Sylvain Schmitz, and Philippe Schnoebelen. The power of priority channel systems. Log. Methods Comput. Sci., 10(4), 2014. URL: https://doi.org/10.2168/LMCS-10(4:4)2014.
  17. Albert R. Meyer. Weak monadic second order theory of succesor is not elementary-recursive. In Rohit Parikh, editor, Logic Colloquium, pages 132-154, Berlin, Heidelberg, 1975. Springer Berlin Heidelberg. Google Scholar
  18. Sylvain Schmitz. Complexity bounds for ordinal-based termination - (invited talk). In Reachability Problems - 8th International Workshop, RP 2014, pages 1-19, 2014. URL: https://doi.org/10.1007/978-3-319-11439-2_1.
  19. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Trans. Comput. Theory, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  20. Sylvain Schmitz and Philippe Schnoebelen. Multiply-recursive upper bounds with higman’s lemma. In Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, pages 441-452, 2011. URL: https://doi.org/10.1007/978-3-642-22012-8_35.
  21. Sylvain Schmitz and Philippe Schnoebelen. The power of well-structured systems. In Pedro R. D'Argenio and Hernán C. Melgratti, editors, CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8052 of Lecture Notes in Computer Science, pages 5-24. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40184-8_2.
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