Document Open Access Logo

Improved Ackermannian Lower Bound for the Petri Nets Reachability Problem

Author Sławomir Lasota

PDF
Thumbnail PDF

File

LIPIcs.STACS.2022.46.pdf
  • Filesize: 0.79 MB
  • 15 pages

Document Identifiers

Author Details

Sławomir Lasota
  • University of Warsaw, Poland

Funding

  • Lasota, Sławomir: Supported by the ERC project ‘Lipa’ within the EU Horizon 2020 research and innovation programme (No. 683080).

Cite As Get BibTex

Sławomir Lasota. Improved Ackermannian Lower Bound for the Petri Nets Reachability Problem. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 46:1-46:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.STACS.2022.46

Abstract

Petri nets, equivalently presentable as vector addition systems with states, are an established model of concurrency with widespread applications. The reachability problem, where we ask whether from a given initial configuration there exists a sequence of valid execution steps reaching a given final configuration, is the central algorithmic problem for this model. The complexity of the problem has remained, until recently, one of the hardest open questions in verification of concurrent systems. A first upper bound has been provided only in 2015 by Leroux and Schmitz, then refined by the same authors to non-primitive recursive Ackermannian upper bound in 2019. The exponential space lower bound, shown by Lipton already in 1976, remained the only known for over 40 years until a breakthrough non-elementary lower bound by Czerwiński, Lasota, Lazic, Leroux and Mazowiecki in 2019. Finally, a matching Ackermannian lower bound announced this year by Czerwiński and Orlikowski, and independently by Leroux, established the complexity of the problem.
Our primary contribution is an improvement of the former construction, making it conceptually simpler and more direct. On the way we improve the lower bound for vector addition systems with states in fixed dimension (or, equivalently, Petri nets with fixed number of places): while Czerwiński and Orlikowski prove F_k-hardness (hardness for kth level in Grzegorczyk Hierarchy) in dimension 6k, our simplified construction yields F_k-hardness already in dimension 3k+2.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Verification by model checking
  • Theory of computation → Logic and verification
Keywords
  • Petri nets
  • reachability problem
  • vector addition systems

Metrics

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

Related Versions

References

  1. David Angeli, Patrick De Leenheer, and Eduardo D. Sontag. Persistence results for chemical reaction networks with time-dependent kinetics and no global conservation laws. SIAM Journal of Applied Mathematics, 71(1):128-146, 2011. Google Scholar
  2. Paolo Baldan, Nicoletta Cocco, Andrea Marin, and Marta Simeoni. Petri nets for modelling metabolic pathways: a survey. Natural Computing, 9(4):955-989, 2010. URL: https://doi.org/10.1007/s11047-010-9180-6.
  3. Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie. Reachability in two-dimensional vector addition systems with states is PSPACE-complete. In Proc. LICS, pages 32-43, 2015. Google Scholar
  4. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27:1-27:26, 2011. URL: https://doi.org/10.1145/1970398.1970403.
  5. Ahmed Bouajjani and Michael Emmi. Analysis of recursively parallel programs. ACM Trans. Program. Lang. Syst., 35(3):10:1-10:49, 2013. URL: https://doi.org/10.1145/2518188.
  6. Frank P. Burns, Albert Koelmans, and Alexandre Yakovlev. WCET analysis of superscalar processors using simulation with coloured Petri nets. Real-Time Systems, 18(2/3):275-288, 2000. URL: https://doi.org/10.1023/A:1008101416758.
  7. Thomas Colcombet and Amaldev Manuel. Generalized data automata and fixpoint logic. In FSTTCS, volume 29 of LIPIcs, pages 267-278. Schloss Dagstuhl, 2014. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2014.267.
  8. Stefano Crespi-Reghizzi and Dino Mandrioli. Petri nets and Szilard languages. Information and Control, 33(2):177-192, 1977. URL: https://doi.org/10.1016/S0019-9958(77)90558-7.
  9. Wojciech Czerwiński, Sławomir 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, Proc. STOC 2019, pages 24-33. ACM, 2019. Google Scholar
  10. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. J. ACM, 68(1):7:1-7:28, 2021. URL: https://doi.org/10.1145/3422822.
  11. Wojciech Czerwinski, Slawomir Lasota, and Łukasz Orlikowski. Improved lower bounds for reachability in vector addition systems. In Proc. ICALP, volume 198 of LIPIcs, pages 128:1-128:15, 2021. Google Scholar
  12. Wojciech Czerwiński and Łukasz Orlikowski. Reachability in vector addition systems is Ackermann-complete. In Proc. FOCS 2021, 2021. To appear. Google Scholar
  13. Normann Decker, Peter Habermehl, Martin Leucker, and Daniel Thoma. Ordered navigation on multi-attributed data words. In Proc. CONCUR, volume 8704 of LNCS, pages 497-511. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44584-6_34.
  14. Stéphane Demri, Diego Figueira, and M. Praveen. Reasoning about data repetitions with counter systems. Logical Methods in Computer Science, 12(3), 2016. URL: https://doi.org/10.2168/LMCS-12(3:1)2016.
  15. Matthias Englert, Ranko Lazić, and Patrick Totzke. Reachability in two-dimensional unary vector addition systems with states is NL-complete. In Proc. LICS, pages 477-484. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933577.
  16. Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of population protocols. Acta Inf., 54(2):191-215, 2017. URL: https://doi.org/10.1007/s00236-016-0272-3.
  17. Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst., 34(1):6:1-6:48, 2012. URL: https://doi.org/10.1145/2160910.2160915.
  18. Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675-735, 1992. URL: https://doi.org/10.1145/146637.146681.
  19. Sheila A. Greibach. Remarks on blind and partially blind one-way multicounter machines. Theor. Comput. Sci., 7:311-324, 1978. URL: https://doi.org/10.1016/0304-3975(78)90020-8.
  20. Piotr Hofman and Sławomir Lasota. Linear equations with ordered data. In Proc. CONCUR, volume 118 of LIPIcs, pages 24:1-24:17. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.24.
  21. John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci., 8:135-159, 1979. URL: https://doi.org/10.1016/0304-3975(79)90041-0.
  22. Alexander Kaiser, Daniel Kroening, and Thomas Wahl. A widening approach to multithreaded program verification. ACM Trans. Program. Lang. Syst., 36(4):14:1-14:29, 2014. URL: https://doi.org/10.1145/2629608.
  23. Max I. Kanovich. Petri nets, Horn programs, linear logic and vector games. Ann. Pure Appl. Logic, 75(1-2):107-135, 1995. URL: https://doi.org/10.1016/0168-0072(94)00060-G.
  24. Richard M. Karp and Raymond E. Miller. Parallel program schemata. J. Comput. Syst. Sci., 3(2):147-195, 1969. URL: https://doi.org/10.1016/S0022-0000(69)80011-5.
  25. S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In Proc. STOC, pages 267-281. ACM, 1982. URL: https://doi.org/10.1145/800070.802201.
  26. Jean-Luc Lambert. A structure to decide reachability in Petri nets. Theor. Comput. Sci., 99(1):79-104, 1992. URL: https://doi.org/10.1016/0304-3975(92)90173-D.
  27. Hélène Leroux, David Andreu, and Karen Godary-Dejean. Handling exceptions in Petri net-based digital architecture: From formalism to implementation on FPGAs. IEEE Trans. Industrial Informatics, 11(4):897-906, 2015. Google Scholar
  28. Jérôme Leroux. The general vector addition system reachability problem by Presburger inductive invariants. Logical Methods in Computer Science, 6(3), 2010. URL: https://doi.org/10.2168/LMCS-6(3:22)2010.
  29. Jérôme Leroux. Vector addition system reachability problem: a short self-contained proof. In POPL, pages 307-316. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926421.
  30. Jérôme Leroux. Vector addition systems reachability problem (A simpler solution). In Turing-100, volume 10 of EPiC Series in Computing, pages 214-228. EasyChair, 2012. URL: http://www.easychair.org/publications/paper/106497, URL: https://doi.org/10.29007/bnx2.
  31. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. In Proc. FOCS 2021, 2021. To appear. Google Scholar
  32. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive, 2021. URL: http://arxiv.org/abs/2104.12695.
  33. Jérôme Leroux and Sylvain Schmitz. Demystifying reachability in vector addition systems. In Proc. LICS, pages 56-67, 2015. Google Scholar
  34. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In Proc. LICS, pages 1-13. IEEE, 2019. Google Scholar
  35. Yuliang Li, Alin Deutsch, and Victor Vianu. VERIFAS: A practical verifier for artifact systems. PVLDB, 11(3):283-296, 2017. URL: https://doi.org/10.14778/3157794.3157798.
  36. 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.
  37. Martin H. Löb and Stanley S. Wainer. Hierarchies of number-theoretic functions. I. Archiv für mathematische Logik und Grundlagenforschung, 13(1-2):39-51, 1970. URL: https://doi.org/10.1007/BF01967649.
  38. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. In STOC, pages 238-246. ACM, 1981. URL: https://doi.org/10.1145/800076.802477.
  39. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. SIAM J. Comput., 13(3):441-460, 1984. URL: https://doi.org/10.1137/0213029.
  40. Roland Meyer. A theory of structural stationarity in the pi-calculus. Acta Inf., 46(2):87-137, 2009. URL: https://doi.org/10.1007/s00236-009-0091-x.
  41. Carl Adam Petri. Kommunikation mit Automaten. PhD thesis, Universität Hamburg, 1962. URL: http://edoc.sub.uni-hamburg.de/informatik/volltexte/2011/160/.
  42. George S. Sacerdote and Richard L. Tenney. The decidability of the reachability problem for vector addition systems (preliminary version). In STOC, pages 61-76. ACM, 1977. URL: https://doi.org/10.1145/800105.803396.
  43. Sylvain Schmitz. Complexity hierarchies beyond elementary. TOCT, 8(1):3:1-3:36, 2016. Google Scholar
  44. Sylvain Schmitz. The complexity of reachability in vector addition systems. SIGLOG News, 3(1):4-21, 2016. Google Scholar
  45. Wil M. P. van der Aalst. Business process management as the "killer app" for Petri nets. Software and System Modeling, 14(2):685-691, 2015. URL: https://doi.org/10.1007/s10270-014-0424-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 About DROPS Imprint Privacy Contact