Approches symboliques de la modélisation et de l’analyse des systèmes biologiques

L’inférence des réseaux de régulation de gènes reste un challenge majeur en biologie des systèmes malgré de nombreux efforts. Aujourd’hui, grâce aux données multi-omiques en cellules uniques, aux modèles dynamiques et stochastiques de la régulation génétique, et à la puissance de calcul disponible, de nouvelles approches telles que WASABI permettront de surmonter toutes les difficultés de ce défi.

Les modèles basés sur les réseaux métaboliques permettent de prédire le potentiel de production de molécules des organismes dans des conditions données. L’obtention de ces réseaux passe par une étape de complétion basée sur la résolution de problèmes d’optimisation combinatoire. Ce chapitre définit et décrit ces problèmes d'optimisation à partir de différents paradigmes de modélisation dynamique qui peuvent être associés à un système biologique.

Ce chapitre dresse un panorama des approches portant sur l’élaboration de modèles qualitatifs de réseaux de régulation, via des démarches s’apparentant au model-checking (pour l’analyse) et à la programmation logique (pour l’inférence). Nous nous attachons à étudier ce problème dans un contexte large-échelle, autrement dit avec potentiellement plusieurs centaines de composants interagissant.

Les modèles Booléens permettent de décrire des mécanismes de dysfonctionnement dans des maladies comme les cancers et d’anticiper les effets possibles de certaines drogues sur les dérégulations observées (mutations, surexpression de gènes, etc.). Cependant, les modèles développés sont génériques et ne sont pas spécifiques à un cancer, ou un patient. Nous présentons une méthodologie qui intègre des données omiques à ces modèles et permet ainsi de caractériser les différences de réponses aux traitements entre patients atteints d’un même cancer.

Ce chapitre présente le formalisme des réseaux booléens, leur relation avec d'autres modèles informatiques classiques, et leur adéquation pour la modélisation des systèmes biologiques. Le chapitre détaille la sémantique la plus permissive (MP) qui apporte une abstraction correcte des comportements quantitatifs, et conclut sur des aspects de complexité pour la vérification de propriétés dynamiques d'accessibilité et d'attracteurs.

Ce chapitre présente l'utilisation d'une logique calculatoire en biologie des systèmes, comme cadre unifié et sûr, adapté à la fois à la modélisation du comportement des systèmes biologiques et à l'expression et à la vérification de leurs propriétés. Ce chapitre offre une introduction à la logique linéaire ainsi qu'à l'utilisation du système Coq dans notre domaine.

La thèse de Church-Turing énonce qu’il n’y a qu’une seule notion universelle de calcul mécaniste, qui donc, d’une façon ou d’une autre, doit permettre de réconcilier le traitement de l’information en informatique et en biologie cellulaire. La preuve récente de Turing-complétude des réseaux de réactions chimiques continus sur un nombre fini d’espèces moléculaires, fournit les bases d’une telle réconciliation, sans construction artificielle, avec des capacités à la fois d’analyse des programmes chimiques naturels dans les cellules vivantes, et de synthèse de programmes chimiques artificiels dans des vésicules non vivantes. Ces résultats ouvrent un vaste champ de recherche fondamentale sur l’informatique analogique chimique de la cellule et des applications nouvelles en santé et environnement.

Ce chapitre démontre que la modélisation des réseaux de régulation biologiques est grandement facilitée par des méthodes symboliques de vérification formelle comme le model-checking et les preuves en logique de Hoare. Il présente une méthodologie complète de modélisation formelle où les approches logiques classiques du génie logiciel s'adaptent remarquablement efficacement au problème majeur de la modélisation des systèmes complexes: l'identification des paramètres.

Ce chapitre propose un langage de réécriture pour modéliser l’évolution d'ensembles d'instances de protéines et de leurs liaisons. Ce niveau de détail permet une représentation compacte grâce à une description locale des interactions et ouvre la voie à diverses abstractions. En particulier, nous utilisons ici cette structure pour calculer des propriétés locales des complexes protéiques.