Formal methods for controller synthesis

Lyapunov theory gives a way to describe at a high level some properties of trajectories of controlled dynamical systems, and formal methods provide powerful tools to work with these properties, when they are expressed as predicates in a (timed) modal logic. 
These predicates and the relationships between them amount to a discrete or hybrid model of the control system. With such models, formal methods make it is possible to check whether a control system verifies some logic formula, and it even allows the synthesis of control strategies that always satisfy a set of formal requirements. 
This results in control strategies that come with theoretical guarantees. While these guarantees should not be taken for granted on the real system (since models are always inaccurate to some degree), they can make it easier to predict, understand and modify the behavior of control systems. Furthermore, the logic formulas used for synthesis are more expressive than classical task descriptions, hence the approach is a way to extend classical motion planning algorithms. 
In this line of research, we proposed algorithms based on timed automata abstractions for verification and reactive synthesis with linear or nonlinear control systems. 
They are presented in the following articles:

• Bouyer, P., Markey, N., Perrin, N. and Schlehuber-Caissier, P. (2017), Timed-automata abstraction of switched dynamical systems using control invariants, Real-Time Systems, Vol. 53 (3), pp. 327-353
• Bouyer, P., Markey, N., Perrin, N. and Schlehuber-Caissier, P. (2015), Timed-automata abstraction of switched dynamical systems using control funnels, Formal Modeling and Analysis of Timed Systems: 13th International Conference (FORMATS 2015), pp. 60-75.