Motion planning and control from temporal logic specifications with probabilistic satisfaction guarantees

We present a computational framework for automatic deployment of a robot from a temporal logic specification over a set of properties of interest satisfied at the regions of a partitioned environment. We assume that, during the motion of the robot in the environment, the current region can be precisely determined, while due to sensor and actuation noise, the outcome of a control action can only be predicted probabilistically. Under these assumptions, the deployment problem translates to generating a control strategy for a Markov Decision Process (MDP) from a temporal logic formula.We propose an algorithm inspired from probabilistic Computation Tree Logic (PCTL) model checking to find a control strategy that maximizes the probability of satisfying the specification. We illustrate our method with simulation and experimental results.