logo-InriaRennes logo-equipeSumo

img-logoHDRNathalieBertrand2015 Contributions to the verification and control of timed and probabilistic models

img-NathalieBertrand-HDR2015 Nathalie Bertrand

chercheur Inria au sein de l'équipe SUMO

Habilitation defense - Monday 16th November 2015

The talk
The slides


The importance of model checking was acknowledged by a Turing award in 2007, and formal methods in general have proved extremely useful in the validation of hardware and software systems. These techniques are based on mathematical abstractions, and require models both of the
system, and of the requirements it has to meet. In order to faithfully represent real-life systems, models should incorporate several features including timing contraints, probabilities, unknown
parameters and imperfect information. This habilitation document reports on my contributions to formal methods for complex systems that combine several of these aspects. More specifically, the following problems are tackled: approximate determinization of timed automata, model checking and control for stochastic timed automata, synthesis for partially observable probabilistic systems, and parameterized verification of probabilistic systems. img-flecheHautHDRNathalieBertrand

The Jury

Christel Baier (TU Dresden)

Paul Gastin (ENS Cachan, LSV)

Thierry Jéron (Inria Rennes)

Marta Kwiatkowska (Oxford Univ.), reviewer

Catuscia Palamidessi (Inria Saclay)

Prakash Panangaden (McGill), reviewer

Sophie Pinchinat (Univ. Rennes 1)

Jean-Francois Raskin (ULB), reviewer


Defense's talk - Nathalie Bertrand (Inria)

(click to the image to start the video) - format MP4 - downloading version ; duration: 01:03:41 mn