Auditorium (IMAG)
7 May 2018 - 13h30
Formal methods for modelling and validation of biological models (Phd Defense)
by Alexandre Rocca from Verimag
Abstract: The focus of this thesis is the modelling and analysis of biological systems using formal methods. The dynamics of biological systems exhibit continuous behaviours but also abrupt changes.
Ordinary differential equations and hybrid dynamical systems are two mathematical formalisms that naturally model such dynamics. A crucial aspect of modelling is the determination of valid parameter values that enable to simulate the behaviour and reproduce experimental data sets. If no valid parameter values are found it becomes necessary to revise the model. An option is to replace one or several lumped parameters (parameters which represent a set of processes) by functions of time.
In this thesis, we first study the model revision problem on hybrid dynamical systems. To this aim, we propose a greedy scheme of optimal control methods based on occupation measures and convex relaxations. Then, we study how to characterize dynamical properties of a model using set-based simulations and reachability analysis. For this purpose, we propose two methods: the first one, which relies on Bernstein expansion, is an extension for hybrid dynamical systems of the reachability tool Sapo, while the other one uses Krivine-Stengle representations to perform the reachability analysis of polynomial ODEs. Finally, we also propose a methodology to generate hybrid dynamical systems modelling a class of experimental protocols.
The proposed methods are applied to different case studies. We first propose a model of haemoglobin production during the differentiation of an erythrocyte in the bone marrow. To develop this model, we first apply the Monte-Carlo based parameters synthesis, followed by the model revision to correctly reproduce the experimental data. We also propose a preliminary study of the effect of low dose Cadmium on glucose response at different steps of a rat growth. Finally, we apply the reachability analysis techniques for the validation on large parameters set of the existing iron homoeostasis model. We note the haemoglobin production process, as well as the glucose response system can be formalised within their experimental context as hybrid dynamical systems. Thus, they serve as proof of concept for the methodology of biological experimental protocols modelling.
Le jury de thèse sera constitué de:
- Pr. François Fages, directeur de recherche à l'INRIA Saclay.
- Pr. Ovidiu Radulescu, professeur à l'université de Montpellier.
- Pr. Hidde de Jong, directeur de recherche à l'INRIA Montbonnot.
- Dr David Safranek, professeur assistant à l'université de Masaryk (République Tchèque), département Machine Learning and Data Processing.
le Doodle du pt de thèse: https://doodle.com/poll/im57t7tbxxhcq8th
