Abstraction formelle de sémantiques quantitatives pour les modèles de réseaux d'interactions entre protéines dans les celluces. – AbstractCell

Nous proposons de développer des approximations et des algorithmes pour évaluer les propriétés des réseaux d'interactions entre protéines. Le comportement d'une cellule est régi par des interactions entre protéines: en effet, les protéines établissent des liaisons covalentes et s'activent les unes les autres afin de capter, de propager, et d'intégrer des messages. Ces réseaux d'interactions contrôlent l'apoptose (mort de la cellule), la mitose (duplication de la cellule), la spécialisation et le transport de la cellule. Lorsque ces réseaux ne jouent plus leur rôle, le cycle cellulaire est perturbé, ce qui peut conduire au développement d'un cancer. Il est très difficile de comprendre comment ces réseaux fonctionnent : d'une part, les concepteurs de modèles doivent contourner la complexité combinatoire de portions d'espèces chimiques, au lieu de suivre la concentration des espèces entières. Ainsi, la cohérence de notre approche est assurée, car par construction, les trajectoires des systèmes réduits sont des projections des trajectoires des systèmes initiaux. Enfin, nous allons proposer des algorithmes pour intégrer les systèmes différentiels ainsi obtenus, ainsi que des simulateurs stochastiques. L'originalité de notre approche repose sur l'utilisation des méthodes formelles. Celles-ci procurent un meilleur niveau de confiance (les approximations sont correctes par construction) et une meilleure compréhension des mécanismes d'approximation. Ceci permettra l'émergence d'outils de modélisation plus fiables et plus efficaces, qui sont nécessaires aux avancées futures en biologie systémique. concise des réseaux d'interactions, mais en plus on peut facilement adapter le modèle à de nouvelles conditions expérimentales. Cependant, il faut pouvoir calculer les propriétés (i.e. les trajectoires) de nos modèles, ce qui est le but de notre projet. Les propriétés d'un modèle sont formalisées par une sémantique qui peut être stochastique ou différentielle. Cependant, ces sémantiques ne passent pas à l'échelle des réseaux d'interactions entre protéines, soit parce que les populations de protéines sont trop grandes (de l'ordre de 106 protéines par exemple), soit parce que le nombre d'assemblages non isomorphes de protéines est trop important (de l'ordre 1030) . Nous proposons d'utiliser l'interprétation abstraite pour réduire la dimension de ces sémantiques. L'interprétation abstraite est une théorie unifiante des approximations entre sémantiques. Elle va nous permettre de concevoir des outils formels et automatiques pour construire des systèmes dynamiques avec un grain d'observation plus opportun : ces systèmes décrivent en effet la concentration de ces réseaux, qui est de nouvelles expériences. Aussi n'est-t-il pas évident de savoir quelles hypothèses sont compatibles entre elles. Il est pourtant primordial de proposer des modèles précis de ces réseaux d'interactions. En effet, ces modèles sont nécessaires non seulement pour faire des progrès en biologie, mais aussi pour fournir à l'industrie pharmaceutique des outils qui vont lui permettre de prévoir en amont l'échec de nouvelles thérapies potentielles. De plus, ces modèles sont nécessaires pour raisonner sur des thérapies plus complexes, comme celles combinant plusieurs protéines. Les modèles à base de règles de récritures permettent de décrire très efficacement les réseaux d'interactions entre protéines. En effet, elles recueillent des règles formelles qui décrivent les contextes (partiellement spécifiés) dans lesquels des réactions peuvent avoir lieu. Ainsi il n'est pas nécessaire de décrire entièrement les espèces chimiques qui réagissent. Non seulement, on obtient une description très due au très grand nombre de complexes protéiques pouvant se former. D'autre part, la connaissance des interactions n'est pas figée. De nouvelles hypothèses sont émises tandis que d'anciennes hypothèses sont réfutées par de nouvelles expériences. Aussi n'est-t-il pas évident de savoir quelles hypothèses sont compatibles entre elles. Il est pourtant primordial de proposer des modèles précis de ces réseaux d'interactions. En effet, ces modèles sont nécessaires non seulement pour faire des progrès en biologie, mais aussi pour fournir à l'industrie pharmaceutique des outils qui vont lui permettre de prévoir en amont l'échec de nouvelles thérapies potentielles. De plus, ces modèles sont nécessaires pour raisonner sur des thérapies plus complexes, comme celles combinant plusieurs protéines. Les modèles à base de règles de récritures permettent de décrire très efficacement les réseaux d'interactions entre protéines. En effet, elles recueillent des règles formelles qui décrivent les contextes (partiellement spécifiés) dans lesquels des réactions peuvent avoir lieu. Ainsi il n'est pas nécessaire de décrire entièrement les espèces chimiques qui réagissent. Non seulement, on obtient une description très concise des réseaux d'interactions, mais en plus on peut facilement adapter le modèle à de nouvelles conditions expérimentales. Cependant, il faut pouvoir calculer les propriétés (i.e. les trajectoires) de nos modèles, ce qui est le but de notre projet. Les propriétés d'un modèle sont formalisées par une sémantique qui peut être stochastique ou différentielle. Cependant, ces sémantiques ne passent pas à l'échelle des réseaux d'interactions entre protéines, soit parce que les populations de protéines sont trop grandes (de l'ordre de 106 protéines par exemple), soit parce que le nombre d'assemblages non isomorphes de protéines est trop important (de l'ordre 1030) Nous proposons d'utiliser l'interprétation abstraite pour réduire la dimension de ces sémantiques. L'interprétation abstraite est une théorie unifiante des approximations entre sémantiques. Elle va nous permettre de concevoir des outils formels et automatiques pour construire des systèmes dynamiques avec un grain d'observation plus opportun : ces systèmes décrivent en effet la concentration de portions d'espèces chimiques, au lieu de suivre la concentration des espèces entières. Ainsi, la cohérence de notre approche est assurée, car par construction, les trajectoires des systèmes réduits sont des projections des trajectoires des systèmes initiaux. Enfin, nous allons proposer des algorithmes pour intégrer les systèmes différentiels ainsi obtenus, ainsi que des simulateurs stochastiques. L'originalité de notre approche repose sur l'utilisation des méthodes formelles. Celles-ci procurent un meilleur niveau de confiance (les approximations sont correctes par construction) et une meilleure compréhension des mécanismes d'approximation. Ceci permettra l'émergence d'outils de modélisation plus fiables et plus efficaces, qui sont nécessaires aux avancées futures en biologie systémique.