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 threestep symbolic approach. First, we define a polyhedral partition of the state space and a finite set of feedback controllers driving the system among the regions of the partitions and use them to 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 symbols that maximizes the probability of following the satisfying run in the MDP. We present illustrative simulation results.

• Type: Journal
• Year: 2009
• Where: CDC
• Authors: Morteza Lahijanian, Sean B. Andersson, Calin Belta
• Keywords: CDC 2009, Control Systems, Corresponding Kripke Structure, Linear Temporal Logic, Threestep Symbolic Approach