What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives
Krishnendu Chatterjee, Martin Chmelík, Mathieu Tracol · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2013
We consider partially observable Markov decision processes (POMDPs) with omega-regular conditions specified as parity objectives. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are known to be undecidable even for very special cases of parity objectives, we establish decidability (with optimal EXPTIME-complete complexity) of the qualitative analysis problems for POMDPs with all parity objectives under finite-memory strategies. We also establish optimal (exponential) memory bounds.