Document Open Access Logo

Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States

Authors Krishnendu Chatterjee , Thomas A. Henzinger, Jan Otop

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2020.23.pdf
  • Filesize: 0.57 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

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

Metrics

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

Abstract

A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A probabilistic VASS consists of a VASS along with a probability distribution over the transitions for each state. Qualitative properties such as state and configuration reachability have been widely studied for VASS. In this work we consider multi-dimensional long-run average objectives for VASS and probabilistic VASS. For a counter, the cost of a configuration is the value of the counter; and the long-run average value of a computation for the counter is the long-run average of the costs of the configurations in the computation. The multi-dimensional long-run average problem given a VASS and a threshold value for each counter, asks whether there is a computation such that for each counter the long-run average value for the counter does not exceed the respective threshold. For probabilistic VASS, instead of the existence of a computation, we consider whether the expected long-run average value for each counter does not exceed the respective threshold. Our main results are as follows: we show that the multi-dimensional long-run average problem (a) is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for probabilistic integer-valued VASS, and probabilistic natural-valued VASS when all computations are non-terminating.

Cite As Get BibTex

Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 23:1-23:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.23

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 B/ST6/00299.

Acknowledgements

We want to thank the anonymous reviewers for their helpful comments, which contributed to the final version of this paper.

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. URL: https://doi.org/10.1145/2603088.2603100.
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. 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. URL: https://doi.org/10.1145/2951860.2951873.
  4. 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 2015, pages 32-43. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.14.
  5. 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. URL: https://doi.org/10.1145/3209108.3209191.
  6. 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: https://doi.org/10.1109/LICS.2015.15.
  7. 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. URL: https://doi.org/10.4230/LIPIcs.MFCS.2016.24.
  8. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative monitor automata. In SAS 2016, pages 23-38, 2016. URL: https://doi.org/10.1007/978-3-662-53413-7_2.
  9. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Long-run average behavior of vector addition systems with states. In CONCUR 2019, pages 27:1-27:16, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.27.
  10. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative automata under probabilistic semantics. Logical Methods in Computer Science, 15(3), 2019. URL: https://doi.org/10.23638/LMCS-15(3:16)2019.
  11. Krishnendu Chatterjee and Yaron Velner. The complexity of mean-payoff pushdown games. J. ACM, 64(5):34:1-34:49, 2017. URL: https://doi.org/10.1145/3121408.
  12. Krishnendu Chatterjee and Yaron Velner. Hyperplane separation technique for multidimensional mean-payoff games. J. Comput. Syst. Sci., 88:236-259, 2017. URL: https://doi.org/10.1016/j.jcss.2017.04.005.
  13. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for petri nets is not elementary. In STOC 2019, pages 24-33, 2019. URL: https://doi.org/10.1145/3313276.3316369.
  14. Emanuele D'Osualdo, Jonathan Kochems, and C.-H. Luke Ong. Automatic verification of erlang-style concurrency. In SAS 2013, pages 454-476, 2013. URL: https://doi.org/10.1007/978-3-642-38856-9_24.
  15. Javier Esparza. Decidability and complexity of petri net problems—an introduction. Lectures on Petri nets I: Basic models, pages 374-428, 1998. Google Scholar
  16. Javier Esparza and Mogens Nielsen. Decidability issues for petri nets - a survey. Bull. EATCS, 52:244-262, 1994. Google Scholar
  17. W. Feller. An introduction to probability theory and its applications. Wiley, 1971. Google Scholar
  18. Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps. Component-based synthesis for complex apis. In POPL 2017, pages 599-612, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3009837.3009851.
  19. Jerzy Filar and Koos Vrieze. Competitive Markov decision processes. Springer, 1996. Google Scholar
  20. Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst., 34(1):6:1-6:48, May 2012. URL: https://doi.org/10.1145/2160910.2160915.
  21. Christoph Haase and Simon Halfon. Integer vector addition systems with states. In RP 2014, pages 112-124, 2014. URL: https://doi.org/10.1007/978-3-319-11439-2_9.
  22. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in succinct and parametric one-counter automata. In CONCUR 2009, pages 369-383, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_25.
  23. Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Dynamic cutoff detection in parameterized concurrent programs. In CAV 2010, pages 645-659, 2010. URL: https://doi.org/10.1007/978-3-642-14295-6_55.
  24. 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: https://doi.org/10.1007/978-3-642-32940-1_35.
  25. 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.
  26. 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: https://doi.org/10.1145/800070.802201.
  27. Jean-Luc Lambert. A structure to decide reachability in petri nets. Theoretical Computer Science, 99(1):79-104, 1992. URL: https://doi.org/10.1016/0304-3975(92)90173-D.
  28. Jérôme Leroux. Vector addition systems reachability problem (A simpler solution). In Turing-100 - The Alan Turing Centenary, Manchester, UK, June 22-25, 2012, pages 214-228, 2012. URL: https://easychair.org/publications/paper/Blr.
  29. Jérôme Leroux. Polynomial vector addition systems with states. In ICALP 2018, pages 134:1-134:13, 2018. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.134.
  30. Richard Lipton. The reachability problem is exponential-space hard. Department of Computer Science, Yale University, Tech. Rep, 62, 1976. Google Scholar
  31. Ernst W. Mayr. An Algorithm for the General Petri Net Reachability Problem. In STOC 1981, pages 238-246, 1981. URL: https://doi.org/10.1145/800076.802477.
  32. Jakub Michaliszyn and Jan Otop. Average stack cost of büchi pushdown automata. In FSTTCS 2017, pages 42:1-42:13, 2017. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2017.42.
  33. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223-231, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
  34. Moritz Sinn, Florian Zuleger, and Helmut Veith. A simple and scalable static analysis for bound analysis and amortized complexity analysis. In CAV 2014, pages 745-761, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_50.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact