M05 DELFT

In control theory, complicated dynamics such as systems of (nonlinear) differential equations are mostly controlled to achieve stability and to optimize a cost. In formal synthesis, simple systems such as finite state transition graphs modeling computer programs or digital circuits are controlled from specifications such as safety, liveness, or richer requirements expressed as formulas of temporal logics. With the development and integration of cyber physical and safety critical systems, there is an increasing need for computational tools for controlling complex systems from rich, temporal logic specifications. The main objective of this course is to present formal methods in control design. We will first present abstraction-based approaches. We will show how continuous dynamics can be formally related (using simulations, bisimulations, approximate bisimulations) to finite abstractions, how finite models can be controlled from temporal logic specifications, and how controllers for the abstractions can be refined into control strategies for the original continuous systems. We will then teach two optimization- based approaches. In the first, we will show how a constrained optimal control problem for a dynamical system with temporal logic specifications can be mapped to (mixed integer) linear or quadratic programs. In the second, we will enforce stability and temporal logic specifications using control barrier functions (CBF) and control Lyapunov functions (CLF). Finally, we will focus on systems with uncertain or unknown dynamics and will show how techniques from adaptive control and reinforcement learning can be used to enforce temporal logic requirements. Outline 1. The need for formal methods in control design 2. Systems, behaviors and relations among them 3. Abstractions of continuous systems 3.1 Discrete abstractions: partition-based approaches, Lyapunov-based approaches 3.2 Continuous abstractions 4. Abstraction-based controller synthesis 4.1 Safety, reachability, attractivity and recurrence specifications: fixed-point synthesis, quantitative and robust synthesis, compositional synthesis 4.2 Linear temporal logic specifications: Finite temporal logic control, language-guided control systems, optimal temporal logic control 5. Optimization-based synthesis 5.1 Synthesis based on temporal logic quantitative semantics 5.2 Synthesis based on control barrier functions (CBF) and control Lyapunov functions (CLF) 6. Formal synthesis for systems with partially known and unknown dynamics 6.1 Data-driven abstractions 6.2 Data-driven synthesis using CBF and CLF 6.3 Automata-based approaches to safe and interpretable reinforcement learning