Abstract
We study stochastic games with energy-parity objectives, which combine quantitative rewards with a qualitative \(\omega \)-regular condition: The maximizer aims to avoid running out of energy while simultaneously satisfying a parity condition. We show that the corresponding almost-sure problem, i.e., checking whether there exists a maximizer strategy that achieves the energy-parity objective with probability 1 when starting at a given energy level k, is decidable and in \(\mathsf {NP}\cap \mathsf {coNP}\). The same holds for checking if such a k exists and if a given k is minimal.
Chapter PDF
Similar content being viewed by others
References
Abdulla, P., Mayr, R., Sangnier, A., Sproston, J.: Solving parity games on integer vectors. In: International Conference on Concurrency Theory (CONCUR). vol. 8052 (2013)
Abdulla, P.A., Ciobanu, R., Mayr, R., Sangnier, A., Sproston, J.: Qualitative analysis of VASS-induced MDPs. In: International Conference on Foundations of Software Science and Computational Structures (FoSSaCS). vol. 9634 (2016)
Abdulla, P.A., Henda, N.B., Mayr, R.: Decisive Markov Chains. Logical Methods in Computer Science Volume 3, Issue 4 (Nov 2007)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)
Billingsley, P.: Probability and Measure. Wiley (1995), third Edition
Blondel, V.D., Canterini, V.: Undecidable problems for probabilistic automata of fixed dimension. Theory of Computing systems 36(3) (2003)
Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). vol. 5215, pp. 33–47 (2008)
Brázdil, T., Brožek, V., Etessami, K., Kučera, A.: Approximating the Termination Value of One-Counter MDPs and Stochastic Games. Information and Computation 222, 121–138 (2013)
Brázdil, T., Kučera, A., Novotný, P.: Optimizing the expected mean payoff in energy Markov decision processes. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). vol. 9938, pp. 32–49 (2016)
Brázdil, T., Brožek, V., Chatterjee, K., Forejt, V., Kučera,A.: Markov decision processes with multiple long-run average objectives. Logical Methods in Computer Science 10 (2014)
Brázdil, T., Brožek, V., Etessami, K.: One-Counter Stochastic Games. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). vol. 8, pp. 108–119 (2010)
Brázdil, T., Brožek, V., Etessami, K., Kučera, A., Wojtczak,D.: One-counter Markov decision processes. In: ACM-SIAM Symposium on Discrete Algorithms (SODA). pp. 863–874 (2010)
Brázdil, T., Kiefer, S., Kučera, A., Novotný, P., Katoen, J.P.: Zero-reachability in probabilistic multi-counter automata. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 22:1–22:10 (2014)
Chakrabarti, A., De Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: International Workshop on Embedded Software. pp. 117–133 (2003)
Chatterjee, K., De Alfaro, L., Henzinger, T.A.: The complexity of stochastic Rabin and Streett games. In: International Colloquium on Automata, Languages and Programming (ICALP). pp. 878–890 (2005)
Chatterjee, K., Doyen, L.: Energy parity games. In: International Colloquium on Automata, Languages and Programming (ICALP). vol. 6199, pp. 599–610 (2010)
Chatterjee, K., Doyen, L.: Energy and mean-payoff parity Markov decision processes. In: International Symposium on Mathematical Foundations of Computer Science (MFCS). vol. 6907, pp. 206–218 (2011)
Chatterjee, K., Doyen, L.: Games and Markov decision processes with mean-payoff parity and energy parity objectives. In: Mathematical and Engineering Methods in Computer Science (MEMICS). LNCS, vol. 7119, pp. 37–46. Springer (2011)
Chatterjee, K., Doyen, L.: Energy parity games. Theoretical Computer Science 458, 49–60 (2012)
Chatterjee, K., Doyen, L., Gimbert, H., Oualhadj, Y.: Perfect-information stochastic mean-payoff parity games. In: International Conference on Foundations of Software Science and Computational Structures (FoSSaCS). vol. 8412 (2014)
Chatterjee, K., Henzinger, T.A., Piterman, N.: Generalized parity games. In: International Conference on Foundations of Software Science and Computational Structures (FoSSaCS). pp. 153–167 (2007)
Chatterjee, K., Jurdziński, M., Henzinger, T.A.: Simple stochastic parity games. In: Computer Science Logic (CSL). vol. 2803, pp. 100–113. Springer (2003)
Chatterjee, K., Jurdziński, M., Henzinger, T.A.: Quantitative stochastic parity games. In: ACM-SIAM Symposium on Discrete Algorithms (SODA). pp. 121–130. SIAM (2004)
Chatterjee, K., Kretínská, Z., Kretínský, J.:Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science 13(2) (2017)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (Dec 1999)
Daviaud, L., Jurdziński, M., Lazić, R.: A pseudo-quasi-polynomial algorithm for mean-payoff parity games. In: Logic in Computer Science (LICS). pp. 325–334 (2018)
De Alfaro, L., Henzinger, T.A.: Interface automata. ACM SIGSOFT Software Engineering Notes 26(5), 109–120 (2001)
Dill, D.L.: Trace theory for automatic hierarchical verification of speed-independent circuits, vol. 24. MIT press Cambridge (1989)
Fearnley, J.: Exponential lower bounds for policy iteration. In: International Colloquium on Automata, Languages and Programming (ICALP). pp. 551–562 (2010)
Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer (1997)
Friedmann, O.: An exponential lower bound for the parity game strategy improvement algorithm as we know it. In: Logic in Computer Science (LICS). pp. 145–156 (2009)
Friedmann, O., Hansen, T.D., Zwick, U.: Subexponential lower bounds for randomized pivoting rules for the simplex algorithm. In: Symposium on Theory of Computing (STOC). pp. 283–292 (2011)
Gillette, D.: Stochastic games with zero stop probabilities. Contributions to the Theory of Games 3, 179–187 (1957)
Gimbert, H., Kelmendi, E.: Two-Player Perfect-Information Shift-Invariant Submixing Stochastic Games Are Half-Positional (Jan 2014), working paper or preprint available at: https://hal.archives-ouvertes.fr/hal-00936371
Jurdziński, M.: Deciding the winner in parity games is in UP \(\cap \) co-UP. Information Processing Letters 68(3), 119–124 (1998)
Jurdziński, M., Lazić, R., Schmitz, S.: Fixed-dimensional energy games are in pseudo-polynomial time. In: International Colloquium on Automata, Languages and Programming (ICALP). vol. 9135, pp. 260–272 (2015)
Kiefer, S., Mayr, R., Shirmohammadi, M., Wojtczak, D.: On strong determinacy of countable stochastic games. Logic in Computer Science (LICS) (2017)
Maitra, A., Sudderth, W.: Stochastic games with Borel payoffs. In: Stochastic Games and Applications, pp. 367–373. Kluwer, Dordrecht (2003)
Martin, D.A.: The determinacy of Blackwell games. Journal of Symbolic Logic 63(4), 1565–1581 (1998)
Mayr, R., Schewe, S., Totzke, P., Wojtczak, D.: MDPs with Energy-Parity Objectives. Logic in Computer Science (LICS) (2017)
Mayr, R., Schewe, S., Totzke, P., Wojtczak, D.: Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP (2021), arXiv:2101.06989
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Annual Symposium on Principles of Programming Languages (POPL). pp. 179–190 (1989)
Pogosyants, A., Segala, R., Lynch, N.: Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. Distributed Computing 13(3), 155–186 (2000)
Rabin, M.O.: Automata on infinite objects and Church’s problem, vol. 13. American Mathematical Soc. (1972)
Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM journal on control and optimization 25(1), 206–230 (1987)
Shapley, L.S.: Stochastic games. Proceedings of the national academy of sciences 39(10), 1095–1100 (1953)
Stoelinga, M.: Fun with firewire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol. Formal aspects of computing 14(3), 328–337 (2003)
Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T.A., Rabinovich, A., Raskin, J.F.: The complexity of multi-mean-payoff and multi-energy games. Information and Computation 241, 177 – 196 (2015)
Wilke, T.: Alternating tree automata, parity games, and modal mu-calculus. Bulletin of the Belgian Mathematical Society Simon Stevin 8(2), 359 (2001)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Mayr, R., Schewe, S., Totzke, P., Wojtczak, D. (2021). Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP. In: Kiefer, S., Tasson, C. (eds) Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science(), vol 12650. Springer, Cham. https://doi.org/10.1007/978-3-030-71995-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-030-71995-1_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71994-4
Online ISBN: 978-3-030-71995-1
eBook Packages: Computer ScienceComputer Science (R0)