Représentation canonique pour l’analyse des Frappes de Processus 

Télécharger le fichier pdf d’un mémoire de fin d’études

Définition des réseaux discrets asynchrones

Certaines contraintes propres aux modèles de Thomas peuvent être relâchées pour per-mettre des comportements supplémentaires. Ainsi, il est courant de représenter des réseaux de régulation biologique sous la forme de réseaux discrets asynchrones. Ces réseaux sont aussi fondés sur un graphe des interactions, mais il utilisent des fonctions d’évolution (dé-finition 2.6) pour plus de permissivité, en lieu et place de paramètres discrets tels que précédemment formalisés à la définition 2.4 en page 19. Par ailleurs, l’hypothèse d’asyn-chronisme est conservée car un seul composant peut évoluer depuis chaque état, mais leur dynamique n’est pas unitaire dans le cas général car ce composant peut évoluer d’un nombre arbitraire de niveaux d’expression (définition 2.7).
Définition 2.6 (Réseau discret asynchrone (RDA)). Si G = ( ; E) est un graphe des interactions, un réseau discret asynchrone est un couple RDA = (G ; F ) avec F = (fx )x2 , tels que 8x 2 ; fx : G 1(x) ! J0 ; lx K.
Définition 2.7 (Dynamique d’un réseau discret asynchrone (!RDA)). Pour tout réseau discret asynchrone RDA = (G ; F ), La dynamique non-unitaire de RDA est donnée par la relation de transition !RDA 2 S S définie par : 8s; s0 2 S; s !RDA s0 () 9a 2 ; s[a] 6= fa(s) ^ s0[a] = fa(s) ^ 8b 2 ; b 6= a ) s[b] = s0[b]
Enfin, nous désignons par réseau booléen asynchrone tout réseau discret asynchrone dont les composants ne possèdent que deux niveaux discrets, c’est-à-dire tel que : 8x 2 ; lx = 1.

Analyses formelles du modèle de Thomas

Nous proposons dans cette section un tour d’horizon rapide des différentes méthodes d’analyse de la dynamique des modèles de Thomas. Nous nous concentrons principale-ment sur les méthodes d’analyse statique, c’est-à-dire permettant d’obtenir des résultats sur la dynamique d’un modèle sans nécessiter d’en calculer la dynamique de façon com-plète et explicite. Ces approches ont l’avantage de jouir d’une faible complexité, même si les résultats formels qu’elles fournissent sont généralement moins précis ou approximés. L’analyse du graphe des interactions seul peut ainsi permettre d’obtenir certains résultats sur sa dynamique, et la prise en compte de la paramétrisation permet d’affiner cette ap-proche. Cependant, ces résultats sont insuffisants dans beaucoup de cas, nécessitant des approches plus exhaustives. L’analyse complète de la dynamique d’un modèle de Thomas est généralement invoquée en dernier recours, car elle peut être coûteuse en temps et en espace mémoire du fait de l’explosion combinatoire inhérente au calcul de l’espace des états. Analyse du graphe des interactions
Plusieurs travaux se sont intéressés aux conclusions qui pouvaient être tirées du seul graphe des interactions. La recherche d’états stables, aussi appelés points fixes, présente un intérêt particulier dans l’étude des réseaux de régulation biologique et a été de fait très étudiée. Les conjectures de René Thomas (1981) tracent notamment un lien entre la présence de circuits dans les régulations et celle d’oscillations ou d’états stables. Elles se formulent comme suit :
– un circuit positif (c.-à-d. comportant un nombre pair de régulations négatives) est une condition nécessaire à la présence de plusieurs points fixes,
– un circuit négatif (c.-à-d. comportant un nombre impair de régulations négatives) est une condition nécessaire à la présence d’oscillations soutenues dans la dynamique, et donc à la présence d’un attracteur constitué d’au moins deux états.
Ces conjectures ont par la suite été démontrées dans le cas booléen, c’est-à-dire lorsque 8x 2 ; lx = 1 (Remy, Ruet & Thieffry, 2008; Richard, 2006) ainsi que dans le cas multivalué (Richard & Comet, 2007; Richard, 2010).
Plusieurs résultats viennent de surcroît enrichir ce résultat concernant l’existence de points fixes. Des travaux ont par exemple permis d’obtenir une valeur maximale du nombre de points fixes possibles dans un modèle de Thomas tant booléen (Aracena, 2008) que multivalué (Richard, 2009). Cette valeur dépend du nombre de composants à supprimer pour éliminer tout circuit positif dans le modèle. Paulevé & Richard (2010) ont quant à eux proposé une valeur minimale du nombre de points fixes topologiques d’un modèle booléen. Ces points fixes ont la particularité de ne pas dépendre de la paramétrisation, ce qui permet de généraliser un tel résultat à un ensemble de modèles de Thomas.
Analyse de la paramétrisation
Les conditions données précédemment sont nécessaires mais non suffisantes pour obser-ver l’apparition des comportements décrits (oscillations soutenues et multistationnarité). Plusieurs travaux permettent d’analyser la fonctionnalité des circuits, c’est-à-dire leur ca-pacité à effectivement « générer » ces comportements, et donc de rendre ces conditions susnommées nécessaires. Partant d’un modèle de Thomas donné, il est possible de re-présenter sa paramétrisation à l’aide de diagrammes de décision binaires ou multivalués (Bryant, 1986; Srinivasan, Ham, Malik & Brayton, 1990) afin d’en déduire l’ensemble des états stables mais aussi d’analyser la fonctionnalité des circuits en effectuant des produits de diagrammes de décision (Naldi, Thieffry & Chaouiya, 2007). Les différentes façons dont les oscillations soutenues et la multistationnarité sont « générées » ont aussi été étudiées, ce qui a permis de préciser ces conditions (Comet, Noual, Richard, Aracena, Calzone, Demongeot, Kaufman, Naldi, Snoussi & Thieffry, 2013).
Analyse de la dynamique
Afin d’obtenir des résultats plus précis sur le comportement d’un modèle, comme l’activa-tion d’un composant ou la présence d’oscillations sur une partie donnée du modèle, ce que les méthodes décrites précédemment ne permettent pas d’obtenir, il peut devenir néces-saire de faire appel à des techniques de model checking plus poussées (voir p. ex. Richard et al., 2006; Gallet, Manceny, Le Gall & Ballarini, 2014). Ces méthodes permettent géné-ralement une analyse exhaustive de la dynamique, tout en devant faire face à l’explosion combinatoire typique de ce type d’analyse, qui limite grandement la taille des modèles étu-diés. De telles analyses ont été théorisées par Bernot, Comet, Richard & Guespin (2004) et se basent sur l’expression de propriétés exprimées en logiques temporelles CTL (Clarke & Emerson, 1982) ou LTL (Pnueli, 1977). Elles possèdent l’avantage d’être très complètes car la dynamique est entièrement explorée et l’expressivité des logiques temporelles per-met d’exprimer beaucoup de propriétés intéressantes, mais au prix d’une complexité très importante. Afin de réduire cette complexité, Naldi, Remy, Thieffry & Chaouiya (2009) proposent d’effectuer de la réduction de modèles en éliminant certaine nœuds qui ont un rôle secondaire. Le modèle obtenu possède une taille inférieure et certaines bonnes propriétés sont conservées, comme l’ensemble des points fixes et des attracteurs, au prix d’une dynamique parfois sous-approximée par rapport au modèle d’origine.

Les Frappes de Processus standards

Cette section définit les Frappes de Processus standards telles qu’elles ont été formali-sées par Paulevé et al. (2011a). En tant que restrictions du -calcul (Brand & Zafiro-pulo, 1983; Milner, 1989), les Frappes de Processus offrent une représentation discrète, asynchrone et indéterministe avec une définition atomique des interactions entre les dif-férents composants du modèle. En cela, elles sont particulièrement adaptées aux repré-sentations des réseaux de régulation biologique bien qu’elles soient assez générales pour potentiellement permettre des applications plus larges en informatique ou dans d’autres domaines.
Nous donnerons tout d’abord à la section 2.2 une définition des Frappes de Processus standards ainsi qu’un certain nombre de définitions formelles supplémentaires nécessaires pour la suite de ce manuscrit. Nous détaillons ensuite à la section 2.2.2 le mécanisme parti-culier des sortes coopératives tel qu’il avait été formalisé dans les travaux de Loïc Paulevé, et nous montrerons qu’il permet de représenter l’action conjointe de plusieurs composants, mais avec certains inconvénients difficiles à corriger dans cette version du formalisme. En-fin, nous aborderons brièvement les travaux précédents concernant l’analyse statique qui permet d’obtenir des résultats sur l’ensemble des états stables (section 2.2.3) et sur l’at-teignabilité d’un niveau local au sein d’un modèle (section 2.2.4), et nous évoquerons les possibilités d’ajout de paramètres stochastiques (section 2.2.5) dans le but d’introduire une composante temporelle continue dans les Frappes de Processus.

Définition des Frappes de Processus standards

Les Frappes de Processus standards telles que données à la définition 2.8, aussi appelées Process Hitting, ou plus simplement Frappes de Processus dans ce chapitre, permettent une modélisation atomique et asynchrone des interactions entre composants. Un modèle de Frappes de Processus standards comporte un nombre fini de sortes généralement notées a, b, c… Celles-ci permettent de représenter les différentes entités du modèle, qu’il s’agisse de composants ayant une réalité biologique (gène, protéine…) ou d’entités nécessaires à la modélisation (comme les sortes coopératives qui seront décrites à la section 2.2.2). Chaque sorte contient plusieurs processus, qui représentent les différents niveaux d’expres-sion discrets accessibles par la sorte, et qui sont notés ai où a est le nom de la sorte et i l’indice du processus dans cette sorte. Un processus n’appartient qu’à une unique sorte. Chaque processus est dit actif (on écrira aussi : présent) s’il représente le niveau d’ex-pression dans lequel doit se trouver sa sorte à un certain moment. Un état du modèle est donc décrit par l’ensemble des processus actifs à un instant donné, avec exactement un processus actif par sorte — afin de ne pas sur-représenter ou sous-représenter le niveau d’expression courant d’une sorte.
La dynamique est introduite dans les Frappes de Processus par des actions qui per-mettent de modifier le processus actif d’une sorte, à la condition éventuelle qu’un processus donné d’une autre sorte soit présent. Une action consiste donc en un triplet de processus ai ! bj bk qui se lit : « ai frappe bj pour le faire bondir en bk », et qui signifie que si, dans un état donné, les processus ai et bj sont tous les deux actifs, alors il est possible d’activer bk (et de désactiver bj ) dans l’état suivant. Autrement dit, le processus actif de la sorte b peut bondir de bj à bk à condition que ai soit actif ; lorsque cela arrive, on dit qu’on a joué l’action ai ! bj bk . Par convention, on contraint de plus que bj 6= bk pour assurer que le jeu d’une action provoque bien le changement d’un processus actif. Il est aussi possible de définir une auto-action, où ai = bj (et nécessairement a = b), qui permet de représenter le cas particulier où le processus bj peut bondir en bk sans autre condition.
Les Frappes de Processus sont conçues comme un formalisme à temps discret asyn-chrone, ce qui signifie que l’évolution d’un tel modèle est modélisée par une succession de pas de temps discrets qui représentent la succession des états du modèle, et exactement une action est jouée entre deux états successifs. Cela implique qu’un seul processus actif à la fois peut bondir entre deux pas de temps successifs, et donc qu’une seule sorte peut évoluer entre deux états. De plus, cela rend la dynamique Frappes de Processus indéter-ministe, car à tout état du modèle peuvent correspondre plusieurs états successeurs dans le cas où plusieurs actions peuvent y être jouées. Enfin, nous notons que si aucune action n’est jouable dans un état, alors celui-ci ne possède pas de successeur et le modèle ne peut plus évoluer.

Utilisation des sortes coopératives

L’une des questions qui se posent face à un formalisme totalement asynchrone comme les Frappes de Processus standards est la représentation des coopérations entre les différents composants. En effet, le bond d’un processus dans un modèle de Frappes de Processus standards ne peut se faire que par le jeu d’une action, elle-même déclenchée par la présence d’au plus deux processus : le frappeur et la cible (c’est-à-dire le processus qui va bondir). Il n’est donc pas possible de conditionner le bond d’un processus par la présence de plusieurs processus de sortes différentes de celle de la cible. En effet, si on souhaite par exemple représenter l’activation d’un processus c1 (d’une sorte c) uniquement lorsque deux autres processus a1 et b1 (de deux autres sortes a et b) sont actifs, il n’est pas suffisant d’ajouter deux actions a1 ! c0 c1 et b1 ! c0 c1, car celles-ci permettent d’activer c1 à la condition que a1 soit actif ou que b1 soit actif : il s’agit bien de deux interactions distinctes et non d’une coopération.
Exemple. Le modèle de Frappes de Processus de la figure 2.3 représente le mécanisme de segmentation métazoaire évoqué à la page 25. Dans ce modèle, la production de pigment devrait uniquement être possible à la condition suivante : « f est actif et c n’est pas actif ».
Or dans l’état courant du modèle, la désactivation du gène f n’empêche pas la production de pigment, car depuis tout état contenant f0, il est toujours possible d’activer a à l’aide des actions f0 ! c1 c0 et c0 ! a0 a1.
Afin de représenter la coopération entre composants, et donc le raffinement de la dy-namique des modèles, Paulevé et al. (2011a) ont proposé d’ajouter des sortes particulières appelées sortes coopératives, qui servent exclusivement à la modélisation. Une sorte co-opérative permet de représenter l’état conjoint de plusieurs sortes dans le modèle. Pour cela, à chaque processus de la sorte coopérative correspond un sous-état des sortes qu’elle représente. Ainsi, il est possible de représenter les différents états combinés d’un ensemble de sortes, afin de ne jouer une action que dans une configuration particulière. Ces sortes ont l’avantage d’être des sortes standards, et donc de ne pas nécessiter d’enrichissement particulier de la sémantique. De plus, leur utilisation n’impacte pas les méthodes d’analyse de la dynamique développées : en effet, ces méthodes sont principalement impactées par le nombre de processus dans chaque sorte, et non le nombre total de sortes. Ainsi, à condi-tion de limiter le nombre de processus dans les sortes coopératives, comme expliqué à la fin de cette section, il est possible de les utiliser en maintenant de bonnes performances d’analyse.
Exemple. Les Frappes de Processus standards de la figure 2.5 reprennent les trois sortes f , c et a du modèle de la figure 2.3 et comprennent en plus une sorte coopérative f c permettant de détecter la présence simultanée de f1 et c1. Les processus de f c décrivent les combinaisons possibles des états de f et de c : f c00 correspond à f0 et c0, f c01 correspond à f0 et c1, etc. Les actions en amont de cette sorte coopérative permettent la mettre à jour, c’est-à-dire de changer son processus actif en fonction des évolutions du processus actif de f et c. Par exemple, si f1 est actif, les deux actions f1 ! f c00 f c10 et f1 ! f c01 f c11 effectuent cette mise à jour en faisant bondir le processus actif de f c depuis un processus représentant la présence de f0 (f c00 ou f c01) vers le processus correspondant représentant la présence de f1 (respectivement f c10 ou f c11). Son action en aval, f c11 ! c0 c1, joue alors le rôle d’une coopération entre f1 et c0 pour frapper a0 et le faire bondir en a1.
Exemple. Afin de pallier partiellement l’absence de coopération entre les sortes f et c dans le modèle de la figure 2.3, il est possible d’intégrer la sorte coopérative décrite à la figure 2.5. La figure 2.6 propose un modèle corrigé de cette manière, avec une sorte coopérative f c permettant de détecter la présence de f1 et c0. Les deux actions c0 ! a0 a1 et c0 ! a0 a1 sont alors remplacées par une action f c10 ! a0 a1 afin d’avoir une véritable coopération entre ces deux processus pour activer a.
Le sortes coopératives possèdent cependant un inconvénient, qui est lié au fait que les actions sont totalement indépendantes car le formalisme des Frappes de Processus standards est totalement asynchrone et indéterministe. En effet, les sortes coopératives ne sont pas nécessairement mises à jour immédiatement après un bond du processus actif d’une des sortes qu’elles représentent. Il peut ainsi exister un « décalage temporel » entre le changement de processus actif d’une sorte et la mise à jour des sortes coopératives.

Paramètres et analyse stochastiques

(Paulevé et al., 2011a) ont aussi proposé un enrichissement des Frappes de Processus standards à l’aide de paramètres stochastiques, l’objectif étant d’intégrer des données temporelles continues dans les modèles. Cet enrichissement est directement inspiré du pi-calcul stochastique (Priami, 1995). Cependant, la loi exponentielle utilisée pour la loi stochastique étant jugée trop grossière, l’approche a été raffinée par l’introduction d’un paramètre supplémentaire permettant de réduire l’intervalle de tir (Paulevé, Magnin & Roux, 2011b).
L’introduction de données dans les Frappes de Processus standards consiste à affecter un couple de paramètres stochastiques (r ; sa) 2 N R à chaque action. La probabilité de tirer une action à un instant donné (sur un axe de temps continu) suit alors une loi d’Erlang en fonction de ces deux paramètres, c’est-à-dire une somme de lois exponentielles. Le premier paramètre, appelé taux, indique le nombre de fois qu’une action peut être tirée par unité de temps. Le second paramètre est l’absorption de stochasticité, qui détermine le nombre de lois exponentielles sommées pour obtenir la distribution finale.
Tout couple de paramètres stochastiques (r ; sa) correspond à un intervalle de tir [d ; D], où d; D 2 R, pour un niveau de confiance 2 [0 ; 1] donné, et inversement, qui peut être approximé (Paulevé, 2011, p. 72). Cette conversion permet de raisonner sur des intervalles de tirs plutôt qu’en termes de loi d’Erlang, ce qui permet notamment de dé-finir des fenêtres de tir pour chaque action — une action devant être tirée dans sa fenêtre avec un niveau de confiance de . Au niveau de l’intervalle de tir, les deux paramètres stochastiques ont un rôle particulier :
– Le taux détermine la distance de l’intervalle de tir par rapport à l’origine de l’axe du temps ; autrement dit, une action avec un taux élevé sera tirée plus rapidement après sensibilisation.
– Le facteur d’absorption de stochasticité détermine la taille de l’intervalle de tir. Ainsi, augmenter ce facteur réduit la quantité D d.
Enfin, il est aussi possible d’assigner un taux infini à une action (r = 1), ce qui a pour conséquence de rendre le tir de l’action instantané : l’action doit être jouée dès sa sensibilisation. Si plusieurs actions de taux infini sont sensibilisées en même temps, le non-déterminisme est la règle et elles peuvent donc être jouées dans n’importe quel ordre. Une action de taux infini ne possède pas de facteur d’absorption de stochasticité, car ce deuxième paramètre ne changerait rien à sa condition de tir.
Exemple. Définissons les fenêtres de tir donnés à la figure 2.7, inspirées de (Paulevé et al., 2011a). Nous pouvons enrichir les Frappes de Processus standards décrites par la figure 2.6 en page 32 à l’aide de ces paramètres, de la façon donnée à la figure 2.8. Cette affectation nous permet notamment d’obtenir un comportement oscillant pour les sortes a et c, et une auto-désactivation de f après plusieurs oscillations. Les paramètres du couple c ont en effet été conçus de façon à ce que l’arrêt de l’horloge, provoqué par la désactivation de f , survienne après la formation de 7 rayures.
Les modèles de Frappes de Processus standards comportant des paramètres stochas-tiques peuvent être simulés afin d’observer un exemple d’exécution du modèle étudié. Du fait de la nature indéterministe et probabiliste du modèle, plusieurs dynamiques sont pos-sibles, et chaque simulation donne des résultats différents en termes de chemin d’exécution
— ou, pour un même chemin d’exécution, en termes de temps de tir des actions. Il est donc possible d’effectuer un grand nombre de simulations pour obtenir des statistiques sur le comportement d’un modèle. Il est aussi possible de recourir à un model checker pro-babiliste comme PRISM, qui fournit des résultats formels sur la dynamique d’un modèle, et des probabilités d’atteignabilité. Cependant, une telle approche est très coûteuse en termes de temps de calcul et d’espace mémoire, ce qui empêche l’analyse de réseaux de grande taille.

Table des matières

1 Introduction 
1.1 Contexte & Motivations
1.2 Les réseaux de régulation biologique
1.3 Contributions
1.4 Collaborations
1.5 Organisation du manuscrit
1.6 Notations
2 État de l’art de la modélisation 
2.1 Le Modèle de Thomas
2.1.1 Définition du modèle de Thomas
2.1.2 Définition des réseaux discrets asynchrones
2.1.3 Analyses formelles du modèle de Thomas
2.2 Les Frappes de Processus standards
2.2.1 Définition des Frappes de Processus standards
2.2.2 Utilisation des sortes coopératives
2.2.3 Recherche de points fixes
2.2.4 Analyse statique pour le calcul d’atteignabilité
2.2.5 Paramètres et analyse stochastiques
3 Enrichissement des Frappes de Processus pour l’aide à la modélisation 
3.1 Frappes de Processus avec classes de priorités
3.1.1 Définition
3.1.2 Équivalences entre Frappes de Processus avec k classes de priorités
3.1.3 Réutilisation des résultats existants
3.2 Frappes de Processus avec arcs neutralisants
3.2.1 Définition
3.2.2 Équivalence avec les Frappes de Processus avec k classes de priorités
3.2.3 Réutilisation des résultats existants
3.3 Frappes de Processus avec actions plurielles
3.3.1 Définition
3.3.2 Traduction vers les Frappes de Processus avec 4 classes de priorités
3.3.3 Équivalence avec les Frappes de Processus avec k classes de priorités
3.3.4 Réutilisation des résultats existants
3.4 Bilan .
4 Représentation canonique pour l’analyse des Frappes de Processus 
4.1 Les Frappes de Processus canoniques
4.1.1 Critères et définitions
4.1.2 Résultats préliminaires sur les Frappes de Processus canoniques
4.2 Équivalence avec les autres formalismes de Frappes de Processus
4.2.1 Aplatissement des Frappes de Processus avec k classes de priorités
4.2.2 Aplatissement des Frappes de Processus avec arcs neutralisants
4.2.3 Aplatissement des Frappes de Processus avec actions plurielles
4.2.4 Représentation en Frappes de Processus avec actions plurielles
4.3 Analyse statique
4.3.1 Définitions préliminaires
4.3.2 Sous-approximation
4.3.3 Atteignabilité d’un sous-état
4.3.4 Raffinement de la sous-approximation séquentielle
5 Expressivité des Frappes de Processus et positionnement par rapport à d’autres formalismes 
5.1 Traduction depuis les réseaux discrets asynchrones
5.2 Inférence du modèle de Thomas
5.2.1 Inférence du graphe des interactions
5.2.2 Inférence des interactions
5.2.3 Inférence des paramètres
5.2.4 Énumération des paramétrisations admissibles
5.2.5 Pistes d’implémentation
5.3 Équivalence avec les réseaux d’automates synchronisés
5.4 Traduction en réseaux de Petri
5.5 Traduction depuis la sémantique booléenne Biocham
5.6 Bilan .
6 Applications sur des exemples de grande taille 
6.1 Traductions vers le modèle de Thomas
6.1.1 Application au récepteur de facteur de croissance épidermique
6.1.2 Temps d’exécution sur quelques modèles de grande taille
6.2 Analyse statique du récepteur de lymphocyte T
6.3 Bilan .
7 Conclusion et perspectives 
7.1 Retour sur les résultats de cette thèse
7.2 Perspectives de travail
Bibliographie 

Télécharger le rapport complet