Verification of indefinite-horizon POMDPs

Markov decision processes are the model to reason about systems involving nondeterministic choice and probabilistic branching. They have widespread usage in planning and scheduling, robotics, and formal methods. In the latter, the key verification question is whether for any policy, i.e., for any resolution of the nondeterminism, the probability to reach the bad states is below a threshold [3]. The verification question may be efficiently analysed using a variety of techniques such as linear programming, value iteration, or policy iteration, readily available in mature tools such as Storm [15], Prism [22] and Modest [13]. However, those verification results are often overly pessimistic.