Document Open Access Logo

Complexity of Coverability in Depth-Bounded Processes

Author A. R. Balasubramanian

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2022.17.pdf
  • Filesize: 0.89 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Problems, reductions and completeness
  • Theory of computation → Distributed computing models
Keywords
  • π-calculus
  • Depth-bounded processes
  • Fast-growing complexity classes

Metrics

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

Abstract

We consider the class of depth-bounded processes in π-calculus. These processes are the most expressive fragment of π-calculus, for which verification problems are known to be decidable. The decidability of the coverability problem for this class has been achieved by means of well-quasi orders. (Meyer, IFIP TCS 2008; Wies, Zufferey and Henzinger, FoSSaCS 2010). However, the precise complexity of this problem has not been known so far, with only a known EXPSPACE-lower bound.
In this paper, we prove that coverability for depth-bounded processes is 𝐅_ε₀-complete, where 𝐅_ε₀ is a class in the fast-growing hierarchy of complexity classes. This solves an open problem mentioned by Haase, Schmitz, and Schnoebelen (LMCS, Vol 10, Issue 4) and also addresses a question raised by Wies, Zufferey and Henzinger (FoSSaCS 2010).

Cite As Get BibTex

A. R. Balasubramanian. Complexity of Coverability in Depth-Bounded Processes. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CONCUR.2022.17

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).

Acknowledgements

I am grateful to the reviewers and Prof. Javier Esparza for their useful comments and suggestions.

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. 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, December 15-17, 2021, Virtual Conference, 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.
  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 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.
  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. Guoli Ding. Subgraphs and well-quasi-ordering. Journal of Graph Theory, 16(5):489-502, 1992. URL: https://doi.org/10.1002/jgt.3190160509.
  10. 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
  11. 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), STACS 2014, March 5-8, 2014, Lyon, France, volume 25 of LIPIcs, pages 1-10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.STACS.2014.1.
  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. 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.
  15. 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.
  16. 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.
  17. 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.
  18. Slawomir Lasota. Improved Ackermannian lower bound for the petri nets reachability problem. In Petra Berenbrink and Benjamin Monmege, editors, 39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022, March 15-18, 2022, Marseille, France (Virtual Conference), volume 219 of LIPIcs, pages 46:1-46:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.STACS.2022.46.
  19. 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.
  20. 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.
  21. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I. Inf. Comput., 100(1):1-40, 1992. URL: https://doi.org/10.1016/0890-5401(92)90008-4.
  22. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, II. Inf. Comput., 100(1):41-77, 1992. URL: https://doi.org/10.1016/0890-5401(92)90009-5.
  23. 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.
  24. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Trans. Comput. Theory, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  25. 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.
  26. 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.
  27. Thomas Wies, Damien Zufferey, and Thomas A. Henzinger. Forward analysis of depth-bounded processes. In C.-H. Luke Ong, editor, Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6014 of Lecture Notes in Computer Science, pages 94-108. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12032-9_8.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact