PhD Position: Efficient synthesis of controllers using symbolic models
Context and Objectives
Cyber-physical systems (CPS) consist of computational elements monitoring and controlling physical entities.
The main objective of the PROCSYS project is to propose a general framework for the design of programmable
CPS that will allow engineers to develop advanced functionalities using a high-level language for specifying
the behaviors of a CPS while abstracting details of the dynamics. Controllers enforcing the specified behaviors
will be generated from a high-level program using an automated model-based synthesis tool. Correctness of the
controllers will be guaranteed by following the correct by construction synthesis paradigm through the use of
symbolic control techniques [1,2]: the continuous physical dynamics is abstracted by a symbolic model, which
is a discrete dynamical system; an interface consisting of low-level controllers is designed such that the
physical system and the symbolic model behaves identically; a high-level symbolic controller is then
synthesized automatically from the high-level program and the symbolic model.
Work description
We will develop efficient controller synthesis techniques based on incremental exploration of the dynamics of
the symbolic model, which can be computed on the fly while synthesizing the controller. This has been the
approach developed in our preliminary work [3], which has demonstrated significant improvements in terms of
scalability for safety specifications and deterministic symbolic models. The main idea is to define priorities
on the transitions of the symbolic model and explore the transitions with higher priority first. The
transitions of lower priority are only explored if the control specification cannot be met with the former
transitions. In the PhD thesis, we will develop efficient controller synthesis algorithms, which extend the
work above in the following directions:
1. Non-deterministic symbolic models, extending the applicability of the approach to a broad class of systems
2. General specifications defined in the high-level language developed within the PROCSYS project,
describing rich and complex behaviors
3. Additional synthesis objectives (timing constraints, quantitative performance criteria, robustness)
Applications to case studies, e.g. in the field of autonomous driving will be considered.
Background of the candidate
The candidate must hold a Master in control theory, applied mathematics or computer science with a strong
mathematical background. A prior experience in the area of hybrid systems is recommended. Programming skills
are also needed.
References
[1] Belta, C., Yordanov, B., & Gol, E. A. (2017). Formal Methods for Discrete-Time Dynamical Systems (Vol. 89).
Springer.
[2] Tabuada, P. (2009). Verification and control of hybrid systems: a symbolic approach. Springer Science &
Business Media.
[3] Girard, A., Gössler, G., & Mouelhi, S. (2016). Safety controller synthesis for incrementally stable
switched systems using multiscale symbolic models. IEEE Transactions on Automatic Control, 61(6), 1537-1549.
https://hal.archives-ouvertes.fr/hal-01197426v2/document
Supervisor: Antoine Girard (Antoine.Girard@l2s.centralesupelec.fr <mailto:Antoine.Girard@l2s.centralesupelec.fr> / https://sites.google.com/site/antoinesgirard/ <https://sites.google.com/site/antoinesgirard/>)
Location: Gif-sur-Yvette (Paris area), France Laboratoire des Signaux et Systèmes - L2S (http://www.l2s.centralesupelec.fr <http://www.l2s.centralesupelec.fr/>)
Institution: CNRS – CentraleSupélec – Univ. Paris-Sud – Univ. Paris-Saclay
Duration: Three years, starting fall 2018
Position fully funded by European project (ERC consolidator) PROCSYS
Master of Science in Informatics at Grenoble (MOSIG 2016-2020)
