About me
I am currently a postdoctoral researcher at ISIR, on Jussieu campus, under the supervision of
Nicolas Perrin-Gilbert, since 2022.
I have been a PhD student at SUMO under the supervision of
Thierry Jéron,
Nicolas Markey and David Mentré from 2018 to 2022.
My research focuses on formal methods for real-time systems.
I defended my thesis on March 11 2022 (
manuscript,
defence slides).
Research projects
Symbolic computation of the maximal permissiveness of timed automata
This is one of my two phd project, under the supervision of Thierry Jéron, Nicolas Markey and David Mentré.
In this project, we model the perturbation of delays in Timed Automata to compute how much we can be permissive during a run.
We model it with a two-player game, where a first player proposes an action and an interval of delay (instead of a delay in the classic semantics) and the opponent chooses the delays taht will really apply.
Our aim is to compute, given an initial location, the optimal strategy of the player to maximize the minimum of the size of all the intervals he have to propose during a run to reach a goal location.
We proposed two algorithms to compute this strategy for all valuations, with a permissiveness function that depend on the valuations.
The first algorithm compute the permissiveness function and the second one the binary and levelled permissiveness functions, that respectivelly computes:
- whether the permissiveness of a configuration is greater than a threshold (binary)
- in which interval the permissiveness of a configuration belongs to (levelled), given a set of finite distincts intervals of R+
I implemented theses two algorithms in python, based on PPLPY, for linear timed Automata.
This implementation is maintained in this gitlab page
Py-Symb-robustness. It was previously maintained in
MERCE-FRA (github). Both are under GPL licence.
Numerical computation of the maximal permissiveness of timed automata
This is my second phd project, under the supervision of Thierry Jéron, Nicolas Markey and David Mentré.
This project consists in computing the permissiveness with a double backtrack algorithm that samples the set of possible intervals and possible delays.
I have proposed an algorithm, detailled in the 6th chapter of my PHD thesis.
This algorithm is implemented in python, based on networkx library.
It was first maintened on the github of MERCE (
MERCE-FRA (github)).
It is now maintained on my gitlab page (
Py-Num-robustness).
Both implementation are under GPL Licence.
Efficient implementation of control strategy for hybrid systems
In my post-doctoral project, in collaboration with Nicolas Perrin-Gilbert and Philipp Schlehuber, our aim is to compute the optimal strategy to reach a goal, for systems of timed automata using some stopwatches.
We use parameters to optimize our goal by minimizing the global time elapsing during the run and use an SMT-based method to make our model more realistic for our application: robotic collision avoidance.
This project is implemented in python (not public yet, coming soon after submission).
