Postdoctoral position:
Formal Controller Synthesis for Complex Systems
using Lifting Functions
Supervisors: Antoine Girard (antoine.girard@l2s.centralesupelec.fr)
Thiago Alves Lima (thiago.alveslima@l2s.centralesupelec.fr)
Location: Laboratoire des Signaux et Syst`emes – L2S
CentraleSup´elec – CNRS – Univ. Paris-Saclay
Gif-sur-Yvette, France
Dates: 1 year – starting anytime between June and November 2024.
Salary: 3200 euros monthly, gross salary.
Context
Real-world dynamical systems such as self-driving cars or walking robots exhibit complex (e.g., nonlinear
or hybrid) behaviors that often defy traditional linear modeling approaches. For safety-critical applications,
it is crucial to synthesize provably correct controllers to avoid catastrophic events. However, the complex
nature of such systems poses challenges for the synthesis of provably-correct controllers.
In recent decades, a major research effort has been devoted to using formal methods to verify and
synthesize controllers for these systems [1]. One popular approach — called hybridization — consists in
(over-)approximating the system dynamics by a piece-wise affine (PWA) system [2]. The PWA system
then simulates the original dynamics. As a result, a controller that guarantees the satisfaction of some
specifications for the PWA system is guaranteed to satisfy the same specifications for the original system.
The strength of such an approach lies in the fact that control methods for PWAs (such as the one developed
in [3]) can then be used for complex systems.
Tangentially, finite-dimensional Koopman approaches have been proposed to approximate discrete-time
nonlinear systems [4, 5, 6]. Such methods involve lifting the state of the system into a higher-dimensional
state space via a lifting function and constructing a linear representation of the system in this higher-
dimensional space. While these methods were originally developed for autonomous systems, generalizations
to systems with inputs have been considered as well [7, 8, 9], allowing to use tools for the control of linear
systems to control nonlinear ones. In a similar spirit, “almost linear” representations such as linear fractional
transformations (LFTs) and, more recently, differential algebraic representation (DARs) leveraged nonlinear
changes-of-variables for the control of continuous-time dynamical systems [10].
Objective and work description
Recently, a simulation relation between discrete-time lifted systems with inputs was proposed in [9], allow-
ing to combine formal methods with finite-dimensional Koopman approaches. However, some important
questions deserve to be further enlightened. This research project will investigate the following ones:
• While lifted systems considered in [9] were introduced to simulate discrete-time nonlinear systems,
this research project will first extend the setting to continuous-time nonlinear systems. Then, possible
extensions to nonlinear switched systems and hybrid systems [11] will be investigated as well.
• PWA lifted systems (i.e., PWA dynamics in the lifted domain) will be considered. This would unify
hybridization and finite-dimensional Koopman approaches. The computational complexity of synthe-
sizing a controller typically grows with the number of pieces for a PWA system, and with the lifting
1
dimension for a linear lifted system. One hope of this research is to show that with a low-dimensional
lifting and a PWA system with only a few pieces, one can get the best of the two worlds and obtain
better performance than with hybridization only or with lifting only.
• The notions of approximate (bi)simulation relations [12] between lifted systems will be investigated as
well, making the approach more robust.
Overall, this research project will contribute to the development of theoretic and algorithmic tools for
the control of complex safety-critical systems.
References
[1] Paulo Tabuada. Verification and control of hybrid systems: a symbolic approach. Springer Science &
Business Media, 2009.
[2] Antoine Girard and Samuel Martin. Synthesis for constrained nonlinear systems using hybridization
and robust controllers on simplices. IEEE Transactions on Automatic Control, 57(4):1046–1051, 2011.
[3] Lucas N Egidio, Thiago Alves Lima, and Rapha¨el M Jungers. State-feedback abstractions for optimal
control of piecewise-affine systems. In 2022 IEEE 61st Conference on Decision and Control (CDC),
pages 7455–7460. IEEE, 2022.
[4] Matthew O Williams, Ioannis G Kevrekidis, and Clarence W Rowley. A data–driven approximation
of the koopman operator: Extending dynamic mode decomposition. Journal of Nonlinear Science,
25:1307–1346, 2015.
[5] Sriram Sankaranarayanan. Change-of-bases abstractions for non-linear hybrid systems. Nonlinear Anal-
ysis: Hybrid Systems, 19:107–133, 2016.
[6] Zheming Wang, Rapha¨el M Jungers, and Chong Jin Ong. Computation of invariant sets via immersion
for discrete-time nonlinear systems. Automatica, 147:110686, 2023.
[7] Joshua L Proctor, Steven L Brunton, and J Nathan Kutz. Generalizing koopman theory to allow for
inputs and control. SIAM Journal on Applied Dynamical Systems, 17(1):909–930, 2018.
[8] Haldun Balim, Antoine Aspeel, Zexiang Liu, and Necmiye Ozay. Koopman-inspired implicit backward
reachable sets for unknown nonlinear systems. IEEE Control Systems Letters, 2023.
[9] Antoine Aspeel and Necmiye Ozay. A simulation preorder for koopman-like lifted control systems. arXiv
preprint arXiv:2401.14909, 2024.
[10] Thiago Alves Lima, Diego de S. Madeira, Valessa V. Viana, and Ricardo C.L.F. Oliveira. Static output
feedback stabilization of uncertain rational nonlinear systems with input saturation. Systems & Control
Letters, 168:105359, 2022.
[11] R. Goebel, R.G. Sanfelice, and A.R. Teel. Hybrid Dynamical Systems: Modeling, Stability, and Robust-
ness. Princeton University Press, 2012.
[12] Antoine Girard and George J Pappas. Approximation metrics for discrete and continuous systems.
IEEE Transactions on Automatic Control, 52(5):782–798, 2007.
