Modélisation hybride, analyse et vérification des grands réseaux de régulation biologique

Informations générales
Nom
FIPPO-FITIME
Prénom
Louis
Diplôme
Thèse
Année
2016
Détails de la thèse/HDR
Université
Jury
Christine Froidevaux
Simon Givry
Anne Poupon
Sylvain SOLIMAN
Directeur (pour les thèses)
Olivier Roux
Carito Guziolowski
Résumé en français
Les Réseaux de Régulation biologique (RRB) sont couramment utilisés en biologie des
systèmes pour modéliser, comprendre et contrôler les dynamiques des différentes fonctions biologiques (différenciation, synthèse protéique, apoptose) au sein des
cellules. Ces réseaux sont enrichis des données expérimentales de plus
en plus nombreuses et disponibles qui renseignent sur les dynamiques des composants des RRB. L'analyse formelle de tels modèles se heurte rapidement à l'explosion combinatoire des comportements engendrés malgré le fait que les RRB offrent une représentation abstraite des systèmes biologiques.

Cette thèse traite de la modélisation hybride, de la simulation, de la vérification formelle et du contrôle des grands Réseaux de Régulation Biologique. Cette modélisation est effectuée grâce aux réseaux d'automates stochastiques, puis aux Frappes de Processus qui en sont une restriction, en intégrant des données de séries temporelles.

En premier lieu, cette thèse propose un raffinement des dynamiques par l'estimation
des paramètres stochastiques et temporels (délais) à partir des données de séries temporelles et l'intégration de ces paramètres dans les modèles en réseaux d'automates. Cette intégration permet de paramétrer les transitions entre les états du système. Puis, une analyse statistique des traces des simulations stochastiques est proposée afin de comparer les dynamiques des simulations à celles des données expérimentales.

En deuxième lieu, cette thèse développe une analyse statique par interprétation abstraite dans les réseaux d'automates permettant des approximations inférieures et supérieures très efficaces des propriétés d'accessibilité d'un point de vue quantitatif (probabilité et délai). Cette analyse permet de faire apparaître des composants critiques pour la satisfaction de ces propriétés.

Enfin, tirant avantage des analyses statiques développées pour l'accessibilité dans les réseaux d'automates, et de la puissance de la programmation logique (ASP),
cette thèse aborde le domaine du contrôle des systèmes en proposant
l'identification des transitions de bifurcation. Les bifurcations sont des transitions après lesquelles le système ne peut plus atteindre un état précédemment accessible.