Correct-by-construction policies for POMDPs

Summary. In this extended abstract, we discuss how to compute policies with finite memory---so-called finite-state controllers (FSCs)---for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications. In particular, for a POMDP M and a specification ϕ, we want to solve the decision problem whether there is a policy σ for M with k memory states, such that ϕ is satisfied by M and σ (Mσ |= ϕ). The underlying method is achieved via a marriage of formal verification and artificial intelligence. The key insight is that computing (randomized) FSCs on POMDPs is equivalent to---and computationally as hard as---synthesis for parametric Markov chains (pMCs). The parameter synthesis problem is to decide whether for a parametric Markov chain (pMC) M and a specification ϕ there is a parameter instantiation u such that in the Markov chain (MC) induced by u the specification is satisfied (M[u] |= ϕ). The correspondence---depicted in Figure 1---allows to utilize efficient tools for synthesis in pMCs to compute correct-by-construction FSCs on POMDPs.