Document Open Access Logo

On Parameterized Verification over Tree Topologies

Authors Romain Delpy , Anca Muscholl , Grégoire Sutre

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.31.pdf
  • Filesize: 1.24 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Concurrent programming
  • Parameterized verification

Metrics

Abstract

Parameterized verification of finite-state processes with rendez-vous synchronization is notoriously undecidable when processes are linearly ordered. In this paper we study two kinds of bounds under which we determine the complexity of safety checking over tree topologies. When bounding the depth we obtain that the complexity is related to the fast growing hierarchy. Our second bound limits the alternations between upwards and downwards synchronizations in the tree (phases), and occurs naturally in many concrete settings. If we fix the number of phases then the complexity of safety checking is EXPSPACE complete, and if the number of phases is part of the input it is 2EXPSPACE complete (both for arbitrary depth).

Cite As Get BibTex

Romain Delpy, Anca Muscholl, and Grégoire Sutre. On Parameterized Verification over Tree Topologies. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.31

Author Details

Romain Delpy
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France
Anca Muscholl
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France
Grégoire Sutre
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France

Funding

This work was (partially) supported by the grant ANR-23-CE48-0005 of the French National Research Agency ANR (project PaVeDyS).

References

  1. Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, Frédéric Haziza, and Ahmed Rezine. Parameterized tree systems. In Kenji Suzuki, Teruo Higashino, Keiichi Yasumoto, and Khaled El-Fakih, editors, Formal Techniques for Networked and Distributed Systems - FORTE 2008, 28th IFIP WG 6.1 International Conference, Tokyo, Japan, June 10-13, 2008, Proceedings, Lecture Notes in Computer Science, pages 69-83. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-68855-6_5.
  2. Parosh Aziz Abdulla, Bengt Jonsson, Pritha Mahata, and Julien d'Orso. Regular tree model checking. In Ed Brinksma and Kim Guldstrand Larsen, editors, Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, Lecture Notes in Computer Science, pages 555-568. Springer, 2002. URL: https://doi.org/10.1007/3-540-45657-0_47.
  3. Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, and Helmut Veith. Parameterized model checking of rendezvous systems. Distributed Comput., 31(3):187-222, 2018. URL: https://doi.org/10.1007/S00446-017-0302-6.
  4. Krzysztof R. Apt and Dexter Kozen. Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett., 22(6):307-309, 1986. URL: https://doi.org/10.1016/0020-0190(86)90071-2.
  5. A. R. Balasubramanian. Complexity of coverability in depth-bounded processes. In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory, CONCUR 2022, Warsaw, Poland, September 12-16, 2022, LIPIcs, pages 17:1-17:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.17.
  6. A. R. Balasubramanian, Javier Esparza, and Mikhail A. Raskin. Finding cut-offs in leaderless rendez-vous protocols is easy. Log. Methods Comput. Sci., 19(4), 2023. URL: https://doi.org/10.46298/LMCS-19(4:2)2023.
  7. A. R. Balasubramanian and Franzisco Schmidt. The complexity of nested reset counter systems. In Claudia Faggian and Joost-Pieter Katoen, editors, 41st Annual Symposium on Logic in Computer Science, LICS 2026, Lisbon, Portugal, July 20-23, 2026, volume 380 of LIPIcs, pages 11:1-11:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. URL: https://doi.org/10.4230/LIPICS.LICS.2026.11.
  8. Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. The complexity of bounded context switching with dynamic thread creation. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, Saarbrücken, Germany (Virtual Conference), July 8-11, 2020, volume 168 of LIPIcs, pages 111:1-111:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.111.
  9. Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. URL: https://doi.org/10.2200/S00658ED1V01Y201508DCT013.
  10. Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, and Tomás Vojnar. Abstract regular (tree) model checking. Int. J. Softw. Tools Technol. Transf., 14(2):167-191, 2012. URL: https://doi.org/10.1007/S10009-011-0205-Y.
  11. Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis, and Christoph Welzel. Structural invariants for the verification of systems with parameterized architectures. In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I, Lecture Notes in Computer Science, pages 228-246. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45190-5_13.
  12. Marius Bozga and Radu Iosif. Specification and safety verification of parametric hierarchical distributed systems. In Gwen Salaün and Anton Wijs, editors, Formal Aspects of Component Software - 17th International Conference, FACS 2021, Virtual Event, October 28-29, 2021, Proceedings, Lecture Notes in Computer Science, pages 95-114. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-90636-8_6.
  13. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323-342, 1983. URL: https://doi.org/10.1145/322374.322380.
  14. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is Ackermann-complete. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229-1240. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  15. Normann Decker and Daniel Thoma. On freeze LTL with ordered attributes, 2016. URL: https://arxiv.org/abs/1504.06355.
  16. 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.
  17. Romain Delpy, Anca Muscholl, and Grégoire Sutre. On parameterized verification over tree topologies, 2026. URL: https://arxiv.org/abs/2606.27172.
  18. Allen E. Emerson and Kedar S. Namjoshi. On reasoning about rings. International Journal of Foundations of Computer Science, 14(04):527-549, 2003. URL: https://doi.org/10.1142/S0129054103001881.
  19. Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In Ernst W. Mayr and Natacha Portier, editors, 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014, Lyon, France, March 5-8, 2014, LIPIcs, pages 1-10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.STACS.2014.1.
  20. Steven M. German and Prasad A. Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675-735, 1992. URL: https://doi.org/10.1145/146637.146681.
  21. Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Phase-bounded broadcast networks over topologies of communication. In Rupak Majumdar and Alexandra Silva, editors, 35th International Conference on Concurrency Theory, CONCUR 2024, Calgary, Canada, September 9-13, 2024, LIPIcs, pages 26:1-26:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2024.26.
  22. Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, and Elad Shahar. Symbolic model checking with rich assertional languages. Theor. Comput. Sci., 256(1-2):93-112, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00103-1.
  23. Marvin Künnemann, Filip Mazowiecki, Lia Schütze, Henry Sinclair-Banks, and Karol Wegrzycki. Coverability in VASS revisited: Improving Rackoff’s bounds to obtain conditional optimality. J. ACM, 72(5):33:1-33:27, 2025. URL: https://doi.org/10.1145/3762178.
  24. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241-1252. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  25. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  26. Richard J. Lipton. The reachability problem requires exponential space. Technical Report 62, Yale University, 1976. URL: http://cpsc.yale.edu/sites/default/files/files/tr63.pdf.
  27. Irina A. Lomazova and Philippe Schnoebelen. Some decidability results for nested petri nets. In Dines Bjørner, Manfred Broy, and Alexandre V. Zamulin, editors, Perspectives of System Informatics, Third International Andrei Ershov Memorial Conference, PSI'99, Akademgorodok, Novosibirsk, Russia, July 6-9, 1999, Proceedings, volume 1755 of Lecture Notes in Computer Science, pages 208-220. Springer, 1999. URL: https://doi.org/10.1007/3-540-46562-6_18.
  28. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223-231, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
  29. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Transactions on Computation Theory (TOCT), 8(1):1-36, 2016. URL: https://doi.org/10.1145/2858784.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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