Application de la logique de Hoare aux réseaux de régulation génétique - Bilan

Au fil des articles que j'ai postés sur ce blog ces derniers mois, j'ai tenté de présenter les notions importantes relatives à mon sujet de Master Recherche. Ces notions se trouvent au croisement de trois domaines :

  • la bio-informatique, qui est l'étude des procédés informatiques au sein des systèmes biologiques,
  • l'informatique théorique, pour ce qui est de la vérification de programmes,
  • la théorie des graphes, qui permet la modélisation de systèmes et l'utilisation d'outils de vérification.

Au cours de cet article bilan, je vais revenir rapidement sur les outils propres à ce sujet, en insistant sur leurs avantages et leurs faiblesses.

Le modèle de Thomas

Je vous avais tout d'abord présenté le modèle de Thomas, qui permet la modélisation d'un système de gènes en interactions à l'aide d'outils mathématiques discrets. Il consiste tout d'abord en l'élaboration d'un graphe de régulation génétique, qui se construit et se comprend de façon très intuitive, les nœuds représentant les gènes et les arcs leurs influences mutuelles. Lorsqu'une paramétrisation est définie relativement à un tel graphe (permettant de quantifier la force des interactions), on obtient un réseau de régulation génétique, qui est un outil définissant entièrement le système, tant au niveau de sa structure que de sa dynamique. Il est donc possible à partir d'un réseau de régulation de construire un graphe d'états-transitions, qui représente toutes les évolutions possibles du système.

La grande force du modèle de Thomas est d'abstraire les niveaux d'expression des gènes en les représentant par des valeurs discrètes (plutôt que par des valeurs continues de concentration des protéines), ce qui permet de compenser le manque de données quantitatives relatives aux systèmes étudiés. Cependant, ses deux principaux points faibles sont la taille du graphe d'états, qui subit une explosion combinatoire relative au nombre de gènes du système, et la définition de la paramétrisation, car il est souvent difficile de trouver la paramétrisation qui modélise le comportement que l'on souhaite étudier, parmi toutes les paramétrisations possibles sur un graphe de régulation.

L'étude par les logiques temporelles

Les logiques temporelles sont un premier outil d'étude des réseaux de régulation. Elles permettent de formuler, puis de vérifier à l'aide d'algorithmes, des propriétés sur un graphe d'états et sur les évolutions possibles du système qu'il représente. On peut par exemple étudier l'évolution au sein d'un graphe à partir d'un état, sur un chemin donné ou sur tous les chemins qui partent de cet état. Ces logiques ont été définies pour l'étude de systèmes automatiques et sont très bien adaptées à l'étude des graphes. Cependant, leur utilisation dans ce cadre nécessite la construction du graphe d'états, qui n'est pas possible pour des réseaux de grande taille pour des raisons de temps et de mémoire.

L'étude par la logique de Hoare

Le sujet de mon Master Recherche consiste en l'étude d'une alternative aux logiques temporelles pour l'étude des réseaux de régulation. Cette alternative repose sur la logique de Hoare, qui était à l'origine définie pour la vérification de programmes informatiques. Cette logique manipule des triplets de Hoare, qui permettent de caractériser un programme (composé d'une instruction ou d'une suite d'instructions) à l'aide d'une pré-condition et d'une post-condition. L'écriture d'un triplet de Hoare signifie que sous réserve que la pré-condition soit vraie avant l'exécution du programme, alors la post-condition sera vraie après. La définition et la manipulation de tels triplets permet de prouver le comportement de parties d'un programmes pour ensuite remonter au programme entier. On peut enfin définir l'outil de plus faible pré-condition sur un triplet de Hoare (pour un programme et une post-condition donnés) qui permet de lui donner un pouvoir d'expression maximal.

L'application de la logique de Hoare aux réseaux de régulation génétiques nécessite de voir un tel réseau de régulation comme un programme informatique. Cela est possible si on considère des instructions de type incrémentation ou décrémentation d'un gène. Si on définit un programme caractérisant une évolution du système et si on formule une post-condition souhaitée, on peut alors utiliser l'outil de plus faible pré-condition, qui indique si l'évolution et la post-condition données existent et sont compatibles, et qui donne des conditions nécessaires sur les niveaux d'expression initiaux des gènes et sur la paramétrisation du réseau. Cette approche (complémentaire à celle des logiques temporelles) possède le double avantage de ne nécessiter que le graphe de régulation pour fonctionner. Ainsi, on se passe de construire la paramétrisation et le graphe d'états, sur lesquels on parvient cependant à obtenir des informations.


Le stage d'application de mon Master Recherche consistera dans un premier temps en l'implémentation de cette application de la logique de Hoare, afin d'automatiser la recherche de propriétés sur la paramétrisation. Puis, dans un deuxième temps, il sera question d'ajouter la dimension temporelle à cette application à partir d'une définition des triplets de Hoare prenant déjà en compte cette dimension.

Comments