Application de la logique de Hoare aux réseaux de régulation génétique - Article 5 : Les logiques temporelles

Ce dernier article sera l'occasion de vous présenter une autre méthode permettant l'analyse des réseaux de régulation génétique : il s'agit des logiques temporelles, qui permettent d'étudier le graphe d'états déduit d'un réseau de régulation génétique. Comme je l'ai présenté dans mon précédent article, l'approche par la logique de Hoare permet de déduire des informations sur la paramétrisation et l'état des gènes pour un scénario donné. Les logiques temporelles constituent une autre approche, qui permet d'étudier les évolutions possibles dans le graphe d'états.

Introduction : les différentes logiques

Les deux logiques les plus connues sont la logique modale et la logique du premier ordre. La logique modale est la logique 'standard' qui permet de formuler des assertions sur des paramètres. Par exemple : « n est pair ⇒ f(n) ≥ 0 » est une formule de logique modale, car les paramètres (n et f) sont connus en dehors de la formule. La logique du premier ordre est l'extension de la logique modale qui permet l'utilisation de variables muettes à l'aide de quantificateurs logiques (d'universalité et d'existence). Une formule en logique du premier ordre s'écrit comme une succession finie de quantifications logiques suivie d'une assertion en logique modale. Par exemple : « ∀ x ∈ R, ∃ y ∈ R, y = x² » est une formule en logique modale car les variables x et y sont muettes (elles n'ont pas d'existence propre en dehors de la formule, et sont uniquement “instanciées” par les quantificateurs).

Cependant, ces deux types de logiques ne permettent de décrire simplement que des entités statiques. L'étude d'entités en évolution reste possible par l'introduction de variables représentant le temps, mais cette technique nécessite l'utilisation d'un formalisme assez lourd et peu pratique : il faudrait à tout moment utiliser des variables muettes permettant de quantifier l'évolution du système. Ces variables peuvent être continues pour représenter un temps physique (un événement peut avoir lieu entre tel et tel instant), ou discrètes pour représenter un temps logique (une succession d'événements ordonnés dans un temps qui n'est en revanche pas quantifié).

Les logiques temporelles ont été introduites afin de proposer un formalisme qui permette d'éviter cette lourdeur. Elles ont été conçues spécialement pour étudier des systèmes dynamiques (capables d'évoluer) modélisés à partir de graphes. Elles permettent d'exprimer des assertions sur l'évolution d'un système en considérant les différents chemins possibles dans le graphe qui modélise ce système. Le temps qu'elles représentent est donc logique (il consiste en une succession d'instants) mais des extensions permettant de modéliser aussi l'évolution d'un temps continu sont aussi utilisées, mais ne seront pas traitées ici.

Présentation des logiques CTL et LTL

Les logiques temporelles que je vais présenter ici s'appliquent à des graphes dont les états sont étiquetés par des propriétés (aussi appelés : structures de Kripke). Plus particulièrement, les logiques que je vais présenter considèrent, pour un état donné du graphe, l'arborescence des chemins qui sortent de cet état, c'est-à-dire l'ensemble de tous les chemins qui partent de l'état considéré. On peut vouloir par exemple prouver des propriétés de sûreté (« Une propriété n'est jamais vérifiée » ou encore « Ces deux propriétés n'arrivent jamais à la suite ») ou de vivacité (« Une propriété finira toujours fatalement par arriver »).

Sur l'arborescence des chemins portant d'un état, la logique LTL formule des propriétés sur un chemin choisi. Sur ce chemin particulier, on définit les modalités suivantes :

  • Xφ (pour neXt) : φ sera vérifiée dans l'état suivant (i.e. le deuxième état du chemin).
  • φUψ (pour Until) : φ sera vérifiée jusqu'à ce que ψ soit vérifiée.

On ajoute aussi les modalités suivantes, très souvent utilisées, et définies à partir des deux modalités précédentes :

  • Fφ (pour Fatalement) : φ sera vérifiée un jour.
  • Gφ (pour Globalement) : φ sera toujours vérifiée.


La logique CTL, au contraire, s'intéresse à l'ensemble des chemins qui débutent dans l'état considéré (donc à l'arborescence complète). On retrouve les mêmes modalités que pour pour LTL, avec des quantifications, à savoir, si δ représente la modalité X ou U :

  • Aδ est vraie ssi δ est vraie pour tous les chemins.
  • Eδ est vraie ssi il existe un chemin tel que δ soit vraie.

Les formules sont donc : AXφ, EXφ, AφUψ, EφUψ, auxquelles on peut aussi ajouter les modalités de globalité et fatalité avec quantificateurs.

Afin de donner quelques exemples simples, on considère les arbres d'exécution ci-dessous. Sur le chemin mis valeur sur le premier, les formules LTL suivantes (par exemple) sont vérifiées : NP et PUQ. Sur l'ensemble des chemins de la seconde arborescence, les formules CTL suivantes sont vraies : ANP et EFQ.

Exemple d'arborescence pour LTL Exemple d'arborescence pour CTL

Notons enfin que ces deux logiques ont des pouvoirs d'expression strictement incomparables. Cela signifie que toutes les formules d'une de ces logiques ne peuvent pas être exprimées à l'aide des formules de l'autre. Afin de combler ce manque, la logique CTL* a été introduite : on peut la considérer comme le regroupement de LTL et CTL car elle permet l'utilisation des modalités X et U (ainsi que G et F) avec ou sans les quantificateurs A et E dans une même formule.

Application au modèle de Thomas

Pour mémoire, la modélisation d'un système de gènes en interaction via le modèle de Thomas consiste en la construction d'un réseau de régulation génétique, qui contient toutes les informations relatives à la dynamique du système. À partir de ce réseau de régulation, on est en mesure de construire un graphe d'états qui représente toutes les configurations que peut prendre ce système et les évolutions possibles entre ces configurations.

On peut naturellement immédiatement appliquer les logiques temporelles au graphe d'états déduit du réseau de régulation génétique. Cela permet de d'obtenir un certain nombre d'informations sur le système modélisé, par exemple l'accessibilité de certains états selon le point de départ choisi, ou encore la présence de cycles ou d'attracteurs.

Cependant, cette méthode peut présenter certaines limites. Tout d'abord, la création du graphe d'états à partir du réseau de régulation génétique est très coûteuse en temps et en mémoire. En effet, ce graphe subit une explosion combinatoire du nombre d'états lorsqu'on augmente la taille du graphe de régulation. De plus, la construction du graphe d'états nécessite d'avoir choisi une paramétrisation ; or ce choix est souvent difficile car il existe en général un grand nombre de paramétrisation possibles. Il est souvent nécessaire d'en tester une bonne partie avant de trouver le réseau de régulation qui modélise le comportement que l'on cherche à étudier. Ce sont ces inconvénients qui ont poussé aux tentatives d'utilisation de la logique de Hoare que j'avais traité dans l'article précédent.

Références

Le livre Vérification de logiciels : techniques et outils du model-checking, de Ph. Schnoebelen, B. Bérard, M. Bidoit, F. Laroussinie et A. Petit, constitue une approche pédagogique et détaillée des logiques temporelles, et plus généralement des techniques de modélisation et de vérification.

Comments