Switching Control of Dynamical Systems from Metric Temporal Logic Specifications

Motivated by designing high-level planners for dynamical systems (such as mobile robots) to achieve complex tasks, we consider the synthesis of switching controllers of nonlinear dynamical systems from metric temporal logic (MTL) specifications. MTL is a popular logic that allows to specify timed properties of real-time reactive systems and hence is appropriate for describing the safe and autonomous operations of robotic systems in an uncertain and possibly adversarial environment. We provide constructive means for computing finite-state abstractions that preserve MTL properties for nonlinear systems, under a weak assumption that these nonlinear systems evolve continuously with respect to their initial conditions. We then provide conditions to ensure that the existence of a discrete strategy (obtained by solving a discrete synthesis problem) guarantees the existence of a switching strategy for controlling the continuous-time dynamical systems to satisfy a given MTL specification. We illustrate the results on a motion planning problem.