12. Optimal Temporal Logic Control

In this chapter, we focus on synthesis of an optimal control strategy for a PWA system constrained to satisfy a temporal logic specification. The specification is a formula of syntactically co-safe Linear Temporal Logic (scLTL). The cost is a quadratic function that penalizes the distance from desired state and control trajectories, which are called reference trajectories. To incorporate dynamic environments, we assume that the reference trajectories are only available over a finite horizon. The goal is to find a control strategy such that the trajectory of the closed-loop system originating from a given initial state satisfies the formula and minimizes the cost. We treat the temporal logic specifications as constraints in an optimal control problem and propose a model predictive control (MPC) solution, as the natural approach for such constrained problems.