Habilitation defense
Mini workshop on quantitative models
The defense and its traditional pot will be followed in the afternoon by talks of two members of the jury:- 3pm Prakash Panangaden A canonical form for weighted automata and applications to approximate minimization
- 4pm Christel Baier Reasoning about cost-utility constraints in probabilistic models
Committee
- 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
Abstract
The importance of model checking was acknowledged by a Turing award in2007, 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.