Document Open Access Logo

Reachability in Fixed Dimension Vector Addition Systems with States

Authors Wojciech Czerwiński , Sławomir Lasota , Ranko Lazić , Jérôme Leroux, Filip Mazowiecki

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.48.pdf
  • Filesize: 0.63 MB
  • 21 pages

Document Identifiers

Author Details

Wojciech Czerwiński
  • University of Warsaw, Poland
Sławomir Lasota
  • University of Warsaw, Poland
Ranko Lazić
  • University of Warwick, Coventry, UK
Jérôme Leroux
  • CNRS & University of Bordeaux, France
Filip Mazowiecki
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany

Funding

  • Czerwiński, Wojciech: Supported by the ERC grant LIPA, agreement no. 683080.
  • Lasota, Sławomir: Supported by the NCN grant 2017 B/ST6/02093.
  • Lazić, Ranko: Supported by EPSRC grant EP/P020992/1.
  • Leroux, Jérôme: Supported by ANR grant ANR-17-CE40-0028.

Acknowledgements

We thank Matthias Englert for inspiring conversations.

Cite AsGet BibTex

Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki. Reachability in Fixed Dimension Vector Addition Systems with States. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 48:1-48:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.48

Abstract

The reachability problem is a central decision problem in verification of vector addition systems with states (VASS). In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We obtain three main results for VASS of fixed dimension. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional ones. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest runs. The smallest dimension for which this was previously known is 14.

Subject Classification

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

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. 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. 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 LICS, pages 32-43. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.14.
  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. 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.
  6. 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.
  7. 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.
  8. 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.
  9. Hubert Comon and Véronique Cortier. Flatness is not a weakness. In CSL, volume 1862 of LNCS, pages 262-276. Springer, 2000. URL: https://doi.org/10.1007/3-540-44622-2_17.
  10. 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.
  11. Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. In STOC, pages 24-33. ACM, 2019. URL: https://doi.org/10.1145/3313276.3316369.
  12. 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.
  13. 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.
  14. Matthias Englert, Ranko Lazić, and Patrick Totzke. Reachability in two-dimensional unary vector addition systems with states is NL-complete. In LICS, pages 477-484. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933577.
  15. 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.
  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. Laurent Fribourg and Hans Olsén. Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In CONCUR, volume 1243 of LNCS, pages 213-227. Springer, 1997. URL: https://doi.org/10.1007/3-540-63141-0_15.
  18. 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.
  19. 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.
  20. 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.
  21. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in succinct and parametric one-counter automata. In CONCUR, volume 5710 of LNCS, pages 369-383. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_25.
  22. Michel Hack. The recursive equivalence of the reachability problem and the liveness problem for Petri nets and vector addition systems. In SWAT, pages 156-164. IEEE Computer Society, 1974. URL: https://doi.org/10.1109/SWAT.1974.28.
  23. 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.
  24. 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.
  25. 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.
  26. 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.
  27. 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.
  28. 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.
  29. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In LICS, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  30. Jérôme Leroux and Grégoire Sutre. On flatness for 2-dimensional vector addition systems with states. In CONCUR, volume 3170 of LNCS, pages 402-416. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-28644-8_26.
  31. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In ICALP, Part II, volume 9135 of LNCS, pages 324-336. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_26.
  32. 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.
  33. 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.
  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. 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.
  37. Carl Adam Petri. Kommunikation mit Automaten. PhD thesis, Universität Hamburg, 1962. URL: http://edoc.sub.uni-hamburg.de/informatik/volltexte/2011/160/.
  38. 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.
  39. Louis E. Rosier and Hsu-Chun Yen. A multiparameter analysis of the boundedness problem for vector addition systems. J. Comput. Syst. Sci., 32(1):105-135, 1986. URL: https://doi.org/10.1016/0022-0000(86)90006-1.
  40. 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.
  41. Juliusz Straszyński. Complexity of the reachability problem for pushdown Petri nets. Master’s thesis, University of Warsaw, Faculty of Mathematics, Informatics, and Mechanics, 2017. URL: https://apd.uw.edu.pl/diplomas/155747.
  42. Leslie G. Valiant and Mike Paterson. Deterministic one-counter automata. J. Comput. Syst. Sci., 10(3):340-350, 1975. URL: https://doi.org/10.1016/S0022-0000(75)80005-5.
  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