Formal synthesis of control strategies for dynamical systems
Calin A. Belta · 2016
In formal verification, the goal is to check whether the executions of a system satisfy a rich property, usually expressed as a temporal logic formula. While the formal verification problem received a lot of attention from the formal methods community for the past thirty years, the dual problem of formal synthesis, in which the goal is to synthesize or control a system from a temporal logic specification, has not received much attention until recently. This tutorial paper provides a self-contained exposition on formal synthesis of control strategies for a particular class of dynamical systems. Central to this paper is the concept of transition system, which is shown to be general enough to model a wide variety of dynamical systems. It is shown how abstractions can be constructed by using simulation and bisimulation relations. The control specifications are restricted to formulas of Linear Temporal Logic (LTL) and some fragments of LTL, which are introduced together with the corresponding automata and the automata games used to generate control strategies for finite transition systems. At the end, we show how such control strategies can be adapted to discrete-time piecewise affine systems. Several examples are provided throughout the paper.