Sure-almost-sure and Sure-limit-sure Mean Payoff in Markov Decision Processes
Raphaël Berthon, Pranshu Gaba, Vaani Goenka, Shibashis Guha, Chandralekha P
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.
In this talk, we look at the sure-almost-sure and sure-limit-sure problems for the mean-payoff objective. Also known as limit-average payoff, this classical objective measures the average performance of the system in the long run, that is over an infinite horizon. We show that sure-almost-sure problem and the sure-limit-sure problems are no harder than sure satisfaction and almost-sure satisfaction when considered separately. We also show that finite memory winning strategies exist for sure-limit-sure but infinite memory is required in general for winning strategies for sure-almost-sure satisfaction.