Sémantique de la dynamique des réseaux d’automates

Introduction

Les premiers formalismes de modélisation utilisés pour étudier les RRB ont été basés sur les systèmes d’équations différentielles ordinaires (EDO) qui ont été proposées pour capturer le comportement du système étudié, par exemple dans (Mesarović, 1968). Dans les EDO, la modélisation est quantitative ; chaque variable du modèle mathématique abstrait la concentration du produit d’un composant biologique particulier (e.g., un gène), et les changements de concentration s’expliquent par la différence entre le taux de synthèse et le taux de dégradation. Toutefois, biologiquement, il est possible de considérer que les régulations de gènes sont qualitatives (chaque régulation est alors distinguée par son activité ou inactivité). Ce besoin de simplification est justifié par le fait que la valeur d’un grand nombre de paramètres reste inconnue. Dans un certain cas, la modélisation peut être sem-qualitative et le modèle mathématique peut devenir un système d’équations différentielles linéaires par morceaux : tant que les régulations ciblant un gène ne changent pas d’état (actif ou inactif), le taux de synthèse de ce gène est considéré constant. Plusieurs travaux sont basés sur des équations différentielles linéaires par morceaux, comme dans (De Jong, Gouzé, Hernandez, Page, Sari & Geiselmann, 2004). Si les paramètres cinétiques sont correctement déterminés, ces modèles produisent des dynamiques cohérentes avec des observations expérimentales.
L’inconvénient d’un formalisme si expressif est sa sensibilité aux paramètres cinétiques.
De plus, le manque de connaissances quantitatives sur ces paramètres, la difficulté de les mesurer dans le système réel aussi bien que la fiabilité des valeurs obtenues, obligent souvent à utiliser pour les simulations des valeurs approximatives si ce n’est plus ou moins arbitraires.
En outre, ces simulations produisent les trajectoires de la dynamique du système, mais ne permettent pas souvent de conclure sur l’effet d’une action particulière sur le système. Plus précisément, les simulations faites avec des valeurs approximatives de paramètres cinétiques ne permettent pas réellement de déduire toutes les conséquences d’une infime modification du système.
Pour faire face à ces limitations, certains chercheurs préfèrent travailler avec des modèles qualitatifs en considérant des domaines où les variables ont des taux de synthèses quasi constants afin de faire du model-checking sur les systèmes modélisés par équations différentielles par morceaux.
Nous ne détaillons pas dans ce chapitre un état de l’art sur les modélisations continues (en l’occurrence sur les ODE), car nos travaux sont plutôt basés sur la modélisation discrète qualitative. Une étude a été faite dans (De Jong, 2002) pour montrer le lien entre ces deux approches de modélisation.
La section 2.2 présente trois niveaux de spécification des RRB couramment utilisés, correspondant à différents degrés d’abstraction du système étudié :
– Le graphe des interactions peut être considéré comme la spécification la plus abstraite d’un RRB : seules les informations qualitatives de régulation entre les composants sont référencées (a est un activateur de b, par exemple).
– Les modélisations discrètes associent à chaque composant un ensemble fini discret de niveaux qualitatifs ({0, 1, 2}, par exemple), reflétant une quantification de sa concentration réelle, et caractérisent l’évolution des composants en fonction de leurs régulateurs. Cette dernière peut par exemple être définie par les paramètres discrets de René Thomas (Thomas, 1991).
– Enfin, les modélisations hybrides ajoutent une dimension continue gouvernant les transitions discrètes du système, généralement par l’attribution de délais (aléatoires ou par intervalle de temps) à l’application des régulations.
Ensuite, la section 2.3 dresse un état de l’art des analyses statiques et dynamiques opérant sur les RRB. Deux propriétés dynamiques sur lesquelles nous nous concentrons :
– la vérification de l’atteignabilité, et
– l’identification des points fixes et des attracteurs cycliques.
Puis, la section 2.4 introduit quelques méthodes de la littérature dont le but est d’apprendre des RRB à partir de leurs dynamiques observées lors des expérimentations.
Nous détaillons ainsi dans cette section quelques avantages et quelques inconvénients de ces méthodes.
Finalement, après un préambule sur les méthodes de modélisation et d’analyse des RRB, la section 2.5 donne la représentation des RRB avec les frappes de processus (ProcessHitting, PH), est un formalisme introduit dans la thèse de Loïc Paulevé (Paulevé, 2011).
Ensuite, ce formalisme a subi plusieurs enrichissements au cours des dernières années et c’est ce qui nous ramène, dans cette thèse, à travailler avec les réseaux d’automates (Automata Networks, AN). En effet, les PH forment une sous classe des AN. Nous défendons ainsi, à la fin de cette section 2.5 le choix de ce formalise.

Modélisation des RRB

Cette section détaille les principales méthodes de modélisation des RRB. Ces méthodes englobent des modélisations discrètes et des modélisations hybrides. Nous commençons par présenter le graphe des interactions, qui permet d’introduire, par la suite, les modèles discrets (comme les modèles de Kaufmann et de Thomas). Puis nous introduisons d’autres modélisations hybrides utilisées pour la modélisation des RRB.

Graphes des interactions

Le graphe des interactions d’un RRB présente les régulations entre les composants avec des réseaux simples. En effet, les composants biologiques sont représentés par des nœuds étiquetés par un nom (celui du composant : a, b, c , etc.) et les interactions par des arcs orientés signés (positifs ou négatifs). Un arc signé positif (resp. négatif) de a vers b dénote que a est un activateur (resp. inhibiteur) de b.
La figure 2.1 (gauche) ci-dessous présente un graphe des interactions simple tel qu’un arc positif (resp. négatif) est étiqueté par le signe + (resp. −).
Afin de mieux identifier le rôle des régulations impliquées, le graphe des interactions peut être agrémenté d’informations supplémentaires en se basant sur le niveau de connaissance du système et les questions posées. Nous illustrons dans la figure 2.1, ces différents niveaux de spécification d’un RRB et nous les expliquons dans la suite.

Modèles stochastiques

Les modèles stochastiques associent une composante temporelle aléatoire aux transitions qui en général, suit une distribution exponentielle, permettant d’avoir un système markovien. Par conséquent, plusieurs travaux ont été initiés dans le cadre des modélisations markoviennes afin de modéliser et d’analyser des systèmes biologiques. Nous pouvons citer l’utilisation de Réseaux de Petri stochastiques (Heiner, Gilbert & Donaldson, 2008), du π-calcul stochastique (Priami, 1995; Maurin, Magnin & Roux, 2009), de κ (Danos, Feret, Fontana & Krivine, 2007) ou encore de Biocham (Rizk, Batt, Fages & Soliman, 2008).
Le but principal des modélisations stochastiques est de permettre le calcul des probabilités d’observation de certains comportements comme dans (Baier, Bertrand, Bouyer, Brihaye & Größer, 2007). Ainsi, il est possible de prédire les évolutions dynamiques les plus probables par rapport à d’autres. Par ailleurs, dans le cas de la vérification de l’atteignabilité, il serait possible d’avoir une idée sur la probabilité d’atteindre un certain objectif fixé.

Modèles temporels

Le but des modélisations temporelles est d’offrir un raffinement sur les dynamiques discrètes initiales. En effet, plusieurs possibilités émergent du fait de la modélisation temporelle : (1) du fait de la contrainte temporelle, il peut être désormais possible d’observer des comportements initialement interdits dans la dynamique discrète et de même, la contrainte temporelle peut aussi interdire certaines transitions ; (2) la composante temporelle permet d’avoir des comportements plus précis sur la dynamique.
Au cours de la dernière décennie, la modélisation hybride des RRB a suscité un intérêt croissant pour les délais entre les états du réseau. Ces approches hybrides considèrent différents cadres de modélisation. En général, la composante temporelle dans les modèles temporels représente le délai d’une transition pris dans un intervalle de temps fixé ou bien sa valeur suit une certaine équation différentielle.
Les mérites des formalismes hybrides dans la biologie ont été étudiés, par exemple dans ; les Réseaux de Petri temporisés (Popova-Zeugmann, Heiner & Koch, 2005), les automates temporisés (Siebert & Bockmayr, 2006; Batt, Salah & Maler, 2007), les automates hybrides linéaires (Ahmad, Roux, Bernot, Comet & Richard, 2008; Behaegel, Comet, Bernot, Cornillon & Delaunay, 2016), les automates hybrides non linéaires (Alur, Belta, Kumar, Mintz, Pappas, Rubin & Schug, 2002), le modèle hybride d’un oscillateur neuronal (Mandon, Haar & Paulevé, 2012), et la représentation booléenne (Paoletti, Yordanov,Hamadi, Wintersteiger & Kugler, 2014; Li, Yang & Chu, 2012).
Dans (Matsuno, Doi, Nagasaki & Miyano, 2000), les auteurs passent des réseaux de Petri aux réseaux de Petri hybrides : l’avantage de l’approche hybride en ce qui concerne la modélisation discrète réside dans la possibilité de capturer des facteurs biologiques, parexemple le délai mis pour la transcription de l’ARN polymérase.
D’autres travaux d’étude de RRB ont aussi été basés sur les équations différentielles avec délais comme dans (Hale & Lunel, 2013). Ces modèles permettent de ne pas spécifier tous les processus explicitement et leurs effets sur la dynamique du système peuvent être regroupés et définis sous la forme de délais. Cette caractéristique est intéressante car des données expérimentales pour le système d’intérêt sont souvent manquantes, et certains des processus qui ne sont pas bien connus ou compris peuvent être regroupés sous forme de délais pour réduire ainsi le nombre de variables et de paramètres du modèle. En revanche, ces équations différentielles avec délais sont difficiles à résoudre et les méthodes géométriques et de plan de phase usuelles ne peuvent pas être utilisées simplement.
Dans (Batt et al., 2007), les auteurs utilisent le formalisme de (Maler & Pnueli, 1995) pour modéliser un RRB. Dans ce formalisme, une distinction est possible entre les gènes et leurs produits. Les gènes sont représentés comme des fonctions booléennes de produits de gènes. Les produits de gène sont représentés par leurs niveaux de concentration et leur évolution (positive ou négative) est en fonction de leur gène (actif ou non). En plus l’action du gène sur le niveau de concentration de son produit est temporisée sur un intervalle de délais. Tout comme dans les travaux de (Siebert & Bockmayr, 2006), ils considèrent l’intervalle de délais pour passer d’un niveau n à un niveau n ± 1 pour une variable donnée.
En fait, ces deux approches de modélisation sont très proches bien que le formalisme pour la description du réseau de régulation génétique pour les modéliser soit différent et que Batt et al. (2007) considèrent que les produits de gène évoluent continuellement (leur vitesse d’évolution n’est donc jamais nulle).
Enfin, dans (Comet, Fromentin, Bernot & Roux, 2010), les auteurs étudient une extension directe de l’approche de modélisation discrète de René Thomas en introduisant des délais quantitatifs. Ces délais représentent le temps obligatoire pour qu’un gène passe d’un niveau qualitatif discret au suivant (ou précédent). Ils présentent l’avantage d’un tel cadre pour l’analyse de la production de mucus dans la bactérie Pseudomonas aeruginosa.
L’approche que nous proposons dans cette thèse dans le chapitre 3 hérite de cette idée que certains modèles doivent saisir ces caractéristiques de synchronisation.
La section 2.5 en page 42 présente le formalisme des Frappes de Processus qui est un modèle discret et une restriction du formalisme des réseaux d’automates. En effet, dans cette thèse, nous utilisons ce dernier pour la modélisation des RRB. Il présente l’avantage de permettre une modélisation hybride des systèmes. Ceci par une modélisation des composants comme des composants à états discrets (Paulevé, 2011; Folschette, 2014) et une dynamique continue qui permet à la fois la prise en compte du temps sous forme continue avec un comportement aléatoire (Fippo-Fitime, 2016).

Analyse formelle des propriétés dynamiques des RRB

La majorité des systèmes biologiques ont une caractéristique qui les différencie des autres champs d’application de l’informatique. Cette caractéristique consiste au regroupement des entités, ayant un comportement simple, et la production d’un comportement complexe de par leurs interactions. Ceci est alors à l’origine de l’explosion combinatoire des comportements à analyser par les méthodes « classiques ». Afin de contourner cette explosion combinatoire, plusieurs recherches ont été menées durant la dernière décennie. Par exemple, l’analyse dite statique qui réussit à conclure sur des propriétés de la dynamique du modèle étudié sans avoir besoin de l’analyser de façon exhaustive. En effet, les approches d’analyses statiques reposent plutôt sur une analyse des structures du modèle tout en ayant parfois un recours à des méthodes d’abstraction afin d’en simplifier le comportement, comme dans (Feret, Henzinger, Koeppl & Petrov, 2012; Paulevé, Chancellor, Folschette, Magnin & Roux, 2014; Folschette et al., 2015).
Dans cette thèse, les propriétés dynamiques étudiées sont : la vérification de l’atteignabilité et l’identification des attracteurs. Ainsi, nous présentons dans cette section un état de l’art sur quelques travaux développés pour l’analyse et la vérification de ces deux propriétés.

Atteignabilité

Quand nous vérifions la propriété de l’atteignabilité dans un RRB, c’est-à-dire que nous vérifions l’existence d’un chemin qui permet d’atteindre l’objectif fixé à partir d’un état initial du réseau. Nous présentons dans la suite quelques méthodes existantes pour l’analyse formelle de cette propriété.

Analyse avec abstraction du modèle

Le but principal de la vérification des modèles par abstraction est de produire des analyses efficaces du système sans l’exécuter (Cousot & Cousot, 1977). Plusieurs travaux sont faits en se basant sur une telle approche, dans le domaine de la biologie des systèmes ou autres.
Par exemple, dans (Klaudel, Koutny, Pelz & Pommereau, 2010), les auteurs proposent une technique d’abstraction pour générer des représentations d’espaces d’états réduites pour les systèmes multi-thread. Dans le domaine de la biologie, on trouve le modèle kappa (Danos, Feret, Fontana & Krivine, 2008) ainsi que les travaux de thèse de Loïc Paulevé (2011).
Les travaux de Loïc Paulevé (Paulevé, 2011) qui ont été par la suite enrichis par Maxime Folschette (Folschette, 2014), fournissent une approche très spécifique qui repose sur une interprétation abstraite des comportements concurrents des réseaux d’automates (Folschette, Paulevé, Magnin & Roux, 2013). Ils déterminent des représentations abstraites, appelées Graphes de Causalité Locale (GCL), de l’ensemble des comportements nécessaires pour la propriété d’atteignabilité recherchée. Les abstractions calculées ne prennent pasen compte une partie de l’information sur l’ordre ou l’arité des transitions locales. Il en résulte ainsi des approximations supérieures et inférieures des comportements du modèleconcret. Une analyse du GCL permet d’identifier les propriétés qui sont soit nécessaires, soit suffisantes à l’atteignalibilité étudiée.
Cette méthode a l’avantage d’avoir une complexité bien inférieure aux méthodes de vérification formelle exacte. En effet, les approches exactes sont de complexité exponentielle selon le nombre d’états dans un seul automate et polynomiale selon le nombre d’automates dans le réseau d’automates asynchrones. Cependant, il existe un risque d’obtenir une réponse non concluante pour le modèle concret, nécessitant alors un raffinement de l’analyse de la dynamique. Une partie de cette analyse statique a par la suite été utilisée dans le but d’approximer efficacement des ensembles de coupes (cut-sets ), c’est-à-dire des ensembles d’états locaux nécessaires à une certaine accessibilité (Paulevé, Andrieux & Koeppl, 2013).
Son utilisation dans ce cadre s’est avérée efficace sur des modèles de plusieurs milliers de composants.

Dynamique des frappes de processus

Nous présentons dans la suite les éléments nécessaires pour la dynamique en complément des actions dans les frappes de processus. Le premier élément va être la propriété de jouabilité introduit à la définition 2.12. Cette propriété permet de décrire la présence d’une configuration de processus actifs dans un état donné, ce qui permet de décrire la « jouabilité » d’une action. Aussi la définition 2.13 permet de définir l’opérateur de jouabilité des frappes de processus standard. Enfin la dynamique proprement dite est donnée à la définition 2.14. Elle est construite à partir de l’opérateur de jouabilité.

Les enrichissements des Frappes de Processus

Le formalisme des frappes de processus a subi plusieurs enrichissements au cours des dernières années par (Folschette, 2014) et (Fippo-Fitime, 2016). Ainsi, c’est ce qui nous amène, dans cette thèse, à travailler avec les réseaux d’automates qui est une extension des frappes de processus. Nous montrons ainsi dans la suite ces différents enrichissements.

Utilisation des sortes coopératives 

L’une des questions qui se posent en présence d’un formalisme totalement asynchrone comme les frappes de processus standard 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 standard 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 vers un autre processus). 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.

Les Réseaux d’automates

Nous définissons dans cette section les AN, un formalisme plus enrichi que les Frappes de Processus (présentées dans la section 2.5 en page 42 du chapitre 2). Nous pouvons assimiler les AN à des Frappes de Processus avec des actions plurielles (introduites dans la sous-section 2.5.3 en page 46) et qui ont été introduites dans la thèse de Maxime Folschette en 2014 (Folschette, 2014).
Un AN est considéré simple grâce à sa définition atomique des interactions entre les composants du système qu’il modélise, ainsi que sa représentation discrète. AN est donc considéré comme particulièrement adapté pour la représentation d’un Réseau de Régulation Biologique (RRB).
Différentes sémantiques de la dynamique peuvent être utilisées avec les formalismes des modèles discrets de type AN. Nous introduisons dans cette section les deux sémantiques les plus répandues dans la littérature : l’asynchrone et le synchrone.

Table des matières
1 Introduction 
1.1 Contexte et motivations
1.2 Réseaux de régulation biologique (RRB)
1.3 Contributions
1.4 Organisation du manuscrit
1.5 Collaborations
1.6 Notations
2 Préliminaires 
2.1 Introduction
2.2 Modélisation des RRB
2.2.1 Graphes des interactions
2.2.2 Les modèles discrets
2.2.3 Modèles hybrides
2.3 Analyse formelle des propriétés dynamiques des RRB
2.3.1 Atteignabilité
2.3.2 Les attracteurs
2.4 L’apprentissage des RRB à partir des données expérimentales
2.4.1 L’inférence des RRB
2.4.2 Validation des RRB appris
2.5 RRB via les frappes de processus
2.5.1 Frappes de processus standards
2.5.2 Dynamique des frappes de processus
2.5.3 Les enrichissements des Frappes de Processus
2.5.4 Discussion
3 Les Réseaux d’automates avec le temps 
3.1 Introduction
3.2 Les Réseaux d’automates
3.2.1 Définitions des réseaux d’automates
3.2.2 Sémantique de la dynamique des réseaux d’automates
3.3 Intégration du temps dans les réseaux d’automates
3.3.1 Définitions des réseaux d’automates avec le temps (T-AN)
3.3.2 Fonctionnement des transitions locales temporisées
3.4 Les réseaux d’automates avec le temps par rapport à d’autres modèles temporels existants
3.4.1 Frappes de processus
3.4.2 Le paradigme S[B]
3.4.3 Les réseaux de Petri temporels et temporisés
3.4.4 Chaîne de Markov(k)
3.5 Discussion
4 L’inférence des réseaux d’automates avec le temps 
4.1 Introduction
4.2 La méthode d’inférence brute
4.2.1 Pré-traitement des données de séries temporelles
4.2.2 Algorithme de la méthode d’apprentissage des modèles : MoT-AN
4.3 Validation du résultat de MoT-AN
4.3.1 Démarche de validation pratique du résultat de MoT-AN
4.3.2 Exemple d’application de la démarche de validation pratique du résultat de MoT-AN
4.3.3 Génération des modèles T-AN appris
4.3.4 Comparaison entre les T-AN appris et le T-AN initial
4.3.5 Étude théorique de MoT-AN
4.3.6 Validation pratique du résultat de MoT-AN sur d’autres exemples
4.4 Raffinement du résultat de MoT-AN par des filtres
4.4.1 Filtre de cohérence entre la dynamique du modèle et la dynamique des T-AN
4.4.2 Filtre basé sur la fréquence d’apparition des transitions locales temporisées dans les modèles appris
4.4.3 Filtre associé au déterminisme des régulateurs entre les composants
4.4.4 Filtre associé à un délai moyen d’une transition locale temporisée
4.5 Révision des modèles
4.6 Application : système de l’horloge circadienne
4.6.1 Description et traitement des données de séries temporelles
4.6.2 T-AN appris par MoT-AN modélisant le système de l’horloge circadienne du foie
4.7 Discussion
5 Analyse de la dynamique des RRB 
5.1 Introduction
5.2 Dynamique généralisée des réseaux d’automates
5.2.1 Définition des réseaux d’automates
5.2.2 La dynamique des réseaux d’automates
5.2.3 Déterminisme et non-déterminisme
5.3 Vérification de l’atteignabilité
5.3.1 Définition de la problématique de l’atteignabilité
5.3.2 Idée intuitive pour la résolution de la problématique de l’atteignabilité
5.4 Identification des attracteurs
5.4.1 Les attracteurs cycliques
5.4.2 Étude des caractéristiques dynamiques des attracteurs cycliques
5.4.3 Les attracteurs singletons (i.e., les points fixes)
5.4.4 Idée intuitive des méthodes pour l’identification des attracteurs
5.5 Discussion
6 Mise en œuvre et résultats 
6.1 Introduction
6.2 Programmation logique en Answer Set Programming
6.2.1 Syntaxe et la sémantique d’ASP
6.2.2 Modélisation d’un programme ASP
6.3 L’inférence des T-AN
6.3.1 La méthode de modélisation des T-AN, MoT-AN, en ASP
6.3.2 Les filtres du raffinement du résultat de MoT-AN en ASP
6.3.3 Application
6.4 La vérification de l’atteignabilité
6.4.1 La dynamique des AN et des T-AN en ASP
6.4.2 L’atteignabilité en ASP
6.4.3 Applications
6.4.4 Discussion
6.5 La recherche des attracteurs
6.5.1 Les attracteurs cycliques en ASP
6.5.2 Les points fixes en ASP
6.5.3 Applications
6.5.4 Discussion
6.6 Conclusion
7 Conclusion et perspectives 
7.1 Introduction
7.2 Récapitulatif
7.3 Perspectives de travail
7.3.1 Extensions de l’analyse dynamique
7.3.2 Raffinement de l’apprentissage et de la révision des RRB
7.3.3 La résilience du modèle de RRB
7.3.4 Enrichissement de la modélisation des RRB
Bibliographie

Lire le rapport complet