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

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

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.