A probabilistic approach for control of a stochastic system from LTL specifications

We consider the problem of controlling a continuous-time linear stochastic system from a specification given as a Linear Temporal Logic (LTL) formula over a set of linear predicates in the state of the system. We propose a three-step solution. First, we define a polyhedral partition of the state space and a finite collection of controllers, represented as symbols, and construct a Markov Decision Process (MDP). Second, by using an algorithm resembling LTL model checking, we determine a run satisfying the formula in the corresponding Kripke structure. Third, we determine a sequence of control actions in the MDP that maximizes the probability of following the satisfying run. We present illustrative simulation results.