2017/01/10 by Richard Mayr, Mayr, Richard, Sven Schewe +5
Biochemistry, Genetics and Molecular Biology · Computer Science · Engineering · #Advanced Control Systems Optimization #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Receptor Mechanisms and Signaling
paper · doi:10.48550/arxiv.1701.02546
openalex publication_date 2017/01/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Energy-parity objectives combine ω-regular with quantitative objectives of reward MDPs. The controller needs to avoid to run out of energy while 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. 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 and limit-sure energy-parity objectives, as well as almost-sure and limit-sure storage parity objectives, are in NP∩ coNP and can be solved in pseudo-polynomial time for energy-parity MDPs.