MéForBio - Méthodes Formelles pour la Bioinformatique

Responsable : Olivier Roux
Pôle(s) de recherche :
SDD
SLS

MeForBio (Méthodes Formelles pour la Bioinformatique) est une équipe de recherche en bioinformatique dans le domaine de la formalisation et du raisonnement automatique du traitement des données et des systèmes avec des caractéristiques temporelles. MeForBio est particulièrement orientée vers l'élaboration des cadres et méthodes qui modèlent et analysent des systèmes biologiques. L'équipe se focalise principalement sur :

  • La complexité de la dynamique des systèmes vivants
  • La simulation (non-déterministe) et le raisonnement (complet et exhaustif) sur un modèle décrivant un système biologique
  • La modélisation de la réponse à l'état stationnaire d'une perturbation sur un système biologique de grande taille
  • L'intégration des données expérimentales à haut débit dans des réseaux de régulation à grande échelle
  • La formalisation automatique des connaissances dans les bases de données de réactions biochimiques
Mots-clés méthodologiques :

méthodes formelles, model-checking, simulateurs stochastiques, résolution de contraintes, programmation logique

Mots-clés en Biologie des Systèmes :

réseaux de régulation génétiques, réseaux de signalisation, données de puces à ADN, données phospho-protéomiques, plan expérimental, bases de données des voies de signalisation

Sujets de recherche

Les principaux axes de recherche de MeForBio comprennent des méthodes pour proposer des analyses sur des modèles dynamiques et statiques des systèmes biologiques basés sur des modèles discrets, ainsi que des méthodes pour obtenir automatiquement des modèles discrets à partir des connaissances stockées dans des bases de données sur les régulations entre molécules.

 

Thématiques
Modélisation dynamique
Méthodes formelles pour l'étude de la dynamique des systèmes biologiques

Forts d'une expertise reconnue dans le domaine des méthodes formelles pour la modélisation, l'analyse, la vérification et le contrôle de systèmes dynamiques chronométriques, notre contribution consiste en l'application de ces méthodes aux systèmes biologiques pour aider les biologistes à analyser et à en déduire des propriétés dynamiques. Les principaux axes de recherche sont les méthodes de modélisation temporelles et hybrides (en plus des approches purement discrètes) afin de prendre en compte des délais d'évolution. Ces paramètres se révèlent cruciaux pour déterminer plus précisément les comportements réels des systèmes analysés. En outre, l'analyse statique d'une part, les approches par contraintes d'autre part, nous permettent de traiter de très grands systèmes.

Intégration de données de séries temporelles dans les modèles discrets, simulations et analyses d'accessibilité

Nous abordons la confrontation des grands réseaux de régulation avec des données expérimentales dépendant du temps. L'idée principale est de modéliser un système biologique avec les frappes de processus et de vérifier si diverses mesures de la variation du gène dans le temps peuvent être expliquées par le modèle. Une première approche de ce problème est de faire correspondre la simulation (stochastique) in-silico des gènes avec les mesures expérimentales. Pour cela, plusieurs paramètres du simulateur doivent être fixés en fonction d' hypothèses établies sur la méthode de discrétisation des données quantitatives, qui représentent un temps expérimental dans notre simulation. Une deuxième approche consiste à faire une analyse exacte d'accessibilité afin de vérifier exhaustivement s'il existe un ensemble de conditions dans le modèle qui nous permettent d'obtenir un certain scénario d'expression qualitatif. Ce thème propose donc de mélanger les approches de raisonnement stochastiques et exacts pour gérer l'intégration des données de séries temporelles dans les modèles discrets.


Modélisation statique
Raisonnement sur les réseaux de régulation biologiques de grande taille pour expliquer des mesures expérimentales à haut débit

Pour découvrir le dysfonctionnement sous-jacent d'un processus cellulaire, un état pathologique ou un processus biologique, les biologistes moléculaires effectuent souvent des mesures expérimentales à haut débit afin d'identifier un ensemble de molécules clés qui contrôlent la plupart des données expérimentales. Idéalement, nous aimerions être en mesure de proposer des plans expérimentaux optimaux (agir sur le comportement de molécules clés) qui nous permettront de comprendre et de contrôler le comportement cellulaire. Cette recherche même de la conception de l'expérience idéale peut être abordée en utilisant des algorithmes sur une représentation discrète et qualitative du système biologique. Nous avons montré dans des travaux précédents que le raisonnement sur ??une représentation discrète, plutôt que continue, des informations d'un système biologique à grande échelle nous permet d'intégrer des données à haut débit, connues pour être hétérogènes, incomplètes et bruyants. Les problèmes combinatoires et de calcul derrière l'intégration de données à haut débit sont difficiles et nécessitent la combinaison de deux aspects principaux : la modélisation de la connaissance des effets mécaniques et l'exploration rapide et complète de l'espace de solutions des problèmes à variables discrètes.

Dans ce contexte , nous avons modélisé la transcription et la signalisation des événements moléculaires à l'aide de contraintes discrètes et résolu le système de contraintes en utilisant des méthodes exhaustives (sur la base de diagrammes de décision, graphes de dépendance, programmation par ensemble réponse). Nos résultats sont capables d'étudier : (1) les prédictions du système, définis comme l'intersection de tous les modèles cohérents possibles, (2) les causes d'une perturbation du système et la robustesse des prédictions, (3) l'optimisation dans l'espace des modèles incompatibles et (4) l'optimisation, dans l'espace des modèles booléens, qui minimise l'erreur entre les données à haut débit et les réseaux de signalisation qualitatifs. Ces méthodes concernent des problèmes de calcul difficiles et proposent une solution pour modéliser des systèmes biologiques à l'état d'équilibre ou leur réponse immédiate.

 


Formalisation de la Connaissance Biologique
Formalisation automatique des connaissances dans les bases de données de réactions biochimiques

Actuellement de nombreuses bases de données électroniques et en ligne stockent la connaissance sur les régulations biologiques. Toutefois , afin de modéliser cette information et de raisonner sur elle, la connaissance existante doit être formalisée et limitée à un vocabulaire spécifique qui, plus tard, peut être interprété et résolu en utilisant des cadres spécifiques. Le vocabulaire qui nous intéresse n'est pas fondée sur des données quantitatives précises (coûteux et difficiles à obtenir et reproduire), mais plutôt sur des données discrètes et qualitatives. Dans un premier travail nous avons proposé une méthode permettant d'obtenir automatiquement des graphes d'interactions à partir d'une base de données publique, tels que l'Interaction Pathways Database. Des résultats de travaux en cours proposent une liste de motifs (réactions biochimiques) qui peuvent être extraits automatiquement à partir de dépôts publics et traduits en contraintes discrètes ou en actions de régulation, nous permettant de modéliser ce système dans un deuxième temps. Nous pouvons alors simuler et raisonner automatiquement sur les modèles obtenus de manière efficace et exhaustive avec des frameworks comme les Frappes de Processus ou la programmation par ensemble réponses.