Energy-parity objectives combine \(\omega\)-regular with quantitative objectives of reward MDPs. The controller needs to avoid running out of energy while at the same time satisfying a parity objective.
We refute the common belief that, if an energy-parity objective holds almost-surely, then this can be realised by some finite memory strategy. We provide a surprisingly simple counterexample that only uses coBüchi conditions.
This breacks a published construction of Chatterjee & Doyen (MFCS'11) that argues for the decidability of the almost-sure problem. We provide a new proof.
We introduce the new class of bounded (energy) storage objectives that, when combined with parity objectives, preserve the finite memory property. Based on these, we show that almost-sure, as well as limit-sure, energy-parity objectives are in \(NP\cap coNP\) and can be solved in pseudo-polynomial time for energy-parity MDPs.
(An uncut version of the slides is available here.)