Document Open Access Logo

Monus Semantics in Vector Addition Systems with States

Authors Pascal Baumann , Khushraj Madnani , Filip Mazowiecki , Georg Zetzsche

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.10.pdf
  • Filesize: 0.8 MB
  • 18 pages

Document Identifiers

Author Details

Pascal Baumann
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Khushraj Madnani
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Filip Mazowiecki
  • University of Warsaw, Poland
Georg Zetzsche
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

Funding

  • Mazowiecki, Filip: Supported by the ERC grant INFSYS, agreement no. 950398.

Acknowledgements

The authors are grateful to Wojciech Czerwiński and Sylvain Schmitz for discussions, and to Sylvain Schmitz for suggesting the term 'monus'.

Cite AsGet BibTex

Pascal Baumann, Khushraj Madnani, Filip Mazowiecki, and Georg Zetzsche. Monus Semantics in Vector Addition Systems with States. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.10

Abstract

Vector addition systems with states (VASS) are a popular model for concurrent systems. However, many decision problems have prohibitively high complexity. Therefore, it is sometimes useful to consider overapproximating semantics in which these problems can be decided more efficiently. We study an overapproximation, called monus semantics, that slightly relaxes the semantics of decrements: A key property of a vector addition systems is that in order to decrement a counter, this counter must have a positive value. In contrast, our semantics allows decrements of zero-valued counters: If such a transition is executed, the counter just remains zero. It turns out that if only a subset of transitions is used with monus semantics (and the others with classical semantics), then reachability is undecidable. However, we show that if monus semantics is used throughout, reachability remains decidable. In particular, we show that reachability for VASS with monus semantics is as hard as that of classical VASS (i.e. Ackermann-hard), while the zero-reachability and coverability are easier (i.e. EXPSPACE-complete and NP-complete, respectively). We provide a comprehensive account of the complexity of the general reachability problem, reachability of zero configurations, and coverability under monus semantics. We study these problems in general VASS, two-dimensional VASS, and one-dimensional VASS, with unary and binary counter updates.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
Keywords
  • Vector addition systems
  • Overapproximation
  • Reachability
  • Coverability

Metrics

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

Related Versions

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. Shaull Almagor, Nathann Cohen, Guillermo A. Pérez, Mahsa Shirmohammadi, and James Worrell. Coverability in 1-VASS with Disequality Tests. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 38:1-38:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.38.
  3. Pascal Baumann, Roland Meyer, and Georg Zetzsche. Regular Separability in Büchi VASS. In Petra Berenbrink, Patricia Bouyer, Anuj Dawar, and Mamadou Moustapha Kanté, editors, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023), volume 254 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.STACS.2023.9.
  4. Michael Blondin. The ABCs of Petri net reachability relaxations. ACM SIGLOG News, 7(3), 2020. URL: https://doi.org/10.1145/3436980.3436984.
  5. Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazic, Pierre McKenzie, and Patrick Totzke. The Reachability Problem for Two-Dimensional Vector Addition Systems with States. J. ACM, 68(5):34:1-34:43, 2021. URL: https://doi.org/10.1145/3464794.
  6. Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. Approaching the coverability problem continuously. In Proc. 22^nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 480-496, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_28.
  7. 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.
  8. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. Reachability in fixed dimension vector addition systems with states. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 48:1-48:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.48.
  9. 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.
  10. Wojciech Czerwinski and Lukasz Orlikowski. Lower bounds for the reachability problem in fixed dimensional vasses. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2-5, 2022, pages 40:1-40:12. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533357.
  11. Stéphane Demri, Marcin Jurdzinski, Oded Lachish, and Ranko Lazic. The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci., 79(1):23-38, 2013. URL: https://doi.org/10.1016/j.jcss.2012.04.002.
  12. Alex Dixon and Ranko Lazic. Kreach: A tool for reachability in petri nets. In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I, volume 12078 of Lecture Notes in Computer Science, pages 405-412. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45190-5_22.
  13. Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset nets between decidability and undecidability. In Kim Guldstrand Larsen, Sven Skyum, and Glynn Winskel, editors, Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings, volume 1443 of Lecture Notes in Computer Science, pages 103-115. Springer, 1998. URL: https://doi.org/10.1007/BFb0055044.
  14. Matthias Englert, Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Juliusz Straszynski. A lower bound for the coverability problem in acyclic pushdown VAS. Inf. Process. Lett., 167:106079, 2021. URL: https://doi.org/10.1016/j.ipl.2020.106079.
  15. Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, and Filip Nikšić. An SMT-based approach to coverability analysis. In Proc. 26^th International Conference on Computer Aided Verification (CAV), pages 603-619, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_40.
  16. John Fearnley and Marcin Jurdziński. Reachability in Two-Clock Timed Automata Is PSPACE-Complete. In Fedor V. Fomin, Rūsiņš Freivalds, Marta Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming, pages 212-223, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  17. John Fearnley and Marcin Jurdzinski. Reachability in two-clock timed automata is pspace-complete. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 212-223. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_21.
  18. Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, and Grégoire Sutre. Polynomial-space completeness of reachability for succinct branching VASS in dimension one. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 119:1-119:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.119.
  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. Estíbaliz Fraca and Serge Haddad. Complexity analysis of continuous Petri nets. Fundamenta Informaticae, 137(1):1-28, 2015. URL: https://doi.org/10.3233/FI-2015-1168.
  21. Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche. Reachability in bidirected pushdown VASS. In Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France, volume 229 of LIPIcs, pages 124:1-124:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.124.
  22. 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.
  23. Stefan Göller, Christoph Haase, Ranko Lazic, and Patrick Totzke. A polynomial-time algorithm for reachability in branching VASS in dimension one. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 105:1-105:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.105.
  24. Eitan M. Gurari and Oscar H. Ibarra. The complexity of decision problems for finite-turn multicounter machines. J. Comput. Syst. Sci., 22(2):220-229, 1981. URL: https://doi.org/10.1016/0022-0000(81)90028-3.
  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, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in succinct and parametric one-counter automata. In Mario Bravetti and Gianluigi Zavattaro, editors, CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, volume 5710 of Lecture Notes in Computer Science, pages 369-383. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_25.
  27. John Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8(2):135-159, 1979. Google Scholar
  28. Eryk Kopczynski. Complexity of problems of commutative grammars. Log. Methods Comput. Sci., 11(1), 2015. URL: https://doi.org/10.2168/LMCS-11(1:9)2015.
  29. 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.
  30. 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.
  31. Jérôme Leroux and Grégoire Sutre. Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of Leibniz International Proceedings in Informatics (LIPIcs), pages 37:1-37:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.37.
  32. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 324-336. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_26.
  33. Richard Lipton. The reachability problem is exponential-space hard. Yale University, Department of Computer Science, Report, 62, 1976. Google Scholar
  34. Filip Mazowiecki, Henry Sinclair-Banks, and Karol Węgrzycki. Coverability in 2-vass with one unary counter is in np. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures, pages 196-217, Cham, 2023. Springer Nature Switzerland. Google Scholar
  35. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223-231, 1978. Google Scholar
  36. Louis E Rosier and Hsu-Chun Yen. A multiparameter analysis of the boundedness problem for vector addition systems. Journal of Computer and System Sciences, 32(1):105-135, 1986. Google Scholar
  37. Sylvain Schmitz. The complexity of reachability in vector addition systems. ACM SIGLOG News, 3(1):4-21, 2016. URL: https://doi.org/10.1145/2893582.2893585.
  38. 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.
  39. Wil M. P. van der Aalst. Verification of workflow nets. In Proc. 18^th International Conference on Application and Theory of Petri Nets (ICATPN), volume 1248, pages 407-426, 1997. URL: https://doi.org/10.1007/3-540-63139-9_48.
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