Finite-memory Strategies for Almost-sure Energy-MeanPayoff Objectives in MDPs

TL;DR

This paper studies finite-memory strategies in Markov decision processes to achieve energy safety and positive mean payoff objectives, showing that exponential memory suffices and is necessary, with decidability results.

Contribution

It proves that finite memory strategies are sufficient for almost-sure winning in Energy-MeanPayoff objectives, contrasting with Energy-Parity objectives requiring infinite memory.

Findings

Finite memory suffices for almost-sure strategies.

Exponential memory is both sufficient and necessary.

Decidability of strategy existence in pseudo-polynomial time.

Abstract

We consider finite-state Markov decision processes with the combined Energy-MeanPayoff objective. The controller tries to avoid running out of energy while simultaneously attaining a strictly positive mean payoff in a second dimension. We show that finite memory suffices for almost surely winning strategies for the Energy-MeanPayoff objective. This is in contrast to the closely related Energy-Parity objective, where almost surely winning strategies require infinite memory in general. We show that exponential memory is sufficient (even for deterministic strategies) and necessary (even for randomized strategies) for almost surely winning Energy-MeanPayoff. The upper bound holds even if the strictly positive mean payoff part of the objective is generalized to multidimensional strictly positive mean payoff. Finally, it is decidable in pseudo-polynomial time whether an almost surely winning strategy exists.