Document Open Access Logo

Sure-Almost-Sure and Sure-Limit-Sure Window Mean Payoff in Markov Decision Processes

Authors Pranshu Gaba , Shibashis Guha

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.36.pdf
  • Filesize: 1.33 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Stochastic processes
Keywords
  • Beyond worst-case synthesis
  • sure-almost-sure satisfaction
  • window mean payoff
  • finitary objectives
  • Markov decision processes

Metrics

Abstract

Given rationals α and β, the sure-almost-sure problem for a threshold Boolean objective φ in a Markov decision process (MDP) asks if one can simultaneously ensure that all outcomes of the MDP have φ-value at least α (i.e. sure α satisfaction), and with probability 1 the outcome has φ-value at least β (i.e. almost-sure β satisfaction). The sure-limit-sure problem asks if for all ε > 0, one can simultaneously ensure that all outcomes have φ-value at least α, and with probability at least 1 - ε the outcome has φ-value at least β. Moreover, if simultaneous satisfaction of objectives is possible, then one would also like to construct a strategy (for sure-almost-sure) or a family of strategies (for sure-limit-sure) that achieves this. Even if both sure satisfaction and almost-sure (resp., limit-sure) satisfaction for an objective are known, combining the two is often non-trivial and requires novel techniques and approaches. 
In this paper, we solve the sure-almost-sure and sure-limit-sure problems for window mean-payoff objectives. While it is known that almost-sure satisfaction and limit-sure satisfaction for window mean-payoff coincide in MDPs, we show that sure-almost-sure satisfaction is distinct from sure-limit-sure satisfaction. The window mean-payoff objective strengthens the standard mean-payoff objective by requiring that eventually, from every point in the infinite run, the average payoff becomes greater than a given threshold within a finite window length. We study two variants of window mean payoff: in the fixed variant, the window length 𝓁 is given, while in the bounded variant, the length is not given but is required to be bounded throughout the run. We show that the sure-almost-sure problem and the sure-limit-sure problem are both in PTIME for the fixed variant (if 𝓁 is given in unary) and are both in NP ∩ coNP for the bounded variant, matching the computational complexity of sure satisfaction and almost-sure satisfaction when considered separately for these objectives. We also give bounds for the memory requirement of winning strategies for all considered problems.

Cite As Get BibTex

Pranshu Gaba and Shibashis Guha. Sure-Almost-Sure and Sure-Limit-Sure Window Mean Payoff in Markov Decision Processes. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 36:1-36:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.36

Author Details

Pranshu Gaba
  • Tata Institute of Fundamental Research, Mumbai, India
Shibashis Guha
  • Tata Institute of Fundamental Research, Mumbai, India

Funding

We acknowledge support of CEFIPRA project no. 7302-I and of the Department of Atomic Energy, Government of India, project no. RTI4014.

Acknowledgements

We thank anonymous reviewers for suggesting various improvements and pointing out a subtle bug in a proof.

References

  1. K. R. Apt and E. Grädel. Lectures in Game Theory for Computer Scientists. Cambridge University Press, 2011. URL: https://doi.org/10.1017/CBO9780511973468.
  2. C. Baier and J-P. Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. R. Berthon, S. Guha, and J.-F. Raskin. Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes. In LICS, pages 195-208. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394805.
  4. R. Berthon, J-P. Katoen, and T. Winkler. Markov Decision Processes with Sure Parity and Multiple Reachability Objectives. In RP, volume 15050 of Lecture Notes in Computer Science, pages 203-220. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-72621-7_14.
  5. R. Berthon, M. Randour, and J.-F. Raskin. Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes. In ICALP, volume 80 of LIPIcs, pages 121:1-121:15, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.121.
  6. B. Bordais, S. Guha, and J-F. Raskin. Expected Window Mean-Payoff. In FSTTCS, volume 150 of LIPIcs, pages 32:1-32:15, 2019. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2019.32.
  7. T. Brihaye, F. Delgrange, Y. Oualhadj, and M. Randour. Life is Random, Time is Not: Markov Decision Processes with Window Objectives. Logical Methods in Computer Science, Volume 16, Issue 4, December 2020. URL: https://doi.org/10.23638/LMCS-16(4:13)2020.
  8. V. Bruyère, E. Filiot, M. Randour, and J-F. Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. Information and Computation, 254:259-295, 2017. URL: https://doi.org/10.1016/j.ic.2016.10.011.
  9. K. Chatterjee, L. de Alfaro, and T. A. Henzinger. The Complexity of Stochastic Rabin and Streett Games. In ICALP, pages 878-890. Springer, 2005. URL: https://doi.org/10.1007/11523468_71.
  10. K. Chatterjee, L. Doyen, M. Randour, and J-F. Raskin. Looking at mean-payoff and total-payoff through windows. Information and Computation, 242:25-52, 2015. URL: https://doi.org/10.1016/j.ic.2015.03.010.
  11. K. Chatterjee, T. A. Henzinger, and F. Horn. Stochastic Games with Finitary Objectives. In MFCS, pages 34-54. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03816-7_4.
  12. K. Chatterjee, Z. Křetínská, and J. Křetínský. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. Logical Methods in Computer Science, Volume 13, Issue 2, July 2017. URL: https://doi.org/10.23638/LMCS-13(2:15)2017.
  13. K. Chatterjee and N. Piterman. Combinations of Qualitative Winning for Stochastic Parity Games. In CONCUR, volume 140 of LIPIcs, pages 6:1-6:17, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.6.
  14. L. Clemente and J.-F. Raskin. Multidimensional beyond Worst-Case and Almost-Sure Problems for Mean-Payoff Objectives. In LICS, pages 257-268. IEEE, 2015. URL: https://doi.org/10.1109/LICS.2015.33.
  15. L. Doyen, P. Gaba, and S. Guha. Expectation in Stochastic Games with Prefix-Independent Objectives. In CONCUR, volume 348 of LIPIcs, pages 16:1-16:19, 2025. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2025.16.
  16. L. Doyen, P. Gaba, and S. Guha. Stochastic Window Mean-Payoff Games. Logical Methods in Computer Science, Volume 21, Issue 2, June 2025. URL: https://doi.org/10.46298/lmcs-21(2:19)2025.
  17. L. Doyen and S. Guha. Algorithm and Strategy Construction for Sure-Almost-Sure Stochastic Parity Games. In STACS, pages 34:1-34:20, 2026. URL: https://doi.org/10.4230/LIPIcs.STACS.2026.34.
  18. A. Ehrenfeucht and J. Mycielski. Positional Strategies for Mean Payoff Games. Int. Journal of Game Theory, 8(2):109-113, 1979. URL: https://doi.org/10.1007/BF01768705.
  19. P. Gaba and S. Guha. Optimising Expectation with Guarantees for Window Mean Payoff in Markov Decision Processes. In AAMAS, pages 820-828, 2025. URL: https://doi.org/10.5555/3709347.3743600.
  20. P. Gaba and S. Guha. Sure-almost-sure and Sure-limit-sure Window Mean Payoff in Markov Decision Processes, 2026. URL: https://doi.org/10.48550/arXiv.2605.12191.
  21. E. Grädel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-36387-4.
  22. D. A. Martin. The Determinacy of Blackwell Games. The Journal of Symbolic Logic, 63(4):1565-1581, 1998. URL: https://doi.org/10.2307/2586667.
  23. M. L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, 1994. Google Scholar
  24. U. Schöning. A low and a high hierarchy within NP. Journal of Computer and System Sciences, 27(1):14-28, 1983. URL: https://doi.org/10.1016/0022-0000(83)90027-2.
  25. U. Zwick and M. Paterson. The Complexity of Mean Payoff Games on Graphs. Theoretical Computer Science, 158(1&2):343-359, 1996. URL: https://doi.org/10.1016/0304-3975(95)00188-3.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact