Symbolic Robustness Analysis and Synthesis of Timed Automata
We consider the robustness analysis of real-time systems modeled by timed automata, and the synthesis of robust-by-construction systems.
In robustness analysis (aka sensitivity analysis), the goal is to compute a bound on the timing imprecisions so that the model satisfies a given specification. We present a fully symbolic semi-algorithm for this problem using parametric data structures for LTL model checking, and present experimental results. Second, we consider controller synthesis for timed automata models where controllers are subject to either adversarially or probabilistically chosen perturbations in timings.
We present algorithms to synthesise controllers that ensure the system to be stable and to satisfy given omega-regular conditions.
Ocan Sankur currently holds a post-doc position at the Universite Libre de Bruxelles. His research interests include formal verification and synthesis for quantitative systems including real-time and probabilistic aspects. He obtained his PhD from Ecole Normale Superieure de Cachan in 2013, and bachelor's and master's degrees from Ecole Normale Superieure in 2010.