Temporal Logic Model Predictive Control

Abstract:

In recent years, there has been increasing interest in formal synthesis of control strategies for dynamical systems. Unlike “classical” control problems, in which the specifications are stability or closeness to a reference point or trajectory possibly coupled with safety, temporal logics allow for richer specifications. The main challenge in formal synthesis is to abstract the dynamics of the system to a finite- state transition graph, for which automata game techniques can be used for control synthesis. The focus of this work is synthesis of optimal control strategies from temporal logic specifications. While some results exist for finite systems such as deterministic transition systems and Markov Decision Processes, this problem is largely open for systems with infinitely many states.

The main problem considered is the synthesis of an optimal control strategy for a discrete-time linear system constrained to satisfy a temporal logic specification over a set of linear predicates in its state variables. The cost is a quadratic function that penalizes the distance from desired state and control trajectories. The specification is a formula of syntactically co-safe Linear Temporal Logic (scLTL), which can be satisfied in finite time. It is assumed that the reference trajectories are only available over a finite horizon and a model predictive control (MPC) approach is employed. The MPC controller solves a set of convex optimization problems guided by the specification and subject to progress constraints. The constraints ensure that progress is made towards the satisfaction of the formula with guaranteed satisfaction by the closed-loop trajectory.