Control of Markov decision processes from PCTL specifications

We address the problem of controlling a Markov Decision Process (MDP) such that the probability of satisfying a temporal logic specification over a set of properties associated to its states is maximized. We focus on specifications given as formulas of Probabilistic Computation Tree Logic (PCTL) and show that controllers can be synthesized by adapting existing PCTL model checking algorithms. We illustrate the approach by applying it to the automatic deployment of a mobile robot in an indoor-like environment with respect to a PCTL specification.