English
B F Bioinfo Formelle
Le projet "bioinfo formelle" vise à fournir des cadres rigoureux et formels pour la modélisation de la dynamique de systèmes biologiques complexes. En ce sens, ce projet contribue à la biologie des systèmes. Les particularités de ce domaine résident dans l'imprécision de l'observation de la réponse cellulaire et dans la construction ad-hoc des interactions entre entités biologiques à partir de données brutes. Le projet se focalise sur la formalisation du comportement du système, sur l'analyse des modèles, et sur l'identification des contraintes d'environnement et de synchronisation qui permettent au modèle d'avoir un comportement cohérent avec les observations.
  • Approche méthodologique Un modèle d'un système biologique n'est pas statique et doit évoluer afin de refléter l'évolution des connaissances sur le système. Pour éviter de relancer le processus entier de modélisation dès qu'une nouvelle information remet en question le modèle, il est souhaitable de maintenir, à chaque étape, non pas un modèle unique du système biologique, mais toutes les formalisations possibles compatibles avec les connaissances biologiques. Ainsi, une connaissance nouvelle n'est plus qu'une contrainte supplémentaire sur l'ensemble des modèles [1].

    Pour accélérer le processus de raffinement d'un modèle, nous cherchont à optimiser la sélection des expériences qui mèneront le plus rapidement possible à des spécifications les plus précises. La tâche est compliquée à cause des contraintes observationnelles (les variables du système ne sont pas toutes observables) et des contraintes d'opérabilité (certains états initiaux ne peuvent pas être choisis). Les modèles formels peuvent aider à la sélection des expériences les plus discriminantes. En particulier, nous avons montré que, sous certaines hypothèses fortes portant sur les contraintes expérimentales, le processus de sélection d'expériences conduit à un ensemble de modèles qui converge vers un ensemble de modèles observationnellement indiscernables.

  • Vérification de propriétés comportementales La vérification des propriétés dynamiques est indispensable car elle permet de vérifier la cohérence des modèles construits vis-à-vis de propriétés connues. Nous avons développé un outil SMBioNet qui permet de sélectionner automatiquement, à travers un usage intensif du model-checking, tous les paramétrages d'un graphe de régulation génique qui mènent à un comportement cohérent avec les connaissances ou hypothèses faites sur la dynamique du système, ces connaissances ou hypothèses étant exprimées dans un langage de logique temporelle. Nous avons également développé une approche basée sur la logique de Hoare et sur le calcul de la plus faible précondition pour générer les contraintes sur les valeurs des paramètres. Les spécifications du comportement observé jouent un rôle similaire à celui des programmes dans la logique de Hoare classique, et la plus faible précondition caractérise les paramétrages compatibles, exprimées comme des contraintes sur les paramètres [2a].

    Nous développons aussi une logique hybride linéaire Hyll dont le but est de faire des arbres de preuve directement sur le système formalisé, en évitant l'énumération de tous les paramètres possibles. Cette logique est désormais soutenu par coq et λ-Prolog pour faciliter la génération de la preuve [2b].

  • Relations entre la dynamique et la structure des interactions. Lorsqu'on modélise un système biologique, les connaissances généralement disponibles résident dans la structure du réseau de régulation (représenté par un graphe dont les arcs sont orientés et habituellement signés). Comme les paramètres cinétiques qui pilotent le comportement ne sont généralement pas connus, il faut s'intéresser aux informations sur la dynamique que l'on peut déduire à partir du graphe de régulation. Par exemple, il est maintenant bien connu (et prouvé dans de nombreux cadres de modélisation) que la présence d'une boucle de rétroaction positive est nécessaire pour l'existence de plusieurs points fixes. Nous étudions actuellement comment déterminer, à partir de la structure, un intervalle qui encadre le nombre de points fixes, ou encore la manière de distribuer les signes sur un graphe partiellement signé afin de maximiser le nombre de points fixes [3].

  • Informations chronométriques Les informations chronométriques (qui complètent la chronologie des événements en ajoutant des informations temporelles sur la durée des actions) sont souvent faciles à obtenir expérimentalement, mais rarement utilisées. Par exemple il peut être facile de connaître le temps nécessaire au système pour passer d'un état à son successeur ou bien pour passer d'un état à un autre à travers un chemin. Ces durées pourraient être utilisées pour contraindre les paramétrages admissibles. Nous développons donc des modèles formels hybrides pour les systèmes biologiques dans lesquels on peut manipuler formellement cette information chronométrique [4].
BF fait partie de l'équipe MDSC de l'I3S, une unité mixte de recherches commune à l'université de Nice et au CNRS.

Animation scientifique

type: École thématique CNRS
lieu: Ile de Porquerolles
date: du 6 au 10 juin 2016
type: Workshop I3S
lieu: Nice
date: du 4 au 7 novembre 2014
type: École thématique CNRS
lieu: Ile de Porquerolles
date: du 24 au 28 juin 2013
type: École thématique CNRS
lieu: Ile de Porquerolles
date: du 6 au 11 juin 2010