Calin teaches an EECI course in Paris, Saclay, Jan 14-18, 2018
The course is titled “Formal Methods in Control Design – from Discrete Synthesis to Continuous Controllers” and is co-taught with Antoine Girard. It is offered as part of the INTERNATIONAL GRADUATE SCHOOL ON CONTROL (IGSC) PROGRAM in the European Embedded Control Institute (EECI).
To register, follow this link:
http://eeciinstitute.web-events.net/registration/
The schedule is available here:
http://eeciinstitute.web-events.net/timetables/
Summary of the course
Antoine Girard
CNRS
https://sites.google.com/site/antoinesgirard/
Summary:
In control theory, complex models of continuous physical processes, such as systems of differential or difference equations, are usually checked against simple specifications, such as stability and set invariance. With the development and integration of cyber-physical and safety-critical systems, there is an increasing need for tools to design controllers for richer specifications. The main objective of this course is to present formal methods in control design. The key concept of these approaches is that of discrete abstraction (a.k.a. symbolic model), which is a finite-state dynamical system, obtained by abstracting continuous trajectories over a finite set of symbols. When the abstraction and the continuous dynamics are formally related by some behavioral relationship (e.g. simulation or bisimulation relations), controllers synthesized for the abstraction can be refined to certified controllers for the original continuous system. Moreover, since the abstractions are discrete, controllers can be synthesized automatically, using discrete synthesis techniques, for rich specifications such as languages or formulas of temporal logics. In this course, we will cover all aspects of formal methods in control design from the computation of discrete abstractions, to discrete synthesis and controller refinement.
Outline
1. The need for formal methods in control design
2. Systems, behaviors and relations among them
3. Discrete abstractions of continuous systems
3.1 Partition-based approaches
3.2 Lyapunov-based approaches
3.3 Abstraction via feedback
4. Controller synthesis using discrete abstractions
4.1 Finite temporal logic control
4.2 Language-guided control systems
4.3 Optimal temporal logic control