An additive cost approach to optimal Temporal Logic control

This paper presents a provably-correct Model Predictive Control (MPC) scheme for a discrete-time linear system. The cost is a quadratic that penalizes the distance from desired state and control trajectories, which are only available over a finite horizon. Correctness is specified as a syntactically co-safe Linear Temporal Logic (scLTL) formula over a set of linear predicates in the states of the system. The proposed MPC controller solves a set of convex optimization problems guided by the specification. The objective of each optimization is to minimize the quadratic cost function and a distance to the satisfaction of the specification. The latter part of the objective and the constraints of the problem guarantee that the closed-loop trajectory satisfies the specification, while the former part is used to minimize the distance from the reference trajectories.