PhD Position at CNRS – Paris Saclay

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.


[1] Belta, C., Yordanov, B., & Gol, E. A. (2017). Formal Methods for Discrete-Time Dynamical Systems (Vol. 89). 
[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.

Supervisor: Antoine Girard ( <> / <>) 
Location: Gif-sur-Yvette (Paris area), France Laboratoire des Signaux et Systèmes - L2S ( <>) 
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

Comments are closed.