Soutenance de thèse de Alexandre Rocca / BCM le...

Alexandre ROCCA de l’équipe BCM soutiendra sa thèse le lundi 7 mai à 13h30 sur le thème :

« Méthodes formelles pour la modélisation et la validation de modèles biologiques »

“ Formal methods for modelling and validation of biological models ”

Direction de Thèse :
- Mme Thao Dang, Directrice de Recherche CNRS, laboratoire Verimag , Grenoble Directeur
- M. Eric Fanchon, Chargé de Recherche Université Grenoble Alpes, laboratoire TIMC-IMAG, Grenoble CoDirecteur

Membres du jury :
- Pr François Fages, Directeur de Recherche à l’INRIA Saclay, Rapporteur
- Pr Ovidiu Radulescu, Professeur, DIMNP Université de Montpellier 2, Rapporteur
- Pr Hidde de Jong, Directeur de Recherche à l’INRIA Montbonnot, Examinateur
- Dr David Safranek, Professeur Assistant à l’Université de Masaryk, Département "Machine Learning and Data Processing", République Tchèque , Examinateur

Lieu : Auditorium du bâtiment IMAG, Université Grenoble Alpes, 700 Avenue centrale, 38401 Saint Martin d’Hères

— 

Mots-clés : Analyse d’atteignabilité, systèmes multi-échelles, systèmes biologiques, modélisation

Résumé : L’objectif de cette thèse est la modélisation et l’étude de systèmes biologiques par l’intermédiaire de méthodes formelles. Les systèmes biologiques démontrent des comportements continues mais sont aussi susceptibles de montrer des changements abruptes dans leur dynamiques. Les équations différentielles ordinaires, ainsi que les systèmes dynamiques hybrides, sont deux formalismes mathématiques utilisés pour modéliser clairement de tels comportements. Un point critique de la modélisation de systèmes biologiques est la recherche des valeurs des paramètres du modèle afin de reproduire de manière précise un ensemble de données expérimentales. Si aucun jeux de paramètres valides n’est trouvé, il est nécessaire de réviser le modèle. Une possibilité est alors de remplacer un paramètre, ou un ensemble de paramètres, définissant un processus biologique par une fonction dépendante du temps.

Dans le cadre de cette thèse, nous exposons tout d’abord une méthode pour la révision de modèles hybrides. Pour cela, nous proposons une approche gloutonne appliquée à une méthode de contrôle optimal utilisant les mesures d’occupations et la relaxation convexe. Ensuite, nous étudions comment analyser les propriétés dynamiques d’un modèle à temps discret en utilisant la simulation ensembliste. Dans cet objectif, nous proposons deux méthodes basées sur deux outils mathématiques. La première méthode, qui se repose sur les polynômes de Bernstein, est une extension aux systèmes dynamiques hybrides, de l’outil de calcul ensembliste Sapo. La seconde méthode utilise les représentations de Krivine-Stengle pour permettre l’analyse d’atteignaiblité de systèmes dynamiques polynomiaux. Enfin, nous proposons aussi une méthodologie pour générer des systèmes dynamiques hybrides modélisant des protocoles biologiques expérimentaux.

Les méthodes précédemment proposées sont appliquées sur divers études biologiques. Nous étudions tout d’abord un modèle de la production d’hémoglobine durant la différentiation des érythrocytes dans la moelle. Pour permettre la construction de ce modèle, nous avons dans un premier temps généré un ensemble de jeux de paramètres valides à l’aide d’une méthode de type Monte-Carlo. Dans un second temps, nous avons appliqué la méthode de révision de modèle afin de reproduire plus précisément les données expérimentales. Nous proposons aussi un modèle préliminaire des effets à faibles doses du Cadmium sur la réponse du métabolisme à différentes étapes de la vie d’un rat. Enfin, nous appliquons les techniques d’analyse ensembliste pour la validation d’hypothèses sur un modèle d’homéostasie du fer dans le cas où des paramètres varient dans de larges intervalles. Dans cette thèse, nous montrons aussi que le protocole associé à l’étude de la production d’hémoglobine, ainsi que le protocole étudiant l’intégration du Cadmium durant la vie d’un rat, peuvent être formalisés comme des systèmes dynamiques hybrides, et servent ainsi de preuves de concepts pour notre méthode de modélisation de protocoles expérimentaux.

— 

Key-words : Reachability analysis, multi-scales systems, biological systems, modelisation

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.


Laboratoire TIMC-IMAG, Domaine de la Merci, 38706 La Tronche Cedex

CNRS
UGA
ENVL
Grenoble INP
Mentions Légales