DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2026.36

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

Authors: Pranshu Gaba and Shibashis Guha

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{gaba_et_al:LIPIcs.CONCUR.2026.36,
  author =	{Gaba, Pranshu and Guha, Shibashis},
  title =	{{Sure-Almost-Sure and Sure-Limit-Sure Window Mean Payoff in Markov Decision Processes}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{36:1--36:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.36},
  URN =		{urn:nbn:de:0030-drops-273664},
  doi =		{10.4230/LIPIcs.CONCUR.2026.36},
  annote =	{Keywords: Beyond worst-case synthesis, sure-almost-sure satisfaction, window mean payoff, finitary objectives, Markov decision processes}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2025.16

Expectation in Stochastic Games with Prefix-Independent Objectives

Authors: Laurent Doyen, Pranshu Gaba, and Shibashis Guha

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract

Stochastic two-player games model systems with an environment that is both adversarial and stochastic. In this paper, we study the expected value of bounded quantitative prefix-independent objectives in the context of stochastic games. We show a generic reduction from the expectation problem to linearly many instances of the almost-sure satisfaction problem for threshold Boolean objectives. The result follows from partitioning the vertices of the game into so-called value classes where each class consists of vertices of the same value. Our procedure further entails that the memory required by both players to play optimally for the expectation problem is no more than the memory required by the players to play optimally for the almost-sure satisfaction problem for a corresponding threshold Boolean objective. We show the applicability of the framework to compute the expected window mean-payoff measure in stochastic games. The window mean-payoff measure strengthens the classical mean-payoff measure by computing the mean payoff over windows of bounded length that slide along an infinite path. We show that the decision problem to check if the expected window mean-payoff value is at least a given threshold is in UP ∩ coUP when the window length is given in unary.

Cite as

Laurent Doyen, Pranshu Gaba, and Shibashis Guha. Expectation in Stochastic Games with Prefix-Independent Objectives. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{doyen_et_al:LIPIcs.CONCUR.2025.16,
  author =	{Doyen, Laurent and Gaba, Pranshu and Guha, Shibashis},
  title =	{{Expectation in Stochastic Games with Prefix-Independent Objectives}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{16:1--16:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.16},
  URN =		{urn:nbn:de:0030-drops-239668},
  doi =		{10.4230/LIPIcs.CONCUR.2025.16},
  annote =	{Keywords: Stochastic games, finitary objectives, mean payoff, reactive synthesis}
}

Search Results

Documents authored by Gaba, Pranshu

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

Abstract

Cite as

Expectation in Stochastic Games with Prefix-Independent Objectives

Abstract

Cite as

Thanks for your feedback!

Could not send message