Document Open Access Logo

Improved Lower Bounds for Reachability in Vector Addition Systems

Authors Wojciech Czerwiński , Sławomir Lasota , Łukasz Orlikowski

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.128.pdf
  • Filesize: 0.8 MB
  • 15 pages

Document Identifiers

Author Details

Wojciech Czerwiński
  • University of Warsaw, Poland
Sławomir Lasota
  • University of Warsaw, Poland
Łukasz Orlikowski
  • University of Warsaw, Poland

Funding

  • Czerwiński, Wojciech: Supported by the ERC grant LIPA, agreement no. 683080.
  • Lasota, Sławomir: Supported by the NCN grant 2017/27/B/ST6/02093.

Cite AsGet BibTex

Wojciech Czerwiński, Sławomir Lasota, and Łukasz Orlikowski. Improved Lower Bounds for Reachability in Vector Addition Systems. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 128:1-128:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ICALP.2021.128

Abstract

We investigate computational complexity of the reachability problem for vector addition systems (or, equivalently, Petri nets), the central algorithmic problem in verification of concurrent systems. Concerning its complexity, after 40 years of stagnation, a non-elementary lower bound has been shown recently: the problem needs a tower of exponentials of time or space, where the height of tower is linear in the input size. We improve on this lower bound, by increasing the height of tower from linear to exponential. As a side-effect, we obtain better lower bounds for vector addition systems of fixed dimension.

Subject Classification

ACM Subject Classification
  • Theory of computation → Parallel computing models
Keywords
  • Petri nets
  • vector addition systems
  • reachability problem

Metrics

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

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. URL: https://doi.org/10.1137/090779401.
  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. 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.
  4. Mikołaj Bojańczyk, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data trees and XML reasoning. J. ACM, 56(3):13:1-13:48, 2009. URL: https://doi.org/10.1145/1516512.1516515.
  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 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, Proc. STOC 2019, pages 24-33. ACM, 2019. Google Scholar
  10. Normann Decker, Peter Habermehl, Martin Leucker, and Daniel Thoma. Ordered navigation on multi-attributed data words. In CONCUR, volume 8704 of LNCS, pages 497-511. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44584-6_34.
  11. 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.
  12. Javier Esparza. Decidability and complexity of Petri net problems - an introduction. In Lectures on Petri Nets I, volume 1491 of LNCS, pages 374-428. Springer, 1998. URL: https://doi.org/10.1007/3-540-65306-6_20.
  13. 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.
  14. Patrick C. Fischer, Albert R. Meyer, and Arnold L. Rosenberg. Counter machines and counter languages. Mathematical Systems Theory, 2(3):265-283, 1968. URL: https://doi.org/10.1007/BF01694011.
  15. 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.
  16. 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.
  17. 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.
  18. Piotr Hofman and Sławomir Lasota. Linear equations with ordered data. In CONCUR, volume 118 of LIPIcs, pages 24:1-24:17. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.24.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In STOC, pages 267-281. ACM, 1982. URL: https://doi.org/10.1145/800070.802201.
  24. 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.
  25. 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. URL: https://doi.org/10.1109/TII.2015.2435696.
  26. 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.
  27. 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.
  28. 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.
  29. Jérôme Leroux and Sylvain Schmitz. Demystifying reachability in vector addition systems. In LICS, pages 56-67. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.16.
  30. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In Proc. LICS 2019, pages 1-13. IEEE, 2019. Google Scholar
  31. Yuliang Li, Alin Deutsch, and Victor Vianu. VERIFAS: A practical verifier for artifact systems. PVLDB, 11(3):283-296, 2017. URL: http://www.vldb.org/pvldb/vol11/p283-li.pdf, URL: https://doi.org/10.14778/3157794.3157798.
  32. 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.
  33. 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.
  34. 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.
  35. 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.
  36. Marvin L. Minsky. Computation: finite and infinite machines. Prentice-Hall, Inc., 1967. URL: https://dl.acm.org/citation.cfm?id=1095587.
  37. Mor Peleg, Daniel L. Rubin, and Russ B. Altman. Research paper: Using Petri net tools to study properties and dynamics of biological systems. JAMIA, 12(2):181-199, 2005. URL: https://doi.org/10.1197/jamia.M1637.
  38. Carl Adam Petri. Kommunikation mit Automaten. PhD thesis, Universität Hamburg, 1962. URL: http://edoc.sub.uni-hamburg.de/informatik/volltexte/2011/160/.
  39. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theor. Comput. Sci., 6:223-231, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
  40. 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.
  41. Sylvain Schmitz. Complexity hierarchies beyond elementary. TOCT, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  42. Sylvain Schmitz. The complexity of reachability in vector addition systems. SIGLOG News, 3(1):4-21, 2016. URL: https://doi.org/10.1145/2893582.2893585.
  43. 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 Imprint Privacy Contact