Document

# Long-Run Average Behavior of Vector Addition Systems with States

## File

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

## Acknowledgements

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

## Cite As

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
• mean-payoff
• Diophantine inequalities

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## 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.
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.
3. Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, and Simon Laursen. Average-energy games. Acta Inf., 55(2):91-127, 2018.
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.
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.
7. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative Monitor Automata. In SAS 2016, pages 23-38, 2016.
8. Krishnendu Chatterjee and Yaron Velner. Hyperplane separation technique for multidimensional mean-payoff games. J. Comput. Syst. Sci., 88:236-259, 2017.
9. Krishnendu Chatterjee and Yaron Velner. The Complexity of Mean-Payoff Pushdown Games. J. ACM, 64(5):34:1-34:49, 2017.
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.
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.
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.
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.
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.
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.
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.
24. Jérôme Leroux. Polynomial Vector Addition Systems With States. In ICALP 2018, pages 134:1-134:13, 2018.
25. R. Lipton. The Reachability Problem Requires Exponential Space. Technical report 62, Yale, 1976.
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.