Document Open Access Logo

The Complexity of Nested Reset Counter Systems

Authors A. R. Balasubramanian , Franzisco Schmidt

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.11.pdf
  • Filesize: 1.01 MB
  • 28 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Problems, reductions and completeness
  • Theory of computation → Models of computation
Keywords
  • Nested counter systems
  • Fast-growing hierarchy
  • Complexity

Metrics

Abstract

Nested counter systems (NCS) are a generalization of counter systems to higher-order counters. Here, a higher-order counter is allowed to have other (lower-order) counters as elements, instead of just a number. Such systems can be viewed as working on trees, where the height of the tree naturally corresponds to the highest order counter that the system is working with. It is known that the coverability problem for NCS, which asks if a given final tree can be covered from a given initial tree, is 𝐅_ε₀-complete. Here 𝐅_ε₀ is a class in the fast-growing hierarchy of complexity classes.
In this paper, we consider an extension of NCS called nested reset counter systems (NRCS) that extends NCS with resets. We show that coverability for NRCS over order-k counters is 𝐅_{Ω_k}-complete where Ω_k is the tower of height k of the ω ordinal. This gives the first natural hierarchy of complete problems for all of these classes. Furthermore, to prove our upper bounds, we also develop length function theorems for any fixed amount of applications of the multiset operation on finite sets.
As an application of our results, we improve existing upper bounds for various problems from XML processing, graph transformation systems, π-calculus, logic and parameterized verification. Furthermore, using our completeness results for k-NRCS, we also prove 𝐅_{Ω_k}-completeness of the considered problems from the realms of parameterized verification and logic, for all k.

Cite As Get BibTex

A. R. Balasubramanian and Franzisco Schmidt. The Complexity of Nested Reset Counter Systems. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 11:1-11:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.11

Author Details

A. R. Balasubramanian
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Franzisco Schmidt
  • Technical University of Munich (TUM), Germany

Funding

  • Balasubramanian, A. R.: This research was sponsored in part by the Deutsche Forschungsgemeinschaft project https://gepris.dfg.de/gepris/projekt/389792660 TRR 248–CPEC.

References

  1. Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 313-321. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/LICS.1996.561359.
  2. Roberto M. Amadio and Charles Meyssonnier. On decidability of the control reachability problem in the asynchronous pi-calculus. Nord. J. Comput., 9(1):70-101, 2002. Google Scholar
  3. A. R. Balasubramanian. Complexity of coverability in bounded path broadcast networks. In Mikolaj Bojanczyk and Chandra Chekuri, editors, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021, Virtual Conference, December 15-17, 2021, volume 213 of LIPIcs, pages 35:1-35:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2021.35.
  4. 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, volume 243 of LIPIcs, pages 17:1-17:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.17.
  5. A. R. Balasubramanian, Timo Lang, and Revantha Ramanayake. Decidability and complexity in weakening and contraction hypersequent substructural logics. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470733.
  6. 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.
  7. Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. Approaching the coverability problem continuously. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 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 9636 of Lecture Notes in Computer Science, pages 480-496. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_28.
  8. 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.
  9. Michael Blondin, Christoph Haase, and Philip Offtermatt. Directed reachability for infinite-state systems. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, volume 12652 of Lecture Notes in Computer Science, pages 3-23. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_1.
  10. 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.
  11. 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.
  12. Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Parameterized verification of ad hoc networks. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 313-327. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_22.
  13. Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. URL: https://doi.org/10.1145/1507244.1507246.
  14. Guoli Ding. Subgraphs and well-quasi-ordering. Journal of Graph Theory, 16(5):489-502, 1992. URL: https://doi.org/10.1002/JGT.3190160509.
  15. 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, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, volume 1427 of Lecture Notes in Computer Science, pages 516-520. Springer, 1998. URL: https://doi.org/10.1007/BFB0028773.
  16. Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 352-359. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782630.
  17. 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.
  18. 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, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 269-278. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.39.
  19. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
  20. Patrick C. Fischer, Albert R. Meyer, and Arnold L. Rosenberg. Counter machines and counter languages. Math. Syst. Theory, 2(3):265-283, 1968. URL: https://doi.org/10.1007/BF01694011.
  21. 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.
  22. Blaise Genest, Anca Muscholl, Olivier Serre, and Marc Zeitoun. Tree pattern rewriting systems. In Sung Deok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee, and Mahesh Viswanathan, editors, Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings, volume 5311 of Lecture Notes in Computer Science, pages 332-346. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-88387-6_29.
  23. Vitor Greati and Revantha Ramanayake. Deducibility in the full Lambek calculus with weakening is HAck-complete. In Agata Ciabattoni, David Gabelaia, and Igor Sedlár, editors, Advances in Modal Logic, AiML 2024, Prague, Czech Republic, August 19-23, 2024, pages 401-422. College Publications, 2024. URL: http://www.aiml.net/volumes/volume15/19-GreatiRamanayake.pdf.
  24. Vitor Greati and Revantha Ramanayake. Tight length theorems for multiset extensions of higman’s lemma. Theor. Comput. Sci., 1057:115546, 2025. URL: https://doi.org/10.1016/J.TCS.2025.115546.
  25. 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.
  26. 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.
  27. Serge Haddad, Sylvain Schmitz, and Philippe Schnoebelen. The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 355-364. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/LICS.2012.46.
  28. Matthew Hague. Senescent ground tree rewrite systems. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, Vienna, Austria, July 14-18, 2014, pages 48:1-48:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603112.
  29. Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(1):326-336, 1952. Google Scholar
  30. Petr Jancar and Sylvain Schmitz. Bisimulation equivalence of first-order grammars is ACKERMANN-complete. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-12. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785848.
  31. Barbara König and Jan Stückrath. Well-structured graph transformation systems. Inf. Comput., 252:71-94, 2017. URL: https://doi.org/10.1016/J.IC.2016.03.005.
  32. Slawomir Lasota and Igor Walukiewicz. Alternating timed automata. ACM Trans. Comput. Log., 9(2):10:1-10:27, 2008. URL: https://doi.org/10.1145/1342991.1342994.
  33. Ranko Lazic, Joël Ouaknine, and James Worrell. Zeno, Hercules, and the Hydra: Safety metric temporal logic is ackermann-complete. ACM Trans. Comput. Log., 17(3):16, 2016. URL: https://doi.org/10.1145/2874774.
  34. Ranko Lazic and Sylvain Schmitz. Nonelementary complexities for branching VASS, MELL, and extensions. ACM Trans. Comput. Log., 16(3):20:1-20:30, 2015. URL: https://doi.org/10.1145/2733375.
  35. Ranko Lazic and Sylvain Schmitz. The complexity of coverability in ν-Petri nets. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 467-476. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933593.
  36. 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.
  37. 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.
  38. 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.
  39. Roland Meyer. On boundedness in depth in the pi-calculus. In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, and C.-H. Luke Ong, editors, Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy, volume 273 of IFIP, pages 477-489. Springer, 2008. URL: https://doi.org/10.1007/978-0-387-09680-3_32.
  40. Balasubramanian Ayikudi Ramachandrakumar. Computational Complexity of Verifying Parameterized Systems. PhD thesis, Technical University of Munich, Germany, 2024. URL: https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20240417-1714488-1-4.
  41. Fernando Rosa-Velardo. Ordinal recursive complexity of unordered data nets. Inf. Comput., 254:41-58, 2017. URL: https://doi.org/10.1016/J.IC.2017.02.002.
  42. Sylvain Schmitz. Complexity bounds for ordinal-based termination - (invited talk). 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 1-19. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11439-2_1.
  43. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Trans. Comput. Theory, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  44. Sylvain Schmitz. The parametric complexity of lossy counter machines. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, Patras, Greece, July 9-12, 2019, volume 132 of LIPIcs, pages 129:1-129:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.129.
  45. Sylvain Schmitz and Philippe Schnoebelen. Multiply-recursive upper bounds with Higman’s lemma. In Luca Aceto, Monika Henzinger, and Jirí Sgall, editors, Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, volume 6756 of Lecture Notes in Computer Science, pages 441-452. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22012-8_35.
  46. Sylvain Schmitz and Philippe Schnoebelen. Multiply-recursive upper bounds with Higman’s lemma. CoRR, abs/1103.4399, 2011. URL: https://arxiv.org/abs/1103.4399.
  47. 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.
  48. Philippe Schnoebelen. Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In Petr Hlinený and Antonín Kucera, editors, Mathematical Foundations of Computer Science 2010, 35th International Symposium, MFCS 2010, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6281 of Lecture Notes in Computer Science, pages 616-628. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15155-2_54.
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