Document Open Access Logo

Long-Run Average Behavior of Vector Addition Systems with States

Authors Krishnendu Chatterjee , Thomas A. Henzinger, Jan Otop

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.27.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Krishnendu Chatterjee
  • IST Austria, Klosterneuburg, Austria
Thomas A. Henzinger
  • IST Austria, Klosterneuburg, Austria
Jan Otop
  • University of Wrocław, Poland

Funding

  • Chatterjee, Krishnendu: The Austrian Science Fund (FWF) NFN grant S11407-N23 (RiSE/SHiNE)
  • Henzinger, Thomas A.: The Austrian Science Fund (FWF) grants S11402-N23 (RiSE/ShiNE) and Z211-N23 (Wittgenstein Award)
  • Otop, Jan: The National Science Centre (NCN), Poland under grant 2017/27/B/ST6/00299

Acknowledgements

We thank Petr Novotný for helpful discussion on the literature.

Cite As Get BibTex

Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Long-Run Average Behavior of Vector Addition Systems with States. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.CONCUR.2019.27

Abstract

A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite computations of VASS. The cost of a configuration is for each state, a linear combination of the counter values. In the special case of uniform cost functions, the linear combination is the same for all states. The (regular) long-run emptiness problem is, given a VASS, a cost function, and a threshold value, if there is a (lasso-shaped) computation such that the long-run average value of the cost function does not exceed the threshold. For uniform cost functions, we show that the regular long-run emptiness problem is (a) decidable in polynomial time for integer-valued VASS, and (b) decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative counters). For general cost functions, we show that the problem is (c) NP-complete for integer-valued VASS, and (d) undecidable for natural-valued VASS. Our most interesting result is for (c) integer-valued VASS with general cost functions, where we establish a connection between the regular long-run emptiness problem and quadratic Diophantine inequalities. The general (nonregular) long-run emptiness problem is equally hard as the regular problem in all cases except (c), where it remains open.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Quantitative automata
Keywords
  • vector addition systems
  • mean-payoff
  • Diophantine inequalities

Metrics

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

Related Versions

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofman, Richard Mayr, K. Narayan Kumar, and Patrick Totzke. Infinite-state energy games. In CSL-LICS 2014, pages 7:1-7:10, 2014. Google Scholar
  2. Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability in Parameterized Verification. SIGACT News, 47(2):53-64, 2016. Google Scholar
  3. Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, and Simon Laursen. Average-energy games. Acta Inf., 55(2):91-127, 2018. Google Scholar
  4. Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, Dominik Velan, and Florian Zuleger. Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. In LICS 2018, pages 185-194, 2018. Google Scholar
  5. Tomás Brázdil, Stefan Kiefer, Antonín Kucera, and Petr Novotný. Long-Run Average Behaviour of Probabilistic Vector Addition Systems. In LICS 2015, pages 44-55, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.15.
  6. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Nested Weighted Limit-Average Automata of Bounded Width. In MFCS 2016, pages 24:1-24:14, 2016. Google Scholar
  7. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative Monitor Automata. In SAS 2016, pages 23-38, 2016. Google Scholar
  8. Krishnendu Chatterjee and Yaron Velner. Hyperplane separation technique for multidimensional mean-payoff games. J. Comput. Syst. Sci., 88:236-259, 2017. Google Scholar
  9. Krishnendu Chatterjee and Yaron Velner. The Complexity of Mean-Payoff Pushdown Games. J. ACM, 64(5):34:1-34:49, 2017. 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. In STOC, pages 398-406, 2019. Google Scholar
  11. Alberto Del Pia, Santanu S Dey, and Marco Molinaro. Mixed-integer quadratic programming is in NP. Mathematical Programming, 162(1-2):225-240, 2017. Google Scholar
  12. Emanuele D'Osualdo, Jonathan Kochems, and C. H. Luke Ong. Automatic Verification of Erlang-Style Concurrency. In Francesco Logozzo and Manuel Fähndrich, editors, SAS 2013, pages 454-476, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/978-3-642-38856-9_24.
  13. Javier Esparza. Decidability and complexity of Petri net problems—an introduction. Lectures on Petri nets I: Basic models, pages 374-428, 1998. Google Scholar
  14. Javier Esparza and Mogens Nielsen. Decidability Issues for Petri Nets - a survey. Bulletin of the European Association for Theoretical Computer Science, 52:245-262, 1994. Google Scholar
  15. Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps. Component-based Synthesis for Complex APIs. In POPL 2017, POPL 2017, pages 599-612, New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3009837.3009851.
  16. Pierre Ganty and Rupak Majumdar. Algorithmic Verification of Asynchronous Programs. ACM Trans. Program. Lang. Syst., 34(1):6:1-6:48, May 2012. URL: http://dx.doi.org/10.1145/2160910.2160915.
  17. John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation (3rd Edition). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2006. Google Scholar
  18. Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Dynamic Cutoff Detection in Parameterized Concurrent Programs. In CAV 2010, pages 645-659, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14295-6_55.
  19. Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Efficient Coverability Analysis by Proof Minimization. In Maciej Koutny and Irek Ulidowski, editors, CONCUR 2012, pages 500-515, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/978-3-642-32940-1_35.
  20. Richard M. Karp and Raymond E. Miller. Parallel Program Schemata. J. Comput. Syst. Sci., 3(2):147-195, 1969. Google Scholar
  21. S. Rao Kosaraju. Decidability of Reachability in Vector Addition Systems (Preliminary Version). In Proceedings of the 14th Annual ACM Symposium on Theory of Computing, May 5-7, 1982, San Francisco, California, USA, pages 267-281, 1982. URL: http://dx.doi.org/10.1145/800070.802201.
  22. Jean-Luc Lambert. A Structure to Decide Reachability in Petri Nets. Theor. Comput. Sci., 99(1):79-104, 1992. URL: http://dx.doi.org/10.1016/0304-3975(92)90173-D.
  23. Jérôme Leroux. Vector addition systems reachability problem (a simpler solution). In EPiC, volume 10, pages 214-228. Andrei Voronkov, 2012. Google Scholar
  24. Jérôme Leroux. Polynomial Vector Addition Systems With States. In ICALP 2018, pages 134:1-134:13, 2018. Google Scholar
  25. R. Lipton. The Reachability Problem Requires Exponential Space. Technical report 62, Yale, 1976. Google Scholar
  26. Ernst W. Mayr. An Algorithm for the General Petri Net Reachability Problem. In STOC 1981, pages 238-246, 1981. URL: http://dx.doi.org/10.1145/800076.802477.
  27. Jakub Michaliszyn and Jan Otop. Average Stack Cost of Büchi Pushdown Automata. In FSTTCS 2017, pages 42:1-42:13, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2017.42.
  28. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223-231, 1978. URL: http://dx.doi.org/10.1016/0304-3975(78)90036-1.
  29. Moritz Sinn, Florian Zuleger, and Helmut Veith. A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. In CAV, pages 745-761, 2014. Google Scholar
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