Formal Methods for Controlling Dynamical Systems

Abstract

In control theory, complicated dynamics such as systems of (nonlinear) differential equations are mostly controlled to achieve stability. This fundamental property, which can be with respect to a desired operating point or a prescribed trajectory, is often linked with optimality, which requires minimization of a certain cost along the trajectories of a stable system. In formal methods, rich specifications, such as formulas of temporal logics, are checked against simple models of software programs and digital circuits, such as finite transition systems. With the development and integration of cyber physical and safety critical systems, there is an increasing need for computational tools for verification and control of complex systems from rich, temporal logic specifications. The current approaches to formal synthesis of (optimal) control strategies for dynamical systems can be roughly divided in two classes: abstraction-based and optimization-based methods. In this entry, we provide a short overview of these techniques.