L'invariance de ces rapports de proportionnalité, pour certains jeux de paramètres est révélateur de la présence d'une relation de groupage faible. Celle-ci permet de quotienter l'exécution d'une chaîne de Markov pour certaines distributions d'états initiales tout en restant Markovien [21]. De même, cela permet de réduire le système différentiel sous-jacent pour certains états initiaux.

Dans le cas du premier jeu de paramètres, le quotient opère même à plus bas-niveau, puisqu'il s'exprime au niveau réactionnel: à chaque réaction peut être associée une réaction symétrique obtenue en échangeant les occurrences des sites x et y dans certaines occurrences de la protéine A, ce qui permet de montrer l'existence d'une bisimulation arrière [22] sur système de transition stochastique sous-jacent ou de réduire le système différentiel sous-jacent.

### 6.1.4 Conclusion sur le cas d'étude

Pour conclure avec cet exemple jouet, nous avons vu que des symétries pouvaient apparaître dans les configurations d'espèces biochimiques, dans les états du système, dans les distributions d'états ou même dans l'effet des règles. Ces symétries ont un impact sur notre capacité à réduire la dynamique du système. En effet, lorsque l'action des règles est symétrique, il est possible d'induire une relation d'équivalence pour quotienter l'ensemble des états, ce qui suggère l'existence d'une bisimulation avant. De plus, lorsque la distribution initiale des états est également symétrique, alors le système non simplifié comporte des invariants statistiques, ce qui suggère l'existence d'une bisimulation arrière. Contrairement aux raisonnements sur les rapport entre constantes de liaison et de dissociation, c'est un raisonnement compositionnel qui considère les réactions, classe de symétries par classe de symétries. C'est pourquoi ce type de raisonnement sera privilégié dans la suite de ce chapitre.

## 6.2 Échanges de sites dans des graphes à sites

Pour rester simple, le cadre général des groupes de symétries sur les graphes à sites ne sera pas décrit. Au lieu de cela, la présentation se concentre sur le cas particulier où les symétries prennent la forme d'échanges de sites. Le but de cette section est de définir l'effet de la permutation de sites dans les différents éléments du langage Kappa, c'est à dire les motifs, les plongements, les règles et l'application des règles.

Les échanges de sites forment un groupe. Ainsi il est possible de les composer et chaque échange de sites admet un échange inverse. De plus, ce groupe est engendré par les échanges entre deux sites (qui consistent à permuter l'état de deux sites dans l'occurrence d'une protéine). Aussi, seul l'effet des échanges entre deux sites sera décrit, l'effet des autres transformations pouvant être déduit en décomposant ces échanges en séquences d'échanges élémentaires de sites.

### 6.2.1 Échanges d'une paire de sites dans la configuration d'une espèce biochimique

Il est possible d'échanger l'état d'une paire de sites de la même occurrence d'un agent dans la configuration d'une espèce biochimique. Plutôt que d'échanger leurs états, il est possible de représenter de manière duale cette transformation en échangeant le nom des sites correspondants. Dans la représentation graphique, le site initial et le site avec lequel il est échangé gardent les mêmes positions pour représenter explicitement l'origine des sites transformés avant cet échange.

Des exemples sont donnés en figure 6.16. Deux configurations d'espèces biochimiques qui peuvent être obtenues l'une à partir de l'autre en permutant éventuellement une paire de sites dans une ou plusieurs occurrences d'une même protéine, seront appelées *symétriques*, en précisant éventuellement par quel type d'échanges de sites.

**Exemple 6.2.1** *En figure 6.16, les échanges de sites sont appliqués aux configurations des espèces biochimiques de l'exemple étudiés dans ce chapitre (voir en figure 6.1).* En figure 6.16(a), est montré l'effet des échanges de sites sur les occurrences du monomère de la protéine A. Il n'y a donc qu'un échange possible, puisqu'il n'y a qu'une occurrence de la protéine A. Cet échange est dessiné en orange. Les deux sites de l'occurrence de la protéine A sont nécessairement libres, sinon ce ne serait pas un monomère. Du coup, l'échange des deux sites laisse la configuration de cette espèce biochimique inchangée (puisqu'en effet la position des sites dans une occurrence de protéine n'a pas de signification particulière en Kappa).*

Pour les occurrences de dimères de la protéine A, il est possible d'échanger les sites de l'occurrence de gauche de la protéine A, les sites de l'occurrence de droite A, ou les deux. En figure 6.16(b), est montré, en vert, l'effet de l'échange des sites de l'occurrence gauche de la protéine A. En figure 6.16(c), est montré, en rouge, l'effet de
<figure><img src="image_104.png" /><figcaption>Figure 6.16: Effet des échanges de sites sur les différentes configurations d'espèces biochimiques dans le modèle jouet.</figcaption></figure>

l'échange des sites de l'occurrence droite de la protéine A. Enfin en figure 6.16(d), est montré, en marron, l'effet de la combinaison des deux échanges de sites. L'ordre n'a pas d'influence sur le résultat. L'échange des sites de deux occurrences de la protéine A dans une occurrence du dimère asymétrique donne également une occurrence de dimère asymétrique, comme le montre la partie droite de la figure 6.16(d). Hormis ce cas particulier, l'application des échanges de sites aux autres configurations de dimères les transforme. Essentiellement, les liaisons entre deux sites identiques deviennent des liaisons entre deux sites différents lorsque les sites sont échangés dans une seule occurrence de la protéine A (voir en figure 6.16(b) et en figure 6.16(c)), alors que réciproquement, les liaisons entre deux sites différents deviennent des liaisons entre deux sites identiques (le site en question dépend de quel côté l'échange est appliqué). Lorsque les échanges de sites sont appliqués simultanément aux deux occurrences de la protéine A (voir en figure 6.16(d)), l'effet est de transformer un dimère formé par une liaison entre les deux sites x des occurrences de la protéine A en un dimère formé par une liaison entre les deux sites y des occurrences de la protéine A, et réciproquement.

## 6.2.2 Échanges d'une paire de sites dans les occurrences d'une protéine d'un motif

Il est possible d'échanger une paire de sites dans une occurrence de protéine dans un motif. Pour cela il suffit de choisir une occurrence de protéine dans un motif, et deux sites dans l'interface de la sorte de la protéine correspondante. Si l'occurrence de protéine ne contient aucun de ces deux sites, alors le motif reste tel qu'il est. Si l'occurrence de protéine contient exactement un des deux sites, alors celui-ci est remplacé par l'autre site en gardant ses éventuels états d'activation et de liaison. Enfin, si l'occurrence de protéine contient les deux sites, alors l'un est remplacé par l'autre, et réciproquement. De ce fait, les deux sites échangent leurs éventuels états d'activation et de liaison. Le motif reste inchangé si les deux sites avaient les mêmes états. Deux motifs qui peuvent être obtenus l'un à partir de l'autre en échangeant éventuellement des paires de sites dans une ou plusieurs occurrences d'une même protéine sont appelés motifs symétriques. On dit également que l'un est le symétrique de l'autre, en précisant éventuellement par quel type d'échanges de sites.

**Exemple 6.2.2** L'effet des échanges de sites dans les occurrences des protéines des motifs connexes qui ne forment pas des configurations d'espèces biochimiques (parce l'une de leur occurrence de la protéine A y est partiellement définie) est décrit en figure 6.17.

L'effet des échanges de sites dans les motifs formés d'une seule occurrence de la protéine A est décrit en figure 6.17(a). Les transformations correspondantes sont représentées par des doubles flèches ondulées oranges. Permuter les sites x et y dans l'occurrence de la protéine A dans un motif qui ne contient aucun site, laisse cette occurrence inchangée. Lorsqu'une occurrence de la protéine A ne contient que le site x, son symétrique ne contient que le site y en préservant son état de liaison (qui peut être libre ou lié sans préciser à quel site)
<figure><img src="image_105.png" /><figcaption>(a) Échange des sites sur les autres motifs avec une seule occurrence de la protéine A partiellement définie.</figcaption></figure>

<figure><img src="image_106.png" /><figcaption>(b) Échange des sites de l'occurrence gauche de la protéine A dans les autres motifs formés de deux occurrences de la protéine A partiellement définies.</figcaption></figure>

<figure><img src="image_107.png" /><figcaption>(c) Échange des sites de l'occurrence droite de la protéine A dans les autres motifs formés de deux occurrences de la protéine A partiellement définies.</figcaption></figure>

<figure><img src="image_108.png" /><figcaption>(d) Échanges des sites des deux occurrences de la protéine A dans les autres motifs formés de deux occurrences de la protéine A partiellement définies.</figcaption></figure>

Figure 6.17: Effet des échanges de sites dans les motifs connexes qui ne sont pas des configurations d'espèces biochimiques.
et réciproquement. Le cas d'une instance du monomère de la protéine A dont les deux sites sont libres, a déjà été vu. En effet, c'est la configuration d'une espèce biochimique (voir en figure 6.16(a)). Par ailleurs, il est impossible dans ce modèle de trouver une instance de la protéine A avec ses deux sites liés, il reste donc uniquement le cas d'une instance de protéine avec deux sites, l'un libre, et l'autre lié à un site inconnu. Dans ce cas, échanger les sites revient à rendre libre le site qui était lié et lié celui qui était libre.

En figure 6.17(b), sont représentés par des doubles flèches ondulées vertes, l'échange des sites x et y dans l'occurrence de gauche de la protéine A dans des motifs formés de deux occurrences de la protéine A connectées entre elles. Les liens symétriques sont transformés en des liens asymétriques, et réciproquement (le type de lien étant défini par la site qui était lié dans l'occurrence de droite de la protéine A). De plus, si le motif contenait un site libre, celui-ci est conservé mais change de nom s'il était situé dans l'occurrence de gauche de la protéine.

En figure 6.17(c), sont représentés par des doubles flèches ondulées rouges, l'échange des sites x et y dans l'occurrence de droite de la protéine A dans des motifs formés de deux occurrences de la protéine A connectées entre elles. Les liens symétriques sont transformés en des liens asymétriques, et réciproquement (le type de lien étant défini par la site qui était lié dans l'occurrence de droite de la protéine A). De plus, si le motif contenait un site libre, celui-ci est conservé mais change de nom s'il était situé dans l'occurrence de gauche de la protéine.

En figure 6.17(d), sont représentés par des doubles flèches marrons, les échanges des sites x et y dans les deux occurrences de la protéine A dans les motifs formés de deux occurrences de la protéine A connectées entre elles. Les liens symétriques restent symétriques mais sont portés par l'autre site. Les liens asymétriques restent asymétriques (mais le rôle des deux occurrences de la protéine A sont échangés). De plus, si le motif contenait un site libre, celui-ci est conservé mais change de nom tout en restant dans la même occurrence de la protéine A.

### 6.2.3 Échanges d'une paire de sites dans les occurrences d'une protéine dans une règle

Il est maintenant possible de définir l'effet des échanges de sites dans une règle. Il faut pour cela utiliser la relation implicite entre les occurrences de protéines du membre gauche et les occurrences de protéines du membre droit de la règle. Dans le sous-ensemble du langage Kappa considéré, comme les créations et les dégradations d'occurrences de protéines ne sont pas permises, chaque occurrence de protéine dans le membre gauche d'une règle correspond à une unique occurrence de protéine dans le membre droit, et réciproquement.

De ce fait, pour échanger les sites dans une règle, il suffit d'appliquer les mêmes échanges de sites au membre gauche et au membre droit de cette règle, c'est à dire appliquer, pour chaque occurrence de la protéine en question, le même échange de sites à gauche et à droite. Le résultat d'une telle transformation reste une règle d'interaction valide. Celle-ci est appelée le *symétrique* de la règle initiale, en précisant éventuellement par quel type d'échanges de sites.

**Exemple 6.2.3** Dans le modèle étudié dans ce chapitre, chaque règle, qu'elle soit d'association ou de disso- ciation, fait intervenir deux occurrences de la protéine A et chacune de ces occurrences documentent l'état de liaison des sites x et y. Il y a donc quatre échanges de sites possibles à opérer sur chaque règle. Leur effet est décrit en figure 6.18 et en figure 6.19.

Ne rien échanger laisse les règles telles quelles. Il est possible d'échanger l'état des sites x et y dans la première occurrence de la protéine A, ce qui est représenté en figure 6.18(a) (pour les règles de liaison) et en figure 6.19(a) (pour les règles de dissociation) par des doubles flèches ondulées de couleur verte. Il est possible d'échanger l'état des sites x et y dans la seconde occurrence de la protéine A, ce qui est représenté en figure 6.18(b) (pour les règles de liaison) et en figure 6.19(b) (pour les règles de dissociation) par des doubles flèches ondulées de couleur rouge. Enfin, il est possible de permuter l'état des sites x et y simultanément dans les deux occurrences de la protéine A(a) seconde occurrence de la protéine A, ce qui est représenté en figure 6.18(c) (pour les règles de liaison) et en figure 6.19(c) (pour les règles de dissociation) par des doubles flèches ondulées de couleur marron.

### 6.2.4 Échanges de sites dans les occurrences d'une protéine dans un plongement

L'application d'une règle repose sur l'existence d'un plongement du membre gauche de cette règle et le graphe représentant soit l'état du système, soit des configurations d'espèces biochimiques à transformer. Pour raisonner sur les échanges de sites au cours de l'exécution d'un modèle, nous avons donc besoin de définir le symétrique d'un plongement d'un motif dans un autre par un échange de sites. Les échanges de sites dans un plongement
<figure><img src="image_109.png" /><figcaption>(a) Échange des sites de l'occurrence gauche de la protéine A dans les règles de liaison.</figcaption></figure>

<figure><img src="image_110.png" /><figcaption>(b) Échange des sites de l'occurrence droite de la protéine A dans les règles de liaison.</figcaption></figure>

<figure><img src="image_111.png" /><figcaption>(c) Échanges des sites des deux occurrences de la protéine A dans les règles de liaison.</figcaption></figure>

Figure 6.18: Effet des échanges de sites dans les règles de liaison du modèle jouet.
<figure><img src="image_112.png" /><figcaption>(a) Échange des sites de l'occurrence gauche de la protéine A dans les règles de dissociation.</figcaption></figure>

<figure><img src="image_113.png" /><figcaption>(b) Échange des sites de l'occurrence droite de la protéine A dans les règles de liaison.</figcaption></figure>

<figure><img src="image_114.png" /><figcaption>(c) Échanges des sites des deux occurrences de la protéine A dans les règles de dissociation.</figcaption></figure>

Figure 6.19: Effet des échanges de sites dans les règles de dissociation du modèle jouet.
<figure><img src="image_115.png" /><figcaption>(a) Échange des sites dans les plongements vers les occurrences du monomère de la protéine A.</figcaption></figure>

<figure><img src="image_116.png" /><figcaption>(b) Échange des sites dans les plongements vers le motif constitué d'une occurrence de la protéine A avec le site x lié et le site y non documenté.</figcaption></figure>

**Figure 6.20:** Effet des échanges de sites sur les plongements vers des motifs constitués d'une seule occurrence de la protéine A.

d'un motif source dans un motif cible, est entièrement caractérisé par les échanges de sites appliqués sur le motif cible. Ensuite, chaque occurrence de protéines dans le motif source se voit appliquer le même échange de sites que ceux qui ont été appliqués à son image dans le motif cible. Ainsi, les échanges de sites qui s'appliquent aux occurrences de protéines du motif image sans antécédent n'ont pas d'effet sur le motif source.

Par construction, la correspondance entre les occurrences de protéines du motif source et ceux du motif cible est toujours valide dans leur symétrique. Du coup, celle-ci induit également un plongement entre le symétrique du motif source et le symétrique du motif cible. Nous appelons ce plongement le *symétrique* du plongement initial par échange des sites en question. On dit alors que ces deux plongements sont symétriques pour le type d'échanges de sites en question.

**Exemple 6.2.4** Des exemples de plongements symétriques sont donnés en figure 6.20, 6.21, 6.22, et en figure 6.23.

En figure 6.20, est décrit l'effet des échanges de sites sur des plongements vers les occurrences du monomère de la protéine A. L'image de ces plongements est donc un graphe constitué d'une occurrence de la protéine A, dont les deux sites sont libres. Quant à la source de ces plongements, cinq graphes à sites sont considérés. Ce sont en fait ceux qui se plongent dans le graphe cible, si l'on s'interdit de représenter un site d'interaction sans état de liaison. De ce fait, le graphe source peut être vide ou comporter une unique occurrence de la protéine A. Dans le second cas, l'occurrence de la protéine peut comporter aucun site d'interaction, l'un des deux sites d'interaction ou les deux sites d'interaction. Par ailleurs, les éventuels sites d'interaction sont libres car, d'une part, seuls les graphes dont chaque site documente son état de liaison sont considérés dans cet exemple et que, d'autre part, les sites ne peuvent être que libres pour que le motif source se plonge dans le graphe cible.

Quel est alors l'effet d'échanger les sites sur le graphe image du plongement ? Cet échange ne peut avoir une action visible que si des sites sont présents dans le graphe source. Ainsi, lorsque la source du plongement est le graphe vide ou lorsque cette source est constitué d'une occurrence de la protéine A sans site documenté, alors
<figure><img src="image_117.png" /><figcaption>Figure 6.21: Effet de l'échange des sites de l'occurrence gauche de la protéine A dans un plongement vers un motifs formé de deux occurrences de la protéine A.</figcaption></figure>
<figure><img src="image_118.png" /><figcaption>Figure 6.22: Effet de l’échange des sites de l’occurrence droite de la protéine A dans un plongement vers un motifs formé de deux occurrences de la protéine A.</figcaption></figure>
<figure><img src="image_119.png" /><figcaption>Figure 6.23: Effet des échanges des sites de chacune des occurrences de la protéine A dans un plongement vers un motifs formé de deux occurrences de la protéine A.</figcaption></figure>
l'échange de site est sans effet. Dans les autres cas, comme le rôle des sites x et y est échangé, les occurrences du site x deviennent des occurrences du site y, et réciproquement. Dans notre cas, les deux sites sont libres dans le graphe cible. De ce fait, si le graphe source ne contient que le site x, l'échange de sites donne un graphe qui ne contient que le site y et si le graphe source ne contient que le site y, l'échange de sites donne un graphe qui ne contient que le site x. Enfin, lorsque le graphe source contient les deux sites, il reste inchangé.

En figure 6.20(b), est représenté l'effet de l'échange des sites sur des plongements vers un motif constitué d'une seule occurrence de la protéine A, dont le site x est lié et dont le site y n'est pas documenté. Toujours en ne considérant que des graphes dont l'état des sites est documenté, il reste trois graphes qui se plongent dans ce graphe cible : le graphe vide ; le graphe constitué d'une occurrence de la protéine A, sans site, et le graphe constitué d'une occurrence de la protéine A avec le site x lié (le graphe cible). Ici encore, dans les deux premiers cas, le graphe source n'est pas affecté par l'échange des sites, puisque ce graphe n'a pas de sites. Dans le troisième cas, le site reste lié, mais devient un site y.

En figure 6.21, 6.22 et en figure 6.23, est représenté l'effet des échanges de sites dans des plongements vers un motif formé de deux occurrences de la protéine A connectées par leurs sites x respectifs, dont le site y d'une occurrence est libre et dont le site y de l'autre occurrence n'est pas documenté. Comme il y a deux occurrences de l'agent A, il est possible d'échanger les sites x et y dans la première instance de la protéine A, dans la seconde ou dans les deux. L'échange des sites x et y dans la première occurrence de la protéine A est représenté par des doubles flèches ondulées rouges en figure 6.21. L'échange des sites x et y dans la seconde occurrence de la protéine A est représenté par des doubles flèches ondulées vertes en figure 6.22. Les échanges simultanés des sites x et y dans les deux occurrences de la protéine A est représenté par des doubles flèches ondulées oranges en figure 6.23. Dans chacune de ces trois figures, les plongements sont représentées en commençant par le cas où la source est le graphe vide, puis par les cas où la source est un graphe formé d'une seule occurrence de la protéine A se plongeant dans la première occurrence de la protéine A du graphe cible (ce qui représente quatre cas, selon que l'état du site x et l'état du site y sont représentés ou non dans ce motif). Ensuite sont considérés les cas où la source est un graphe formé d'une seule occurrence de la protéine A se plongeant dans la seconde occurrence de la protéine A du graphe cible (ce qui représente deux cas, selon que l'état du site x est documenté ou non dans ce motif ; l'état du site y ne peut pas être documenté puisque le motif doit se plonger dans la seconde occurrence de la protéine A dans le motif cible). Enfin, sont considérés les cas où le motif source contient deux occurrences de la protéine A. Pour limiter le nombre de cas, seuls sont considérés ceux où les deux occurrences sont liées entre elles par leur site x respectifs. De ce fait, cela restreint l'ensemble de ces cas à deux, selon que l'état du site y de la première occurrence de la protéine A est représenté ou non.

Voici maintenant les remarques principales qui peuvent être faites sur ces exemples. D'une part, le motif source n'est transformé que s'il contient au moins une occurrence de la protéine A avec au moins un site et qui se plonge dans une occurrence de la protéine A du motif cible dont les sites x et y sont échangés. De ce fait, quand le motif source est vide, il n'est pas transformé. De plus, quand le motif source ne contient qu'une occurrence de la protéine A qui se plonge dans la seconde occurrence de la protéine A dans la motif cible et que seuls les sites x et y de la première occurrence de la protéine A sont échangés, le motif source n'est pas modifié non plus (voir en figure 6.21). C'est aussi le cas lorsque le motif source ne contient qu'une occurrence de la protéine A et que celle-ci se plonge dans la première occurrence de la protéine A alors que seuls les sites x et y de la seconde occurrence de la protéine A sont échangés (voir en figure 6.22).

## 6.2.5 Échanges d'une paire de sites dans les occurrences d'une protéine dans le raffinement d'une règle

Les pas de calculs de la sémantique stochastique et les réactions de la sémantique différentielle sont obtenus en raffinant les règles (voir en section 5.1.3). Le but de cette partie est de définir l'effet de l'échange d'une paire de sites dans le raffinement d'une règle.

Appliquer des échanges de sites sur le raffinement d'une règle consiste à appliquer ces échanges de sites sur la règle raffinée, puis à propager ces échanges le long du plongement entre le membre gauche de la règle initiale et le membre gauche de la règle raffinée. Il suffit alors d'appliquer à la règle initiale l'effet de ces échanges de sites. Le symétrique de la règle raffinée par ces échanges de sites est alors un raffinement du symétrique de la règle initiale le long du symétrique du plongement entre le membre gauche de la règle initiale et le membre gauche de sa règle raffinée. Ce raffinement est alors appelé le *symétrique* du raffinement initiale par les échanges de la paire de sites en question.

**Exemple 6.2.5** *En Figure 6.24 sont donnés deux exemples de raffinement de pas de calculs.*
<figure><img src="image_120.png" /></figure>

Figure 6.24: Deux exemples de raffinements de pas de calculs. Dans le premier 6.24(a) est appliqué un échange de sites dans un pas de calcul consistant à associer les deux sites x de deux occurrences du monomère de la protéine A dans un état formé de quatre occurrences de la protéine A, deux libres et deux liées par leurs sites x respectifs. L'échange de sites porte sur l'occurrence gauche de la protéine A dans l'occurrence du dimère. De ce fait, son action ne concerne pas la règle d'interaction qui est donc gardée telle quelle lorsque cet échange est restreint à celle-ci. Dans le second 6.24(b), un échange de sites est appliqué à une réaction - ou un pas de calcul - qui consiste à enlever une liaison entre les deux sites x de deux occurrences de la protéine A. L'échange porte sur l'occurrence de gauche de la protéine A. Le résultat de cet échange est donc une dissociation entre deux occurrences de la protéine A liées par le site y de l'occurrence gauche de la protéine et leur site x de l'occurrence droite de la protéine. Ceci impose de remplacer la règle d'interaction qui a engendré la réaction - ou le pas de calcul - par sa règle symétrique.

Le premier exemple illustre le cas où les échanges de sites ont lieu dans des occurrences de protéines qui ne concernent par l'application de la règle d'interaction. Ainsi, en Figure 6.24(a) est considéré l'application d'une règle d'association symétrique entre les sites x de deux occurrences de la protéine A, à un état formé de quatre occurrences de la protéine A, deux libres (qui vont donc se lier par l'application de la règle) et deux déjà liées par leurs sites x respectifs. L'échange de sites opère dans l'occurrence gauche des deux occurrences de la protéine A déjà liées. Ces deux occurrences ayant été ajoutées pour le raffinement de la règle d'interaction, ils ne sont pas l'image d'occurrences de la protéine A du membre gauche de cette règle. De ce fait, le pas de calcul initial et son symétrique sont tous deux engendrés par la même règle d'interaction.

Dans le second exemple, donné en Figure 6.24(b), un échange entre une paire de sites intervient dans un pas de calcul qui consiste à retirer la liaison entre les deux sites x de deux occurrences de la protéine A. Cela peut être pris non seulement comme un pas de calcul, mais aussi comme une réaction, car aucune nouvelle composante connexe n'a été ajoutée dans le raffinement de la règle. L'échange de sites porte sur l'occurrence gauche de l'occurrence de la protéine A. Le résultat est un pas de calcul - ou une réaction - qui retire une liaison entre le site x d'une occurrence de la protéine A et le site y d'une autre occurrence de cette protéine. Pour ce faire, il faut utiliser une règle de déliaison asymétrique. C'est bien ce qui est obtenu en restreignant l'échange de sites le long du plongement entre le membre gauche de la règle d'interaction et le membre gauche du pas de calcul - ou de la réaction.

Dans le symétrique d'un raffinement de règle, le symétrique de la règle de base n'est pas nécessairement une règle du modèle en question. Ainsi la réaction ou le pas de calcul obtenu n'est pas nécessairement une réaction ou un pas de calcul de ce modèle, et même dans ce cas, des conditions sur les constantes d'interaction correspondantes doivent être vérifiées pour engendrer des propriétés quantitatives sur le comportement du
modèle. Ceci sera l'objet de la section 6.3.1.2.

## 6.3 Symétries et conséquences sur le comportement des modèles

Après avoir examiné l'effet des échanges de sites sur les motifs, leurs plongements et les règles d'interaction, il est temps de se définir sous quels conditions un ensemble de règles, un état de la sémantique différentielle ou une distribution d'états de la sémantique stochastique sont symétriques par rapport à un type d'échanges de sites dans une ou plusieurs occurrences d'une protéine. Ceci sera fait en examinant leurs orbites qui sont obtenues à partir d'un objet de départ en appliquant toutes les combinaisons d'échanges de sites possibles. Les symétries permettent de déduire des propriétés sur le comportement des modèles, ce qui prendra la forme de bisimulations en avant ou en arrière.

### 6.3.1 Ensembles de règles

Sous certaines conditions, un ensemble de règle peut être symétrique par rapport à un type d'échanges de sites. Ceci permet de considérer les différentes sémantiques à échange de sites près.

#### 6.3.1.1 Orbites de règles d'interaction

L'orbite d'une règle d'interaction, selon une paire de sites, regroupe toutes les manières de transformer cette règle, en échangeant cette paire de sites dans un sous-ensemble des occurrences de la protéine en question. Au sein d'une même orbite, la règle de départ n'est pas importante. En effet, les échanges de sites éventuels entre deux règles peuvent s'annuler en échangeant les deux sites de nouveau dans les mêmes occurrences de la protéine A. De ce fait, les orbites regroupent les règles en classes d'équivalence. Elle définissent les règles qui établissent la même transformation sur les graphes à sites, modulo les échanges de la paire de sites en question.

**Exemple 6.3.1** Les règles du modèle dessinées en section 6.1.1.1 présentent exactement deux orbites. Celles-ci sont données en figure 6.25. La première orbite, voir en figure 6.25(a), regroupe les règles qui établissent une liaison entre les deux occurrences de la protéine A, alors que la seconde, voir en figure 6.25(b), regroupe les règles qui brisent une liaison.

À noter que chaque règle de liaison et de dissociation symétrique apparaît exactement une fois dans son orbite respective. Les règles asymétriques apparaissent exactement deux fois, quitte à échanger l'occurrence de droite et de gauche dans ces règles.

#### 6.3.1.2 Ensembles symétriques de règles

Pour vérifier si deux sites jouent exactement le même rôle dans un ensemble de règles, il suffit d'en inspecter les orbites.

Dans un premier temps, il faut vérifier que si un modèle comporte une règle donnée, alors elle comporte également toutes les autres règles de son orbite, c'est à dire, toutes les règles qui peuvent être obtenues en échangeant ces deux sites dans une ou plusieurs occurrences de la protéine en question. Toutefois, une règle peut compter pour une règle équivalente par isomorphisme de règle (voir page 21). Dans un second temps, il faut s'assurer que leurs constantes d'interaction sont proportionnelles à leurs nombres d'apparitions dans l'orbite.

**Exemple 6.3.2** Dans l'exemple de la section 6.1.1.1, les règles symétriques (celles qui agissent sur deux sites x ou sur deux sites y) apparaissent chacune une fois dans leurs orbites respectives, alors que les règles asymétriques (celles qui agissent sur un site x et un site y) apparaissent sous deux formes isomorphes quitte à changer l'ordre des occurrences de la protéine A. Ainsi pour que l'ensemble des règles du modèle soit symétrique, il faut que les contraintes suivantes soient vérifiées :

$$ \frac{k_{xx}}{1} = \frac{k_{yy}}{1} = \frac{k_{xy}}{2} \qquad \text{et} \qquad \frac{k_{xx}^d}{1} = \frac{k_{yy}^d}{1} = \frac{k_{xy}^d}{2}. $$

Dans ces fractions, le dénominateur représente le nombre de formes de la règle (à permutation des agents près) qui apparaissent dans les catégories de règles.

De ce fait, les contantes d'interaction pour les liaisons symétriques doivent être égales, alors que la constante d'interaction pour les liaisons asymétriques doit être égale au double de cette valeur commune. Il en
<figure><img src="image_121.png" /><figcaption>Figure 6.25: Quitte à échanger les sites x et y dans certaines occurrences de la protéine A, les règles se regroupent en deux catégories. Les règles d'association sont représentées en figure 6.25(a), alors que les règles de dissociation sont représentées en figure 6.25(b). L'effet des échanges de sites est représenté par des doubles flèches ondulées. Les échanges des sites x et y dans l'occurrence gauche de la protéine sont représentés en vert, alors ceux dans l'occurrence de droite sont représentés en rouge.</figcaption></figure>

est de même pour les constantes d'interaction des règles de dissociation. On retrouve ainsi les contraintes sur les constantes d'association et les constantes de dissociation qui avaient permis, d'une part, de quotienter la sémantique différentielle et la sémantique stochastique en section 6.1.3.1 et, d'autre part, de faire émerger des invariants quantitatifs en section 6.1.3.2.

### 6.3.1.3 Orbites de motifs

Les ensembles symétriques de règles assurent des propriétés sur les pas de calculs. Toutefois, de telles règles ne produisent pas les différents états dans les mêmes proportions. Il convient donc d'inspecter les orbites formées par les graphes à sites lorsque des paires de sites sont échangées pour comprendre les rapports de proportionnalités qui vont apparaître. Ces orbites sont, une fois encore, obtenues en échangeant une paire de sites dans une occurrence d'une protéine donnée dans un motif.

**Exemple 6.3.3** Dans le cadre de l'exemple du modèle introduit en section 6.1.1.1, l'exemple d'une orbite pour un motif est donné en figure 6.26. Ce motif en question est formé de trois occurrences de la protéine A. Une occurrence, celle du dessous, est libre, alors que les deux autres, au dessus, sont liées. Comme il y a trois
<figure><img src="image_122.png" /><figcaption>Figure 6.26: Orbite du motif formé d'une configuration du dimère et d'une configuration du monomère de la protéine A.</figcaption></figure>
<figure><img src="image_123.png" /><figcaption>Figure 6.27: Les différentes étapes de calcul pour lier deux occurrences libres de la protéine A.</figcaption></figure>

occurrences de la protéine A dans lesquelles les sites x et y peuvent être échangés, l'orbite de ce graphe à sites peut être décrite sous la forme d'un cube, chacune des dimensions correspondant à l'échange des sites dans l'une de ces trois occurrences. Les échanges des sites x et y dans l'occurrence de gauche de la protéine A dans les dimères sont représentés en rouge, ceux dans l'occurrence de droite en vert. Enfin, les échanges des sites x et y dans l'occurrence du monomère de la protéine A sont représentés en bleu. Dans ce dernier cas, comme les deux sites des occurrences de la protéine A sont libres, leur échange ne change pas le motif.

Au sein de l'orbite, le graphe à sites formé de deux occurrences de la protéine A liées entre-elles par leurs sites x et d'une occurrence libre, apparaît 2 fois. Il en est de même pour le graphe à sites formé de deux occurrences de la protéine A liées entre-elles par leurs sites y et d'une occurrence libre. Enfin, le graphe à sites formés de deux occurrences de la protéine A liées entre-elles par un site x et un site y et d'une occurrence libre apparaît, lui, 4 fois.

### 6.3.1.4 Propriété fondamentale

La propriété fondamentale des ensembles symétriques de règles peut désormais être formulée.

**Théorème 6.3.1 (Bisimulation avant-arrière)** Dans un modèle dont l'ensemble des règles est symétrique par rapport à un type d'échanges de sites dans les occurrences d'une protéine donnée, étant donné un pas de calcul entre un état q et un état q', et le symétrique de ce pas de calcul entre l'état $q_σ$ et un état $q'_σ$, alors les quantités $\tau(\{q\}, \{q'\})$ et $\tau(\{q_σ\}, \{q'_σ\})$ définies respectivement comme la somme pour chaque pas de calcul entre l'état q (resp. $q_σ$) et un état équivalent à q' (resp. $q'_σ$) à isomorphisme près (voir page 18) de la constante d'interaction de la règle qui a engendré ce pas de calcul sont proportionnelles au nombre d'apparitions $w(q)$ et $w(q')$ d'états isomorphes à q et à q' dans leurs orbites respectives :

$$w(q') \cdot \tau(\{q\}, \{q'\}) = w(q) \cdot \tau(\{q_σ\}, \{q'_σ\}).$$

**Exemple 6.3.4** Une illustration du théorème 6.3.1 est donnée en examinant la somme des constantes d'interaction
<figure><img src="image_124.png" /><figcaption>Figure 6.28: Les différentes étapes de calcul pour dissocier deux occurrences liées de la protéine A.</figcaption></figure>

pour les différents types de liaison et les dissociation entre les occurrences de la protéine A dans le modèle introduit en section 6.1.1.1.

* Lorsque l'ensemble des règles est symétrique, les liaisons entre un site x et un site y se forment deux fois plus souvent que celles entre deux sites x et que celles entre deux sites y.

Étant données deux occurrences libres de la protéine A, chacune des trois règles de liaison peut s'appliquer selon deux plongements (voir en figure 6.27). Ceci donne comme somme des constantes d'interaction $2 \cdot k_{xx}$ pour une liaison entre les deux sites x, $2 \cdot k_{yy}$ pour une liaison entre les deux sites y, et $2 \cdot k_{xy}$ pour une liaison entre un site x et un site y. Or dans les ensembles symétriques de règles, les constantes $k_{xx}$ et $k_{yy}$ sont égales, alors que la constante $k_{xy}$ est égale au double de la constante $k_{xx}$. Les sommes des constantes d'interaction sont donc bien proportionnelles au nombre d'occurrences des configurations du dimère de la protéine A dans leur orbite, sachant que la configuration asymétrique y apparaît deux fois, alors que chaque configuration symétrique y apparaît exactement une fois.

* Lorsque l'ensemble des règles est symétrique, les liaisons entre les occurrences de la protéine A se séparent toutes au même rythme.

En effet, les occurrences des configurations symétrique des dimères se séparent avec la constante d'interaction $k_{xx}^d$ ou $k_{yy}^d$ selon leur type. Cependant, il existe deux manières d'appliquer la règle correspondante, ce qui donne une somme de constantes égale à $2 \cdot k_{xx}^d$ ou $2 \cdot k_{yy}^d$. Par ailleurs, il n'existe qu'une manière d'appliquer la règle de dissociation pour les configurations de dimère asymétriques, ce qui donne une somme égale à $k_{xy}^d$. Comme dans les ensembles symétriques de règles, les deux constantes $k_{xx}^d$ et $k_{yy}^d$ sont égales et que la constante $k_{xy}^d$ est égale au double de la constante $k_{xx}^d$, le comportement attendu est bien obtenu.

Une conséquence directe du théorème 6.3.1, est qu'un ensemble symétrique de règles engendre à la fois une bisimulation en avant et une bisimulation en arrière.

Ainsi la propriété suivante s'obtient en sommant pour les états cibles, sur tous les états d'une classe de symétrie.
**Propriété 6.3.1 (Bisimulation en avant)** Dans un modèle dont l'ensemble des règles est symétrique par rapport à un type d'échanges de sites dans les occurrences d'une certaine protéine, étant donnés deux états symétriques q et q', et un autre état q'' d'équivalence d'états C, alors la somme $\tau(\{q\}, [q''])$ et la somme $\tau'(\{q'\}, [q''])$ définies respectivement comme la somme pour chaque pas de calcul entre l'état q (resp. q') et un état isomorphe à un état symétrique à q'' de la constante d'interaction de la règle d'interaction qui a engendré ce pas de calcul sont égales :

$$ \tau(\{q\}, [q'']) = \tau'(\{q'\}, [q']). $$

La propriété 6.3.1 indique que deux états symétriques ont toujours le même comportement vis à vis d'une classe d'équivalence d'états.

La propriété suivante s'obtient, elle, en sommant pour les états départs, sur tous les états d'une classe de symétrie.

**Propriété 6.3.2 (Bisimulation en arrière)** Dans un modèle dont l'ensemble des règles est symétrique par rapport à un type d'échanges de sites dans les occurrences d'une certaine protéine, étant donnés deux états symétriques q et q', alors :

1. d'une part, la somme $\tau(\{q\}, \_)$ et la somme $\tau(\{q'\}, \_)$ définies respectivement comme la somme pour chaque pas de calcul issu de l'état q (resp. q') des constantes d'interaction de la règle qui a engendré ce pas de calcul sont égales (quelque soit l'état d'arrivée), sont égales :

$$ \tau(\{q\}, \_) = \tau'(\{q'\}, \_); $$

2. et, d'autre part, pour tout état q'', la somme $\tau([q''], \{q\})$ et la somme $\tau'([q''], \{q'\})$ définies respectivement comme la somme pour chaque pas de calcul entre un état symétrique à l'état q'' et l'état q (resp. q') à isomorphisme près, de la constante d'interaction de la règle qui a engendré ce pas de calcul, sont proportionnelles au nombre d'apparition $w(q)$ et $w(q')$ d'états isomorphes à q et à q' :

$$ w(q') \cdot \tau([q''], \{q\}) = w(q) \cdot \tau'([q''], \{q'\}). $$

La propriété 6.3.2 indique que d'une part, le système avance à la même vitesse pour toute paire d'états symétriques, et que d'autre part, le comportement du système préserve les rapports de proportionnalité.

## 6.3.2 Effet des symétries dans la sémantique différentielle

Le but de cette partie est de donner sous quelles conditions suffisantes des symétries dans un ensemble de règles d'interaction induisent des propriétés quantitatives dans le modèle différentiel induit par ces règles.

### 6.3.2.1 Orbites des configurations d'espèces biochimiques

Pour ce faire, il faut regarder l'effet des échanges de sites sur les configurations d'espèces biochimiques. En effet, ce sont leurs quantités respectives qui constituent les variables des systèmes différentiels engendrés par les ensembles de règles de réécriture de graphes à sites.

Les configurations d'espèces biochimiques sont des motifs particuliers. Comme le symétrique d'une configuration d'une espèce biochimique par échange de sites est lui-même la configuration d'une espèce biochimique, il est possible de les regrouper en classe d'équivalence en calculant leurs orbites.

**Exemple 6.3.5** Dans le modèle donné en section 6.1.1.1, les configurations d'espèces biochimiques se classent exactement en deux classes d'équivalence, lorsque l'état de liaison des sites x et y des occurrences de la protéine A est échangé : l'unique configuration du monomère, d'une part, et les configurations du dimère, d'autre part. Ces deux orbites sont dessinées en Figure 6.29.

Les monomères existent sous une seule forme (voir en figure 6.29(a)). Ils ne sont pas modifiés par l'échange de leurs sites x et y. Les dimères existent sous trois formes, selon que la liaison entre les deux occurrences de la protéine A se fasse sur les deux sites x des occurrences de la protéine, sur leurs deux sites y ou sur un site x et un site y (voir en Figure 6.29(b)). Cette dernière forme est représentée deux fois, sous deux formes isomorphes quitte à intervertir l'ordre des deux occurrences de la protéine A.
<figure><img src="image_125.png" /><figcaption>Figure 6.29: Quitte à permuter les sites $x$ et $y$ dans les occurrences de la protéine $A$, les configurations d'espèces biochimiques se classent en deux catégories, celles du monomère de la protéine $A$ (voir en figure 6.29(a)) et celles du dimère de la protéine $A$ (voir en figure 6.29(b)). Pour la configuration du monomère, la seule transformation possible consiste à permuter les sites de l'unique occurrence de la protéine (ce qui est dessiné avec une double flèche ondulée orange). Ceci ne change par la configuration de la protéine puisque l'ordre des sites n'a pas d'importance dans le langage Kappa. Pour les configurations du dimère, les rôles des sites peuvent être échangés dans l'occurrence gauche (ce qui est dessiné avec une double flèche ondulée verte) ou dans l'occurrence droite (rouge). Quitte à changer l'ordre des agents et des sites de liaisons, les deux représentations graphiques de configurations asymétriques du dimère sont isomorphes.</figcaption></figure>

### 6.3.2.2 Bisimulation en avant

Le but de cette section est de montrer que les symétries dans un ensemble de règles d'interactions induisent une relation de bisimulation sur les états des modèles différentiels qu'elles induisent.

Cette relation consiste à regrouper la quantité des configurations symétriques d'espèces biochimiques. Il suffit pour cela de choisir une représentante pour chaque classe d'équivalence. Ceci permet de définir une fonction $r$ qui associe à chaque configuration d'une espèce biochimique, la configuration symétrique qui est la représentante de sa classe d'équivalence. La fonction $r$ est une fonction idempotente (ainsi $r \circ r = r$). Cette fonction permet de définir deux fonctions sur les états différentiels. La première, $P_r$, regroupe la quantité des configurations d'espèces biochimiques sur les représentantes de leurs classes d'équivalence respectives, alors que la seconde, $Z_r$, annule la quantité des configurations d'espèces biochimiques qui ne sont pas les représentantes de leurs classes d'équivalence respectives.

Ceci donne les définitions suivantes :

$$P_r(\rho) = \begin{cases} \mathcal{V} \to \mathbb{R} \\ v \mapsto \sum \{\rho(v') | r(v') = v\} & \text{si } r(v) = v \\ v \mapsto 0 & \text{sinon,} \end{cases}$$

$$Z_r(\rho) = \begin{cases} \mathcal{V} \to \mathbb{R} \\ v \mapsto \rho(v) & \text{si } r(v) = v \\ v \mapsto 0 & \text{sinon.} \end{cases}$$

**Exemple 6.3.6** Dans le modèle jouet introduit en section 6.1.1.1, il existe deux classes d'équivalence de configurations d'espèces biochimiques pour les échanges entre les sites $x$ et $y$ dans les occurrences de la protéine $A$, selon le nombre d'occurrences de cette protéine dans l'espèce biochimique en question. La classe de configuration du monomère est réduite à un élément qui est donc la représentante de sa classe d'équivalence. Pour les configurations du dimère de la protéine $A$, la configuration choisie comme représentante de sa classe d'équivalence est celle où les deux occurrences de la protéine $A$ sont liées par leurs sites $x$ respectifs.
Les fonctions $P_r$ et $Z_r$ prennent alors les valeurs suivantes :

$$P_r(\rho) = \begin{cases} A & \mapsto \rho(A) \\ A.x - x.A & \mapsto \rho(A.x - x.A) + \rho(A.y - y.A) + \rho(A.x - y.A) \\ A.y - y.A & \mapsto 0 \\ A.x - y.A & \mapsto 0 \end{cases}$$

$$Z_r(\rho) = \begin{cases} A & \mapsto \rho(A) \\ A.x - x.A & \mapsto \rho(A.x - x.A) \\ A.y - y.A & \mapsto 0 \\ A.x - y.A & \mapsto 0 \end{cases}$$

Les fonctions $P_r$ et $Z_r$ sont des projections linéaires. En effet, elles sont toutes deux linéaires et idempotentes. Par ailleurs, elles ont la même image, à savoir l'ensemble des états qui associent la quantité 0 à toutes les configurations d'espèces biochimiques qui ne sont pas les représentantes de leurs classes d'équivalence respectives. De ce fait, le diagramme suivant :

<figure><img src="image_126.png" /></figure>

commute, ce qui signifie que les fonctions $P_r$ et $Z_r \circ P_r$ sont égales.

Lorsque l'ensemble de règles est symétrique, la fonction $P_r$ induit une bisimulation sur l'ensemble des états de la sémantique différentielle du modèle engendrée par ces règles. En effet, pour deux états $X$ et $X'$ tels que $P_r(X) = P_r(X')$, le théorème 6.3.1 permet de montrer que l'égalité suivante : $P_r(\mathbb{F}(X)) = P_r(\mathbb{F}(X'))$ est également satisfaite.

De manière équivalente, le diagramme suivant :

<figure><img src="image_127.png" /></figure>

commute, ce qui signifie que les fonctions suivantes $P_r \circ \mathbb{F}$ et $P_r \circ \mathbb{F} \circ P_r$ sont égales.

Ainsi:

$$P_r \circ \mathbb{F} = P_r \circ \mathbb{F} \circ P_r \\ P_r \circ \mathbb{F} = P_r \circ \mathbb{F} \circ [Z_r \circ P_r] \\ P_r \circ \mathbb{F} = [P_r \circ \mathbb{F} \circ Z_r] \circ P_r$$

ce qui peut se résumer par la diagramme commutatif suivant :

<figure><img src="image_128.png" /></figure>

Ce diagramme définit une réduction de modèle (voir en section 4.3) avec pour fonction d'abstraction $P_r$ et pour contre-partie abstraite à la fonction $\mathbb{F}$ la fonction $P_r \circ \mathbb{F} \circ Z_r$.
**Exemple 6.3.7** Dans le modèle jouet introduit en section 6.1.1.1, la fonction $\mathbb{F}$ est définie de la manière suivante :

$$ \mathbb{F}(\rho) = \left\{ \begin{array}{ll} A & \mapsto 2k_{xy}^d \rho(A.x - y.A) + 2k_{yy}^d 2\rho(A.y - y.A) + 2k_{xx}^d 2\rho(A.x - x.A) - (2k_{yy} + 2k_{xx} + 2k_{xy}) \rho(A)^2 \\ A.x - x.A & \mapsto 2k_{xx}\rho(A)^2 - k_{xx}^d 2\rho(A.x - x.A) \\ A.y - y.A & \mapsto 2k_{yy}\rho(A)^2 - k_{yy}^d 2\rho(A.y - y.A) \\ A.x - y.A & \mapsto 2k_{xy}\rho(A)^2 - k_{xy}^d \rho(A.x - y.A). \end{array} \right. $$

La composition à droite avec la fonction $Z_r$ annule la contribution des configurations d'espèces biochimiques qui ne sont pas les représentantes de leurs classes d'équivalence. Cela élimine donc les occurrences des variables $A.y - y.A$ et $A.x - y.A$ dans la fonction $\mathbb{F}$.

Ainsi:

$$ [\mathbb{F} \circ Z_r](\rho) = \left\{ \begin{array}{ll} A & \mapsto 2k_{xx}^d 2\rho(A.x - x.A) - (2k_{yy} + 2k_{xx} + 2k_{xy}) \rho(A)^2 \\ A.x - x.A & \mapsto k_{xx}\rho(A)^2 - k_{xx}^d 2\rho(A.x - x.A) \\ A.y - y.A & \mapsto k_{yy}\rho(A)^2 \\ A.x - y.A & \mapsto k_{xy}\rho(A)^2. \end{array} \right. $$

Enfin, la composition à gauche avec la fonction $P_r$ regroupe les différentes contributions sur les représentantes de leurs classes d'équivalence.

Ainsi:

$$ [P_r \circ \mathbb{F} \circ Z_r](\rho) = \left\{ \begin{array}{ll} A & \mapsto 2k_{xx}^d 2[A.x - x.A] - (2k_{yy} + 2k_{xx} + 2k_{xy}) [A]^2 \\ A.x - x.A & \mapsto (k_{xx} + k_{yy} + k_{xy}) [A]^2 - k_{xx}^d 2[A.x - x.A] \\ A.y - y.A & \mapsto 0 \\ A.x - y.A & \mapsto 0. \end{array} \right. $$

Ce qui correspond à l'équation différentielle pour le modèle simplifié suivante :

$$ \left\{ \begin{array}{l} A_1 \mapsto 2K^d 2\rho(A_2) - 2K\rho(A_1)^2 \\ A_2 \mapsto K\rho(A_1)^2 - 2K^d \rho(A_2). \end{array} \right. $$

La bisimulation en avant prouve alors les résultats observés en figure 6.14(b) et 6.14(f), à savoir que les trajectoires de concentrations dans le modèle réduit sont bien la somme des trajectoires des quantités de configurations d'espèces biochimiques correspondantes dans le modèle initial dès lors que l'ensemble de règles est symétrique et sans imposer que l'état initial le soit.

### 6.3.2.3 Bisimulation en arrière

Le but de cette section est de montrer que les symétries dans un ensemble de règles d'interactions permettent d'assurer des invariants sur les quantités de configurations d'espèces biochimiques, puis d'utiliser ces invariants pour éliminer des variables dans le système d'équations différentielles engendré par l'ensemble de règles en question.

Il faut dans un premier temps définir la notion de symétrie pour les états de la sémantique différentielle par rapport à un type d'échanges de sites. Les états de la sémantique différentielle sont des fonctions qui associent à chaque configuration d'espèces biochimiques, un réel positif qui représente sa quantité. Un tel état est dit symétrique par rapport à un type d'échanges de sites, si, pour toute paire de configurations symétriques d'espèces biochimiques pour ce type d'échanges de sites, les quantités présentes de ces deux configurations sont proportionnelles à leurs nombres de répétitions dans l'orbite correspondante.

**Exemple 6.3.8** L'orbite des configurations potentielles du monomère de la protéine A du modèle introduit en section 6.1.1.1 n'est formée que d'un élément. Par contre, celle pour les configurations du dimère de la protéine A comporte les configurations symétriques du dimère avec une liaison entre les deux sites x ; les configuration symétriques du dimère avec une liaison entre les deux sites y et les configuration asymétriques du dimère avec une liaison entre le site x d'une occurrence de la protéine A et le site y de l'autre occurrence de la protéine A. À isomorphisme près, cette dernière configuration apparaît deux fois dans son orbite.
En conséquence, les états symétriques de la sémantique différentielle sont ceux tels que la quantité de configuration asymétriques des dimères représente la moitié de la quantité totale en dimère et la quantité de chacune des deux configurations symétriques du dimère de la protéine A représentent chacune un quart de la quantité totale en dimère. Il s'agit des mêmes proportions que pour le jeu de "pile" ou "face".

La propriété 6.3.2 assure, par sommation, que dans un modèle engendré par un ensemble symétrique de règles par rapport à un type d'échanges de sites, si X est un état symétrique par rapport ce type d'échanges de sites, alors il en est de même pour $F(X)$. Puis, comme les combinaisons linéaires de deux états symétriques par rapport à un type d'échanges de sites, sont également symétriques par rapport à ce type d'échanges de sites, il en résulte que le système reste dans un état symétrique par rapport à ce type d'échanges de sites tout au long de son exécution.

**Exemple 6.3.9** Il est maintenant possible de justifier les constatations qui avaient été faites en figure 6.15(b). En effet, pour les paramètres cinétiques $k_{xx} = k_{yy} = 0.5$, $k_{xy} = 1$, $k_{xx}^d = k_{yy}^d = 1$ et $k_{xy}^d = 2$ et un état initial formé uniquement de la configuration du monomère de la protéine A, à la fois l'ensemble des règles et l'état initial du système sont symétriques par rapport aux échanges des sites x et y dans les occurrences de la protéine A. En conséquence, l'état du système reste symétrique pour ces échanges de sites tout au long de l'exécution du système. Ainsi la quantité de configurations du dimère avec les deux sites x reste toujours égale à la quantité de configurations du dimère avec les deux sites y, alors que la quantité de configurations du dimère formé par une liaison entre le site x d'une occurrence de la protéine et le site y de l'autre occurrence reste égale au double.

Il est alors possible d'éliminer des variables en utilisant cette propriété. Pour cela, il faut choisir une représentante pour chaque classe d'équivalence modulo les échanges de cette paire de sites dans les configurations d'espèces biochimiques. La représentante d'une configuration d'espèce biochimique $v$ est notée $r(v)$. Ainsi $r: \mathcal{V} \to \mathcal{V}$ est une fonction idempotente (c'est à dire $r \circ r = r$) de l'ensemble des configurations des espèces biochimiques dans lui-même. On note également $w: \mathcal{V} \to \mathbb{N} \setminus \{0\}$ la fonction qui a chaque configuration d'une espèce biochimique, associe son nombre d'occurrences dans son orbite pour les échanges de la paire de sites en question.

Deux fonctions de l'ensemble des états $\mathcal{V} \to \mathbb{R}$ vers lui-même sont définies ci-dessous. La première $Eq_r$ a pour but de remplacer les occurrences des variables qui ne sont pas les représentantes de leurs classes d'équivalence par des occurrences de leurs représentantes respectifs avec des coefficients pour tenir des rapports de proportionnalité dans les états symétriques. La seconde $Z_r$ a pour but d'annuler la valeur des variables qui ne sont pas les représentantes de leurs classes d'équivalence.

Ceci donne les définitions suivantes :

$$Eq_r(\rho) : \begin{cases} \mathcal{V} \to \mathbb{R} \\ v \mapsto \frac{w(v)}{w(r(v))} \cdot \rho(r(v)) \end{cases}$$

$$Z_r(\rho) : \begin{cases} \mathcal{V} \to \mathbb{R} \\ v \mapsto \rho(v) & \text{si } r(v) = v \\ v \mapsto 0 & \text{sinon.} \end{cases}$$

Les fonctions $Eq_r$ et $Z_r$ sont deux projections linéaires, mais cette fois-ci leurs images sont différentes. Grâce à la fonction $Eq_r$, il est possible de proposer une nouvelle manière de caractériser les états symétriques par rapport au type d'échanges de sites en question. En effet, les états $\rho$ sont symétriques si et seulement si ils sont égaux à leurs propres images par la fonction $Eq_r$, c'est à dire si $Eq_r(\rho) = \rho$.

**Exemple 6.3.10** Dans le modèle jouet qui est étudié en section 6.1.1.1, il existe deux classes d'équivalence de configurations d'espèces biochimiques pour les échanges entre les sites x et y dans les occurrences de la protéine A, selon le nombre d'occurrences de cette protéine dans l'espèce biochimique en question. La classe des monomères est réduite à un élément qui est dont la représentante de sa classe d'équivalence. Pour les dimères, la configuration choisie comme représentante est celle où les deux occurrences de la protéine A sont liées par leurs sites x respectifs.

Les fonctions $Z_r$ et $Eq_r$ sont définies de la manière suivante :

$$Eq_r(\rho) = \begin{cases} A \mapsto \rho(A) \\ A \cdot x - x \cdot A \mapsto \frac{1}{1} \cdot \rho(A \cdot x - x \cdot A) \\ A \cdot y - y \cdot A \mapsto \frac{1}{1} \cdot \rho(A \cdot x - x \cdot A) \\ A \cdot x - y \cdot A \mapsto \frac{2}{1} \cdot \rho(A \cdot x - x \cdot A) \end{cases}$$

$$Z_r(\rho) = \begin{cases} A \mapsto \rho(A) \\ A \cdot x - x \cdot A \mapsto \rho(A \cdot x - x \cdot A) \\ A \cdot y - y \cdot A \mapsto 0 \\ A \cdot x - y \cdot A \mapsto 0. \end{cases}$$
Soit $\rho$ un état, la propriété $Eq_r(\rho) = \rho$ est équivalente à l'ensemble des contraintes suivantes :

$$
\left\{
\begin{array}{l}
\rho(A) = \rho(A) \\
\rho(A \cdot x - x \cdot A) = \rho(A \cdot x - x \cdot A) \\
\rho(A \cdot y - y \cdot A) = \rho(A \cdot x - x \cdot A) \\
\rho(A \cdot x - y \cdot A) = 2 \cdot \rho(A \cdot x - x \cdot A),
\end{array}
\right.
$$

ce qui correspond bien aux critères pour qu’un état soit symétrique par rapport aux échanges des sites x et y dans les occurrences de la protéine A.

Les trois diagrammes suivants sont utilisés pour construire l'élimination des variables qui ne sont pas les représentantes de leurs classes d'équivalence :

<figure><img src="image_129.png" /></figure>

Ces trois diagrammes commutent. Le premier diagramme vient du fait que la fonction $Eq_r$ est idempotente, car c'est une projection linéaire. Ainsi $Eq_r = Eq_r \circ Eq_r$ ce qui constitue le premier diagramme. Ensuite, d'une part, le fonction $Z_r$ ne change que la valeur des variables qui ne sont pas les représentantes de leurs classes d'équivalence et d'autre part, la fonction $Eq_r$ ne dépend pas de ces variables. Il en découle que $Eq_r = Eq_r \circ Z_r$ ce qui constitue le second diagramme commutatif. Enfin, le troisième diagramme provient du fait que l'image par $\mathbb{F}$ d'un état symétrique est lui même symétrique. En effet, pour tout état $\rho \in \mathcal{V} \to \mathbb{R}$, l'état $Eq_r(\rho)$ est symétrique, puis comme la fonction $\mathbb{F}$ préserve l'ensemble des états symétriques, $\mathbb{F}(Eq_r(\rho))$ est un état symétrique, ce qui implique que $Eq_r(\mathbb{F}(Eq_r(\rho))) = \mathbb{F}(Eq_r(\rho))$. Cette dernière propriété est celle représentée par le troisième diagramme.

Il est alors possible de prouver l'égalité suivante :

$$
[Z_r \circ Eq_r] \circ [\mathbb{F}] \circ [Eq_r] = [Z_r \circ \mathbb{F} \circ Eq_r] \circ [Z_r \circ Eq_r] \circ [Eq_r]
$$

est réalisée.

En effet:

$$
\begin{align*}
[Z_r \circ Eq_r] \circ [\mathbb{F}] \circ [Eq_r] &= Z_r \circ [Eq_r \circ \mathbb{F} \circ Eq_r] \\
[Z_r \circ Eq_r] \circ [\mathbb{F}] \circ [Eq_r] &= Z_r \circ [\mathbb{F} \circ Eq_r] \\
[Z_r \circ Eq_r] \circ [\mathbb{F}] \circ [Eq_r] &= [Z_r \circ \mathbb{F} \circ [Eq_r \circ Eq_r]] \\
[Z_r \circ Eq_r] \circ [\mathbb{F}] \circ [Eq_r] &= [Z_r \circ \mathbb{F} \circ [[Eq_r \circ Eq_r] \circ Eq_r]] \\
[Z_r \circ Eq_r] \circ [\mathbb{F}] \circ [Eq_r] &= [Z_r \circ \mathbb{F} \circ [[Eq_r \circ Z_r] \circ Eq_r] \circ Eq_r]] \\
[Z_r \circ Eq_r] \circ [\mathbb{F}] \circ [Eq_r] &= [Z_r \circ \mathbb{F} \circ Eq_r] \circ [Z_r \circ Eq_r] \circ Eq_r.
\end{align*}
$$

Ce calcul est résumé dans le diagramme commutatif suivant :

<figure><img src="image_130.png" /></figure>
Ainsi pour tout état $\rho \in V \to \mathbb{R}$ tel que $Eq_r(\rho) = \rho$, la propriété suivante :

$$[[Z_r \circ Eq_r] \circ [F]] (\rho) = [Z_r \circ F \circ Eq_r] \circ [Z_r \circ Eq_r](\rho)$$

est satisfaite.

Cette propriété est similaire à la caractérisation des réductions de modèles vues en section 4.3, avec la fonction $F$ pour définir la dynamique du système différentiel initial, $Z_r \circ Eq_r$ comme fonction d'abstraction et $Z_r \circ F \circ Eq_r$ comme contre-partie abstraite de la fonction $F$. Il y a toutefois deux différences. D'une part, cette propriété n'est valable que pour les états symétriques (qui sont leur propre image par la fonction $Eq_r$). Ce n'est pas un problème puisque lorsque l'état initial est symétrique, la trajectoire reste dans l'ensemble des états symétriques. D'autre part, il peut y avoir des variables dont la contribution est nulle dans la fonction $Z_r \circ Eq_r$, puisque seules les variables qui sont les représentantes de leurs classes d'équivalence ont une contribution non nulle. Ici encore, ce n'est pas un problème, car le système simplifié préserve tout de même les asymptotes verticales. En effet, si la valeur d'une variable diverge, il en est de même pour la valeur de sa représentante de sa classe d'équivalence qui elle, apparaît avec une contribution non nulle dans le système simplifié.

De ce fait, les trajectoires maximales du systèmes simplifiées sont bien l'image point par point par la fonction d'abstraction $Z_r \circ Eq_r$ des trajectoires du système initiale qui commence dans un état symétrique.

**Exemple 6.3.11** Dans le modèle introduit en section 6.1.1.1, la fonction $F$ est définie de la manière suivante :

$$F(\rho) = \begin{cases} A & \mapsto 2k_{xy}^d \rho(A.x - y.A) + 2k_{yy}^d 2\rho(A.y - y.A) + 2k_{xx}^d 2\rho(A.x - x.A) - (2k_{yy} + 2k_{xx} + 2k_{xy}) \rho(A)^2 \\ A.x - x.A & \mapsto 2k_{xx} \rho(A)^2 - k_{xx}^d 2\rho(A.x - x.A) \\ A.y - y.A & \mapsto 2k_{yy} \rho(A)^2 - k_{yy}^d 2\rho(A.y - y.A) \\ A.x - y.A & \mapsto 2k_{xy} \rho(A)^2 - k_{xy}^d 2\rho(A.x - y.A). \end{cases}$$

La composition à droite avec la fonction $Eq_r$ remplace la contribution des configurations d'espèces biochimiques qui ne sont pas les représentantes de leurs classes d'équivalence par leur représentante avec comme co-efficient le rapport entre les nombres d'apparitions sous un forme isomorphe de la représentante dans l'orbite et celui de la configuration d'espèces biochimiques en question. Cela élimine donc les occurrences des variables $A.y - y.A$ et $A.x - y.A$ dans la fonction $F$.

Ainsi:

$$[F \circ Eq_r](\rho) = \begin{cases} A & \mapsto 2k_{xy}^d 2\rho(A.x - x.A) + 2k_{yy}^d 2\rho(A.x - x.A) + 2k_{xx}^d 2\rho(A.x - x.A) \\ & \quad - (2k_{yy} + 2k_{xx} + 2k_{xy}) \rho(A)^2 \\ A.x - x.A & \mapsto 2k_{xx} \rho(A)^2 - k_{xx}^d 2\rho(A.x - x.A) \\ A.y - y.A & \mapsto 2k_{yy} \rho(A)^2 - k_{yy}^d 2\rho(A.x - x.A) \\ A.x - y.A & \mapsto 2k_{xy} \rho(A)^2 - k_{xy}^d 2\rho(A.x - x.A) \end{cases}$$

D'où :

$$F \circ Eq_r = \begin{cases} A & \mapsto 4(k_{xy}^d + k_{yy}^d + k_{xx}^d) \rho(A.x - x.A) - (2k_{yy} + 2k_{xx} + 2k_{xy}) \rho(A)^2 \\ A.x - x.A & \mapsto k_{xx} \rho(A)^2 - k_{xx}^d 2\rho(A.x - x.A) \\ A.y - y.A & \mapsto k_{yy} \rho(A)^2 - k_{yy}^d 2\rho(A.x - x.A) \\ A.x - y.A & \mapsto k_{xy} \rho(A)^2 - k_{xy}^d 2\rho(A.x - x.A). \end{cases}$$

Enfin, la composition à gauche avec la fonction $Z_r$ élimine les variables $A.y - y.A$ et $A.x - y.A$ qui ne sont pas les représentantes de leurs classes d'équivalence.

Ainsi:

$$[Z_r \circ F \circ Eq_r](\rho) = \begin{cases} A & \mapsto 4(k_{xy}^d + k_{yy}^d + k_{xx}^d) \cdot \rho(A.x - x.A) - (2k_{yy} + 2k_{xx} + 2k_{xy}) \rho(A)^2 \\ A.x - x.A & \mapsto k_{xx} \rho(A)^2 - k_{xx}^d 2\rho(A.x - x.A) \\ A.y - y.A & \mapsto 0 \\ A.x - y.A & \mapsto 0. \end{cases}$$

Ce qui correspond à l'équation différentielle pour le modèle simplifié suivante :

$$\left\{ \begin{array}{l} A_1 \mapsto 16K^d \rho(A.x - x.A) - 2K \rho(A_1)^2 \\ A.x - x.A \mapsto \frac{K}{4} \rho(A_1)^2 - 2K^d \rho(A.x - x.A), \end{array} \right.$$
$$ \text{avec } K = k_{xx} + k_{xy} + k_{yy} \text{ et } K^d = k_{xx}^d = k_{yy}^d = \frac{k_{xy}^d}{2}. $$

Ceci clôt la partie sur l'utilisation des symétries pour réduire la sémantique différentielle des modèles engendrés par des règles.

## 6.3.3 États discrets

Le but de cette partie est de dériver des propriétés similaires à celles données en Section 6.3.2, mais cette fois-ci pour la sémantique stochastique.

### 6.3.3.1 Bisimulation en avant

La propriété 6.3.1 implique que lorsque qu'un ensemble de règles est symétrique par rapport à un type d'échanges de sites, le système engendré par ces règles se comporte de la même manière quand un tel échange est effectué dans l'état du système. En effet, la probabilité d'aller dans une classe d'équivalence donnée est la même pour deux états symétriques.

**Exemple 6.3.12** Dans l'exemple jouet introduit en section 6.1.1.1, quitte à intervertir les sites x et y dans une ou plusieurs occurrences de la protéine A, les configurations des espèces biochimiques se répartissent en deux catégories selon qu'elles soient formées d'une ou de deux occurrences de la protéine A. Ces deux catégories sont dessinées en figure 6.29. De ce fait, les classes d'équivalence pour les échanges des sites x et y sont caractérisées par le nombre d'occurrences i de l'unique configuration du monomère de la protéine A et par la somme j des trois configurations du dimère de la protéine A.

Cette propriété se décline sur plusieurs niveaux d'abstraction.

1. **Distribution des traces.** La sémantique de traces qui opère sur des classes d'équivalence d'états est une approximation fidèle de la sémantique de traces initiale. En effet, deux états symétriques se comportent de manière identique vis à vis des classes d'équivalence. La probabilité d'un ensemble de traces dans la sémantique quotient est alors la somme des probabilités des ensembles de traces dont ils sont l'abstraction, l'abstraction d'un ensemble de traces étant obtenue en remplaçant chaque état et chaque pas de calcul par sa classe d'équivalence et en conservant les intervalles de temps pour le délai entre chaque pas de calcul. Il faut pour cela supposer que la distribution initiale des états dans la sémantique simplifiée soit égale à la distribution obtenue en sommant la probabilité de chaque état par classe d'équivalence dans la distribution initiale des états dans la sémantique initiale.

**Exemple 6.3.13** Ceci permet de justifier les remarques de la section 6.1.2. En effet, quite à oublier la différence entre les sites x et y dans les occurrences de la protéine A, il y a, dans le modèle de la section 6.1.1.1, uniquement deux classes d'équivalence de configurations d'espèces biochimiques, celles de l'unique configuration du monomère de la protéine A et celle qui regroupe les trois configurations du dimère de la protéine A. Ces deux classes d'équivalence peuvent se représenter comme en figure 6.8 page 101. Les règles d'interaction elles-même se représentent sous-forme de classes d'équivalence en oubliant la différence entre les sites x et y dans les occurrences de la protéine A dans leurs membres gauches et droits, ce qui donne bien les règles dessinées en figure 6.9 page 101. Les constantes de ces règles doivent assurer que la propensité d'une interaction dans un état du modèle simplifié soit la même que dans un état du modèle initial dans cette classe d'équivalence. Ainsi, la constante d'association du modèle simplifié doit être égale à la somme des trois constante d'association, alors que la règle de dissociation doit être égale à la valeur commune des deux constantes de dissociation pour les liaisons symétriques et de la moitié de la constante de dissociation pour la liaison asymétrique (le fait que le modèle soit symétrique impose que les constantes de dissociation pour les liaisons symétriques soient égales et que cette valeur commune soit la moitié de la constante de dissociation pour les liaisons asymétriques).

2. **Simulation stochastique.** Comme dans un modèle engendré par un ensemble symétrique de règles, deux états symétriques se comportent de la même manière vis à vis des classes d'équivalence de cette symétrie, il est possible d'échanger, entre chaque étape de calcul, les paires de sites en question dans une ou plusieurs occurrences de protéines. Ceci peut avoir une incidence sur les structures de données qui sont utilisées pour représenter l'état du système en réduisant le nombre de configurations différentes d'espèces biochimiques.
**Exemple 6.3.14** Ainsi, dans le cas d'étude présenté en section 6.1.1.1, il est possible, quitte à ajuster les constantes d'interaction, d'imposer que seuls les sites x des protéines A se lient. Ceci a pour conséquence, de réduire à la fois la nombre de configurations d'espèces biochimiques accessibles et le nombre des réactions, sans changer le comportement du modèle. Ainsi, il n'y a plus que deux configurations d'espèces biochimiques, au lieu de 4, et 2 réactions au lieu de 6.

3. **Équation maîtresse.** L'équation maîtresse est similaire à l'équation de la sémantique différentielle, si ce n'est qu'elle manipule des distributions de probabilité sur des états discrets, et non des quantités continues de configurations d'espèces biochimiques. Toutefois, une démarche analogue peut être utilisée pour réduire le nombre de variables dans celle-ci.

L'équation maîtresse de système est notée $\frac{dX(t)}{dt} = A(X(t))$. Il suffit donc de choisir un représentant $r(q)$ de la classe d'équivalence de chaque état $q$, pour définir deux projections linéaires $P_r$ et $Z_r$ :

$$P_r(\rho) = \begin{cases} Q \to \mathbb{R} \\ q \mapsto \sum \{\rho(q') | r(q') = q\} & \text{si } r(q) = q \\ q \mapsto 0 & \text{sinon,} \end{cases} \qquad Z_r(q) = \begin{cases} Q \to \mathbb{R} \\ q \mapsto \rho(q) & \text{si } r(q) = q \\ q \mapsto 0 & \text{sinon.} \end{cases}$$

Alors l'équation maîtresse réduite $\frac{dY(t)}{dt} = [P_r \circ A \circ Z_r](Y(t))$ définit, pour chaque état représentant de sa classe d'équivalence, l'évolution de la probabilité que le système soit dans un état symétrique à cet état au cours du temps.

**Exemple 6.3.15** Dans le cas d'étude présenté en section 6.1.1.1, les états potentiels du système sont notés $q_{i,j,k,l}$ où $i$ est le nombre d'occurrences de l'unique configuration du monomère de la protéine A, $j$ celui de la configuration du dimère de la protéine A dans laquelle les deux occurrences de la protéine A sont liées par leurs sites $x$, $k$ celui de la configuration du dimère de la protéine A dans laquelle les deux occurrences de la protéine A sont liées par leurs sites $y$ et $l$ celui de la configuration du dimère de la protéine A dans laquelle les deux occurrences de la protéine A sont liées par le site $x$ de l'une et le site $y$ de l'autre.

Les représentants des classes d'équivalence d'états sont choisis en assimilant toutes les occurrences de configurations du dimère à des occurrences de la configuration du dimère dans laquelle les deux occurrences de la protéine A sont liées par leurs sites $x$.

Les projections $P_r$ et $Z_r$ sont alors définies de la manière suivante :

$$P_r(P_t(q_{i,j,k,l})) = \begin{cases} \sum_{0 \le j' \le j} \sum_{0 \le k' \le j-j'} P_t(q_{i,j',k',j-j'-k'}) & \text{si } k=0 \text{ et } l=0 \\ 0 & \text{si } k \neq 0 \text{ ou } l \neq 0. \end{cases}$$

$$Z_r(P_t(q_{i,j,k,l})) = \begin{cases} P_t(q_{i,j,k,l}) & \text{si } k=0 \text{ et } l=0 \\ 0 & \text{si } k \neq 0 \text{ ou } l \neq 0. \end{cases}$$

L'équation $\frac{dY(t)}{dt} = [P_r \circ A \circ Z_r](Y(t))$ définit l'équation maîtresse réduite suivante :

$$\left\{
\begin{aligned}
\frac{dP_t(Q_{6,0,0,0})}{dt} &= 2K^d P_t(Q_{4,1,0,0}) - 30KP_t(Q_{6,0,0,0}) \\
\frac{dP_t(Q_{4,1,0,0})}{dt} &= 30KP_t(Q_{6,0,0,0}) + 4K^d P_t(Q_{2,2,0,0}) - (12K + 2K^d) P_t(Q_{4,1,0,0}) \\
\frac{dP_t(Q_{2,2,0,0})}{dt} &= 12KP_t(Q_{4,1,0,0}) + 6K^d P_t(Q_{0,3,0,0}) - (2K + 4K^d) P_t(Q_{2,2,0,0}) \\
\frac{dP_t(Q_{0,3,0,0})}{dt} &= 2KP_t(Q_{2,2,0,0}) - 6K^d P_t(Q_{0,3,0,0})
\end{aligned}
\right.$$

dans laquelle les états sont notés avec un Q majuscule pour les distinguer de ceux du système initial. Les solutions $X(t)$ et $Y(t)$ de l'équation maîtresse initiale et de l'équation maîtresse réduite sont liées par la relation, $Y(t) = P_r(X(t))$, à tout instant de l'exécution du système.
La relation de bisimulation avant suffit alors pour prouver les résultats constatés en figure 6.14(a) et en figure 6.14(e). Ainsi la distribution des états au cours du temps dans le modèle simplifié reste identique à celle obtenue dans le modèle initial en regroupant les états par classes d'équivalence. Il n'est pas nécessaire que la distribution initiale des états soit symétrique (voir en figure 6.14(e)).

### 6.3.3.2 Bisimulation en arrière

La propriété 6.3.2 assure que des invariants quantitatifs, prenant la forme de rapport de proportionnalité entre des probabilités des états symétriques, sont préservés lors de l'exécution stochastique d'un modèle symétrique.

Il faut dans un premier temps définir la notion de symétrie pour les distributions d'états. Une distribution d'états est une fonction de l'ensemble des états potentiels (qui peuvent être vus comme des graphes à sites qui ne peuvent être raffinés davantage sans ajouter de composante connexe ou encore comme des multi-ensembles de configurations d'espèces biochimiques) dans l'intervalle des nombres réels compris entre 0 et 1, dont la somme de toutes les images, pour tous les états potentiels du système est égal à 1. Une distribution d'états sera alors dîtes symétrique par rapport à un type d'échanges de sites, si et seulement si, pour toute paire d'états, telle que l'un des états puisse être obtenu à partir de l'autre en appliquant des échanges de ce type, les valeurs prises par les images des deux états par la distribution sont proportionnelles au nombre d'occurrence de ces états dans l'orbite de ces états pour ce type d'échanges de sites.

**Exemple 6.3.16** Dans l'exemple introduit dans la section 6.1.1.1, seuls les rapports entre les distributions des états qui comportent le même nombre d'occurrences de l'unique configuration du monomère de la protéine A et le même nombre global d'occurrences des trois configurations de son dimère, doivent être regardés. Le nombre d'occurrence d'un état dans l'orbite obtenue en échangeant les sites x et y dans des occurrences de la protéine A est inversement proportionnel à son nombre d'automorphisme. Soient deux états $q_{i,j,k,l}$ et $q_{i',j',k',l'}$, comportant respectivement i et i' occurrences de l'unique configuration du monomère de la protéine A, j et j' occurrences du dimère dans sa configuration dans laquelle la liaison porte sur les deux sites x des occurrences de la protéine A, k et k' occurrences du dimère dans sa configuration dans laquelle la liaison est entre les deux sites y des occurrences de la protéine A, et enfin l et l' occurrences du dimère de la protéine A dans sa configuration asymétrique. Ces états admettent respectivement $i! \cdot j! \cdot k! \cdot l! \cdot 2^j \cdot 2^k$ et $i'! \cdot j'! \cdot k'! \cdot l'! \cdot 2^{j'} \cdot 2^{k'}$ automorphismes. Dans les deux cas, les quatre premiers facteurs correspondent aux permutations entre les différentes occurrences d'une même configuration d'espèces biochimiques. Ensuite les deux suivants viennent du fait que chaque occurrence d'une configuration symétrique du dimère de la protéine A admet 2 automorphismes. En supposant que ces deux états sont symétriques pour l'échange des sites x et y dans des occurrences de la protéine A, il vient les deux contraintes supplémentaires $i = i'$ et $j + k + l = j' + k' + l'$. Ainsi $\frac{2^j \cdot 2^k}{2^{j'} \cdot 2^{k'}} = 2^{l'-l}$. Puis, le rapport entre les nombres d'automorphismes entre le premier et le second état est égal à $\frac{j! \cdot k! \cdot l! \cdot 2^{l'-l}}{j'! \cdot k'! \cdot l'!}$. Ainsi, une distribution d'états est symétrique, si pour chaque paire d'états $q_{i,j,k,l}$ et $q_{i',j',k',l'}$ tels que $i = i'$ et $j + k + l = j' + k' + l'$, le rapport entre la probabilité d'être dans l'état $q_{i,j,k,l}$ et celle d'être dans l'état $q_{i',j',k',l'}$ est égal à $\frac{j'! \cdot k'! \cdot l'! \cdot 2^{k'-l'}}{j! \cdot k! \cdot l!}$.

Les rapports de proportions observés en figure 6.15(a) correspondent bien à cette expression. Ainsi pour les états $q_{4,0,1,0}$ et $q_{4,1,0,0}$, ce rapport est égal à $\frac{1! \cdot 0! \cdot 0! \cdot 2^{0-0}}{0! \cdot 1! \cdot 0!}$, soit la valeur 1 ; pour les états $q_{4,0,0,1}$ et $q_{4,1,0,0}$, ce rapport est égal à $\frac{1! \cdot 0! \cdot 0! \cdot 2^{1-0}}{0! \cdot 0! \cdot 1!}$, soit la valeur 2 ; pour les états $q_{2,1,1,0}$ et $q_{2,0,0,2}$, ce rapport est égal à $\frac{0! \cdot 0! \cdot 2^{0-2}}{1! \cdot 1! \cdot 0!}$, soit la valeur 2.

Cette propriété se décline sur plusieurs niveaux d'abstraction.

1. **Distribution de traces.** Partant d'une distribution symétrique d'états pour un type d'échanges de sites, si l'ensemble des règles du modèle est lui-même symétrique par rapport à ce type d'échanges de sites, alors les pas de calculs préservent la symétrie de la distribution des états. Plus précisément, étant donnée une distribution symétrique d'états, la distribution d'états obtenue après un pas de calcul sachant que ce pas de calcul appartient à une classe d'équivalence de pas de calculs est elle-aussi symétrique (quite à sommer, c'est une conséquence directe de la propriété 6.3.2). En tenant compte du temps et en procédant par induction sur le nombre de pas de calculs, il est possible d'étendre ce résultat aux distributions obtenues après un ensemble de traces [117]. Soit $\beta$ la fonction d'abstraction définie sur les traces, qui consiste à remplacer chaque état par sa classe d'équivalence et chaque pas de calcul par la classe d'équivalence pour les échanges de sites étudiés tout en préservant les intervalles pour les délais entre les pas de calculs. L'image d'une trace du modèle initial par la fonction $\beta$ est alors appelée une trace abstraite. Si à la
<table><caption>Figure 6.30: Principales caractéristiques combinatoires des différents modèles testés en fonction du nombre de site *n* par occurrences de la protéine.</caption><thead><tr><th rowspan="2">model</th><th rowspan="2">sites</th><th rowspan="2">rules</th><th colspan="2">species</th><th colspan="2">reactions</th></tr><tr><th>original</th><th>reduced</th><th>original</th><th>reduced</th></tr></thead><tbody><tr><td>kinase/phosphatase</td><td>n</td><td>6n</td><td>2 + 4<sup>n</sup></td><td>2 + (n+3)/3</td><td>6n4<sup>n-1</sup></td><td>2n (n+2)/2</td></tr><tr><td>multiple phosphorylation</td><td>n</td><td>n2<sup>n</sup></td><td>2<sup>n</sup></td><td>n + 1</td><td>n2<sup>n</sup></td><td>2n</td></tr><tr><td>mult. phosphoryl. with counter</td><td>n</td><td>2n<sup>2</sup></td><td>2<sup>n</sup></td><td>n + 1</td><td>n2<sup>n</sup></td><td>2n</td></tr></tbody></table>

fois l'ensemble des règles et la distribution initiale des états sont symétriques pour le type d'échanges de sites en question, alors pour tout ensemble $X^\#$ de traces abstraites, la distribution conditionnelle des états obtenue après avoir appliqué une trace sachant que son abstraction est dans l'ensemble $X^\#$ est elle-même symétrique.

2. **Équation maîtresse.** Il est possible d'exploiter la propriété 6.3.2 directement sur l'équation maîtresse [22]. Ainsi si un ensemble de règles est symétrique par rapport à un type d'échanges de sites et si la distribution initiale des états est symétrique par rapport à ce même type d'échanges de sites, alors, par sommation, la distribution des états à l'instant *t* est elle aussi symétrique par rapport à ce type d'échanges de sites.

**Exemple 6.3.17** Dans l'exemple introduit dans la section 6.1.1.1, cette propriété justifie les observations faites en figure 6.15(a). Par ailleurs, en figure 6.15(e), est donné un exemple de simulation numérique dans lequel l'ensemble des règles est symétrique sans que la distribution initiale des états ne le soit. Dans ce cas, la distribution des états convergent vers une distribution symétrique. C'est en fait le cas, car tout état accessible du système appartient à une unique composante fortement connexe maximale, elle-même stable par symétrie. La distribution des états restreintes à chaque composante fortement connexe terminale converge vers une distribution ergodique.

Tout comme c'était le cas pour la sémantique différentielle, il est possible d'utiliser les symétries par rapport à un type d'échanges de sites pour éliminer des variables dans l'équation maîtresse. Il faut pour cela, choisir un représentant pour chaque classe d'équivalence d'états. Le représentant d'un état *q* est notée $r(q)$. Le nombre d'automorphismes de *q* est alors noté $aut(q)$.

Les deux fonctions de l'ensemble des distributions d'états vers lui-même sont définies ci-dessous :

$$ Eq_r(d) : \left\{ q \mapsto \frac{aut(r(q))}{aut(q)} \cdot d(r(q)) \right. \\ Z_r(d) : \left\{ \begin{array}{ll} \mathcal{V} & \rightarrow \mathbb{R} \\ q & \mapsto \rho(q) \quad \text{si } r(q) = q \\ q & \mapsto 0 \quad \text{sinon.} \end{array} \right. $$

L'élimination des états qui ne sont pas les représentants de leurs classes d'équivalence est alors formalisée par l'équation suivante :

$$ [[Z_r \circ Eq_r] \circ [\mathbb{F}]](d) = [[Z_r \circ \mathbb{F} \circ Eq_r] \circ [Z_r \circ Eq_r]](d) $$

qui est réalisée dès lors que l'ensemble des règles et la distribution d'états *d* sont tous deux symétriques par rapport aux échanges de sites en question.

## 6.4 Étude de performance

Cette approche est implantée dans un outils appelé KADE. Dans [29], est effectuée une étude de performance de cet outils, à la fois en terme de capacité de réduction et en terme de temps de calcul, ainsi qu'une comparaison avec d'autres outils existants pour réduire les sémantiques différentielles et stochastiques des réseaux réactionnels. Cette étude de performance mériterait d'être faite à nouveau avec les versions récentes des outils cités. Par ailleurs, il serait bien de comparer avec l'outils Jupiter [33] qui opère directement sur les systèmes d'équations différentielles.

En particulier, trois modèles paramétriques ont été considérés.
<figure><img src="image_131.png" /><figcaption>(a) Modèle avec kinase et phosphatase.</figcaption></figure>

<figure><img src="image_132.png" /><figcaption>(c) Modèle de phosphorylations multiples implanté par un compteur.</figcaption></figure>

<figure><img src="image_133.png" /><figcaption>(b) Modèle de phosphorylations multiples.</figcaption></figure>

<figure><img src="image_134.png" /><figcaption>(d) Légende.</figcaption></figure>

Figure 6.31: Comparaison entre les performances en temps de calcul des outils KADE, BNGL, et ERODE, sur un MacBookPro avec un puce Intel Core i7 cadencée à 2,8 GHz CPU et une mémoire DDR de 16 Go 1600 MHz. Les exécutions sont interrompues lorsque leurs temps d'exécution dépasse 10 minutes. Ces tests ont été effectués en 2017 (il faudrait les mettre à jour). **Génération du réseau réactionnel non-réduit** : sont donnés le temps CPU pour la génération du réseau non réduit avec les outils KADE et BNGL. **Inférence des symétries** : est tracé le temp total pour calculer les paires de sites équivalents avec KADE. **Réduction de modèle** : sont reportés les temps de calculs pour obtenir le réseau réactionnel réduit avec KADE, BNGL, et ERODE. Pour KADE le point d'entrée est l'ensemble des règles d'interaction des modèles, alors que pour les deux autres c'est le réseau réactionnel non réduit. **Réduction supplémentaire** : est donné le temps CPU pour l'exécution d'ERODE sur les réseaux réactionnels réduits par KADE.

* La première famille implique une kinase, une phosphatase et une protéine cible. La protéine cible dispose de *n* sites (*n* étant un paramètre entier), pouvant être phosphorylés ou non, et liés ou non à la kinase ou à la phosphatase. Une occurrence de la kinase peut se lier ou se séparer de chaque site d'une occurrence de la protéine cible dans une configuration où ce site est non phosphorylé et libre. Dans ce cas, l'occurrence de la kinase peut également phosphoryler l'occurrence de ce site tout en se dissociant de celle-ci. Réciproquement, une occurrence de la phosphatase peut se lier et de séparer de chaque site d'une occurrence de la protéine cible dans une configuration où ce site est phosphorylé et libre. Dans ce cas, l'occurrence de la kinase peut également déphosphoryler l'occurrence de ce site tout en se dissociant de celle-ci.

* La seconde famille est inspirée du comportement de la protéine *Kai*. Cette protéine joue un rôle crucial dans la contrôle des oscillations du cycle circadien. Elle implique une protéine avec *n* sites de phosphorylation. La kinase et la phosphatase ne sont pas décrites explicitement. Les taux de phosphorylation et de déphosphorylation de chaque occurrence de chaque site est supposé dépendre du nombre de sites déjà phosphorylé dans l'occurrence de la protéine correspondante.

* La troisième famille représente le même système que la seconde famille, mais en utilisant une astuce suggérée par Pierre Boutillier pour limiter le nombre de règles à écrire pour décrire le comportement des occurrences de configurations de la protéine. Cet astuce consiste à ajouter un site fictif à chaque protéine qui sera lié à une chaîne d'occurrences de protéines fictives, en maintenant l'invariant que la longueur de la chaîne des occurrences de la protéine fictive est toujours égale au nombre de sites phosphorylés dans la
configuration de la protéine en question. Ceci permet de connaître le nombre de sites phosphorylés dans une configuration de la protéine, sans avoir à énumérer les différentes possibilités pour le sous-ensemble des sites phosphorylés. Ce mécanisme est d'ailleurs à la base de l'implantation des protéines à compteur dans Kappa [16]. Il reprends des comportements présent dans la nature, notamment ceux impliqués dans le processus d'ubiquitination.

D'autres examples, notamment la plupart de ceux de la base de tests du langage BNGL sont donnée en information complémentaire [28].

Pour chaque jeu de paramètres des modèles, sont donnés, en figure 6.30, les nombres de règles, de configurations d'espèces biochimiques et de réactions, ainsi que le nombre de configurations d'espèces biochimiques et le nombre de réactions dans la modèle réduit correspondant. Les tests sont fait en faisant varier le paramètre *n* entre 1 et 10. Les performances des outils sont tracées en figure 6.31. En particulier sont comparés les temps de génération du réseau réactionnel réduit obtenu avec KADE et avec BNGL. Il est important de remarquer que dans l'approche utilisant BNGL, les symétries entre les sites doivent être spécifier par l'utilisateur, alors qu'elles sont inférées automatiquement par KADE. Les réseaux réduits obtenus sont les mêmes pour tous les modèles de cette batterie de tests. Cependant, le temps de génération avec l'outils KADE est bien meilleur.

Enfin, les performances de KADE ont été comparée avec celle d'ERODE. ERODE adopte une approche al-gébrique pour inférer des bisimulation, en-avant ou en arrière, dans des réseaux réactionnels. Ont été considérées à la fois la version rapide [35] et celle complète [34] (qui calcule les meilleurs bisimulations). L'outils ERODE a été testé à la fois sur les réseaux réactionnels initiaux et ceux réduit. Dans notre batterie de test (qui inclue ceux de la plate-forme BNGL), aucune nouvelle réduction n'a été trouvée, même avec la version complète. Ceci montre la prépondérance des symétries dans les tests réalisés. L'approche utilisant KADE est plus rapide que la version rapide de l'outils ERODE. Cela vient du fait que KADE opère directement sur la structure des règles, et ne nécessite pas de considérer l'ensemble des réactions. Par ailleurs, l'utilisation d'ERODE impose d'avoir une description extensionnelle du réseau réactionnel ou de sa sémantique différentielle, ce qui est prohibitif pour les modèles de grandes ou moyennes tailles.

## 6.5 Pour aller plus loin

Dans ce chapitre a été esquissé une méthode pour utiliser des symétries entre paires de sites d'interaction pour réduire la dimension de la sémantique différentielle et la taille de la sémantique stochastique des modèles de réécriture de graphes à sites. Cette approche a été implantée dans l'outils KADE.

Cette méthode a été obtenue en étendant la définition des échanges de sites dans un motif, d'une part, aux plongements, aux règles et aux raffinements de règles, d'autres parts aux états de la sémantique différentielle et aux états de la sémantique stochastique. Il en résulte une définition des états symétriques (dans la sémantique différentielle et dans la sémantiques stochastique) et des ensembles symétriques de règles. Les symétries entre paires de sites induisent une bisimulation avant-arrière. Ainsi dans un modèle issu d'un ensemble de règle symétrique pour les échanges de sites dans les occurrences d'une protéine, l'exécution du modèle dans la sémantique différentielle et celle dans la sémantique stochastique peuvent être vues à échanges de ces sites près dans les configurations d'espèces biochimiques. De plus, lorsque l'état initial — dans la sémantique différentielle — ou la distribution initiale des états — dans la sémantique stochastique — est symétrique, alors cela reste vrai au cours de l'exécution du système.

**Combinaion de réduction de modèles.** Comme montré dans [27], les réductions de modèles décrites dans le chapitre 4 et dans le chapitre 5 peuvent se combiner avec les réductions basées sur les échanges de sites symétriques. Le but est d'alors d'oublier au moins autant d'information que dans chacune des deux réductions, et parmi toutes les réductions qui oublient au moins autant d'information, choisir celle qui en oublie le moins. Pour la sémantique différentielle, la principale difficulté vient du fait que les réductions de modèles du chapitre 4 ne sont pas engendrées par des relations d'équivalence sur l'ensemble des configurations des espèces biochimiques. En effet, une configuration d'espèces biochimiques donnée peut apparaître dans plusieurs combinaisons linéaires. Le diagramme dessiné en figure 6.32 propose une manière de composer une réduction classique avec une réduction basée sur une relation d'équivalence sur les configurations des espèces biochimiques. Dans ce dernier, outre les diagrammes commutatifs intermédiaires qui correspondent à la réduction de modèle classique et à la bisimulation en avant induite par la relation d'équivalence *r*, se trouvent deux nouveaux diagrammes intermédiaires. Ceux-ci permettent d'étendre la notion de symétries sur les variables du modèle réduit du chapitre 4. Pour cela, il
<figure><img src="image_135.png" /><figcaption>Figure 6.32: Diagramme commutatif pour composer une réduction de modèle classique et une réduction basée sur des échanges de paires de sites symétriques. Dans celui-ci, $\mathbb{F}$ désigne la dynamique du système dans la sémantique concrète, $\mathbb{F}^\sharp$ sa contre-partie abstraite dans le modèle obtenu par la réduction classique et $\psi$ la fonction d'abstraction correspondante. Le fonction $r$ spécifie un choix de représentantes pour les classes d'équivalence des configurations des espèces biochimiques et la fonction $r^\sharp$ un choix de représentantes pour les classes d'équivalence des variables du modèle obtenu par la réduction classique. $P_r$ et $P_{r^\sharp}$ sont les fonctions de projection qui regroupent la quantité des éléments sur leurs classes d'équivalence, alors que la fonction $Z_{r^\sharp}$ annule la quantité des variables du modèle réduit qui ne sont pas les représentantes de leurs classes d'équivalence. Les deux fonctions pour choisir les représentantes doivent vérifier la contrainte $P_{r^\sharp} \circ \psi = \psi \circ P_r$. Sous cette hypothèse, le modèle initial peut être réduit par la fonction d'abstraction $P_{r^\sharp} \circ \psi$. La contre-partie abstraite de la dynamique du système est alors donnée par la fonction $P_{r^\sharp} \circ \mathbb{F}^\sharp \circ Z_{r^\sharp}$.</figcaption></figure>

faut choisir une fonction de représentantes $r^\sharp$ pour les classes d'équivalence modulo les symétries des variables du modèle obtenu par la réduction classique. Le premier nouveau diagramme exploite le fait que la fonction d'oublie $Z_{r^\sharp}$ qui annule la quantité des variables du modèle obtenu par la réduction classique qui ne sont pas les représentantes de leurs classes d'équivalence, et la fonction d'abstraction $P_{r^\sharp}$ qui regroupe ces quantités sur les représentantes des classes d'équivalence, sont deux projection linéaires définies sur le même espace et partageant la même image. De ce fait, $P_{r^\sharp} = Z_{r^\sharp} \circ P_{r^\sharp}$. Le choix des représentantes pour les configurations des espèces biochimiques, celui des représentantes pour les variables du modèle réduit et la fonction d'abstraction entre le modèle initial et le modèle réduit (avant la prise en compte des symétries) doivent respecter le second nouveau diagramme commutatif :

<figure><img src="image_136.png" /></figure>

qui signifie qu'étant donné un état concret, abstraire cet état puis regrouper les quantités par classes d'équivalence des variables du modèle réduit ou regrouper les quantités par classes d'équivalence de configurations d'espèces biochimiques, puis abstraire le résultat, donnent la même fonction. Cette condition signifie qu'aucune corrélation entre les états de deux sites symétriques n'est abstrait par la réduction de modèles, ce qui revient à dire tout motif d'intérêt du modèle obtenu par la réduction classique qui contient un site, contient tous les sites qui lui sont symétriques. Sous cette hypothèse, la combinaison des deux réductions de modèles donne lieu à une nouvelle. La fonction d'abstraction applique la fonction d'abstraction de la réduction de modèle du chapitre 4, puis regroupe les quantités de motifs d'intérêt sur les représentants de leurs classes d'équivalence. La contre-partie abstraite de la fonction $\mathbb{F}$ s'obtient en éliminant la contribution des motifs d'intérêt qui ne sont pas les représentants de leurs classes d'équivalence, puis en applicant la contre-partie abstraite de la réduction de modèle du chapitre 4, puis en regroupant les quantités de motifs d'intérêt sur les représentants de leurs classes d'équivalence.

Les combinaisons de réductions de modèles dans le cadre stochastique prennent la forme de compositions et de sommes amalgamées, dans la catégorie des relations d'équivalence. De ce fait, le diagramme donné en figure 6.33 donne une hiérarchie des sémantiques de traces pour les modèles de réécriture de graphes à sites. De gauche à droite, l'abstraction oublie graduellement de l'information sur les occurrences de protéines. La sémantique individuelle définit une distribution de traces sur des états dans lesquels les occurrences de protéines portent un identifiant unique qui les suit tout le long des exécutions potentielles du système. Les sémantiques de population, elles, décrivent l'état du système à permutation des identifiants près, c'est à dire à isomorphisme près. Le terme population vient du fait qu'une classe d'équivalence d'un état pour les isomorphismes contient
<figure><img src="image_137.png" /><figcaption>Figure 6.33: Hiérarchie de sémantiques de traces dans le cadre stochastique. Les sémantiques individuelles décrivent des distributions de traces portant sur des occurrences de protéines annotées par un identifiant unique qui les suit le long de l'exécution du modèle. Les sémantiques de population sont obtenues en raisonnant sur les graphes à sites à isomorphisme près, ce qui revient à oublier ces identifiants. Enfin, les sémantiques de motifs indépendants sont obtenus en découpant les occurrences de configurations de protéines selon la méthode présentée en chapitre 5. Chaque sémantique existe sous deux formes selon que les éventuelles symétries entre les paires de sites aient été utilisées pour réduire le modèle ou non. Chaque flèche représente un quotient par une relation d'équivalence sur les ensemble des états de la sémantique à la source de cette flèche. Deux relations se composent séquentiellement, lorsque que la seconde est plus grossière que la première. Deux relations peuvent aussi se combiner en utilisant une somme amalgamée. La relation obtenue est alors la plus petite relation qui identifie au moins toute paire d'éléments identifiées dans au moins l'une ou l'autre des deux relations initiales. Ce diagramme est valide pour les bisimulations avant-arrière, pour les bisimulation en avant et pour les bisimulations en arrière.</figcaption></figure>

peut être décrite comme un multi-ensemble d'occurrences de configurations d'espèces biochimiques. Il est alors possible d'aller encore plus loin en découpant les occurrences de protéines sur les parties qui se comportent de manière indépendante. Les flèches verticales correspondent, elles, au quotient des états par les échanges de sites symétriques. La somme amalgamée de deux relations d'équivalence se définit comme la relation d'équivalence la plus grossière qui est au moins aussi fine que les deux relations données en argument. Elle se calcule en effectuant la clôture transitive du graphe formé par l'union des deux relations. Cette opération est définie modulo le choix des noms qui sont associés aux classes d'équivalence dans la somme amalgamée des deux relations. Grâce à cela, il n'y a pas d'ordre à fixer entre les deux relations. Cette hiérarchie est valable pour les bisimulations avant-arrière, pour les bisimulations en avant et pour les bisimulations en arrière. Dans le dernier cas, il est intéressant de remarquer que toutes les flèches d'abstraction partant d'une sémantique individuelle correspondent à des bisimulations uniformes (dans lesquelles deux objets en relation ont le même poids). Il est possible de retrouver les poids qui interviennent dans le quotient des sémantiques de populations en définissant ces quotients comme la restriction de deux quotients de la sémantique individuelle. Le poids de chaque élément correspond alors au rapport entre le cardinal de ses classes d'équivalence. Ceci donne une autre manière de retrouver les rapports de proportionnalités en inverse du nombre d'automorphismes.

**D'autres groupes de symétries.** Dans [73] est présenté un cadre générique pour suivre les sémantiques des modèles de règles de réécriture modulo des groupes de symétries. Les échanges de sites qui ont été étudiés dans ce chapitre en sont un cas particulier. Dans ce cadre plus général, il est possible de définir des sous-groupes de symétries à partir de groupes existants. Par exemple, il est possible de considérer les configurations à permutation circulaire près de l'état d'un sous-ensemble de ses sites. Il est aussi possible de contraindre les échanges de sites qui sont appliquées à deux occurrences de configurations d'une protéine dans une même composante connexe. La question essentielle est de comprendre si de tels sous-groupes de symétries engendrent également des bisimulations en avant et des bisimulations en arrière sur les ensembles symétriques de règles.
<figure><img src="image_138.png" /><figcaption>Figure 6.34: Orbites des configurations du dimère de la protéine A dans lesquelles exactement un site par occurrence est phosphorylée. En figure 6.34(a), pour les échanges hétérogènes de sites, toutes les configurations appartiennent à la même orbite. En figure 6.34(b), les échanges homogènes de sites séparent les dimères dont les deux occurrences de la protéine A sont dans la même configuration, des autres.</figcaption></figure>

**Exemple 6.5.1** Dans cet exemple est considéré deux groupes de symétries qui permettent d'échanger deux sites dans les occurrences d'une protéine. Dans le premier, les échanges peuvent être choisis indépendamment pour chaque occurrence de la protéine (c'est la notion de symétrie qui a été étudiée dans ce chapitre). Ces échanges de sites seront dits hétérogènes. Dans le second, le même échange de sites doit être appliqué à toutes les occurrences de la protéine dès lors qu'elles sont dans la même composante connexe. Ces échanges de sites seront dit homogènes.

Soit A une protéine comportant trois sites : deux sites de phosphorylation x et y et un site de liaison z. Les sites z de deux occurrences de la protéine A peuvent se lier entre eux. Une attention particulière est portée sur l'ensemble des configurations du dimère de la protéine dans lesquelles exactement un site par occurrence de la protéine, est phosphorylé. En figure 6.34(a), cet ensemble forme une orbite pour les échanges hétérogènes des sites x et y dans les occurrences de la protéine A (cette orbite est constituée de 4 éléments dont deux sont isomorphes). En figure 6.34(b), cet ensemble forme deux orbites disjointes pour les échanges homogènes de sites, selon que les sites phosphorylés dans les deux occurrences de la protéine soient les même ou non.

C'est un point essentiel pour étendre l'utilisation du langage Kappa à d'autres champs d'applications, comme la chemioinformatique. Dans ce domaine, les nœuds des graphes à sites représentent des atomes et les sites d'interaction des électrons susceptibles d'être partagés ou liés deux à deux. Deux différences principales entre les modèles en biochimie et ceux en chemioinformatique sont les suivantes. En chemioinformatique, les atomes ont peu d'électrons disponibles. Par contre, des symétries complexes sont à prendre en compte. Ainsi en stéréochimie, seules les permutations de sites de signe paire (celles qui sont engendrées par un nombre paire d'échanges de sites deux à deux) peuvent être appliquées aux occurrences des atomes. Par ailleurs, il est impossible de dissocier deux électrons qui participent à une double liaison. Enfin, lorsque deux électrons participants à une double liaison sont échangés l'un à l'autre dans l'occurrence d'un atome, il doit en être de même pour les deux électrons de l'autre côté de la liaison. Toutes ces contraintes se traduisent sous la forme d'un sous-groupe de symétries. L'étude et la prise en compte de ce groupe de symétries permettront de compléter les outils offert pour la chemioinformatique par le langage mod [4] avec des analyses statiques, des analyses causales et des réductions de modèles.

En toute généralité, le cadre algébrique considère des groupes de transformations sur les graphes à sites telles que les transformations qui s'appliquent aux motifs cibles des plongements puissent être restreintes à leurs motifs sources. Par contre, contrairement aux échanges de sites qui ont été proposés dans ce chapitre, il n'est pas toujours possible d'étendre une transformation qui s'applique au motif source d'un plongement à son motif cible. Cette propriété ne passe pas au sous-groupe.

**Exemple 6.5.2** Pour poursuivre l'exemple précédent, est donné en figure 6.35 un exemple d'échange de sites
<figure><img src="image_139.png" /><figcaption>(a) Lorsque les échanges de sites sont indépendants, il est possible d'étendre l'échange des états des sites x et y dans la première occurrence de la protéine A dans le motif source du plongement au motif cible.</figcaption></figure>

<caption>(b) C'est impossible lorsque le même échange doit être effectué sur toutes les occurrences d'une même protéine au sein des composantes connexes.</caption>

Figure 6.35: Un exemple de plongement, pour lequel un échange de sites opérant sur le motif source peut s'étendre au motif cible uniquement pour le cas des échanges de sites indépendants. Le motif source est constitué de deux occurrences de la protéine A, toutes deux dans une configuration dans laquelle le site x est phosphorylé, mais pas le site y. L'état du site z n'est pas précisé. Le plongement consiste à ajouter le site z dans les deux occurrences de la protéine et à préciser que ces sites sont liées. Dans le motif cible, les deux occurrences de la protéine A sont donc dans la même composante connexe. L'échange de sites en question consiste à intervertir les états des sites x et y dans la première occurrence de la protéine A, mais pas dans la deuxième. La question est de savoir si un tel échange de sites peut s'étendre au motif cible du plongement. Avec le groupe des échanges hétérogènes de sites (voir en figure 6.35(a)), cela ne pose pas de problèmes, puisque les choix d'échanger les états des sites x et y dans chaque occurrence de la protéine A sont indépendants. En revanche, avec le sous-groupe des échanges homogènes de sites (voir en figure 6.35(b)), ce n'est pas possible. Comme les deux occurrences de la protéine A sont dans la même composante connexe dans le motif cible, il faut soit ne procéder à aucun échange, soit échanger les états des sites x et y dans les deux occurrences de la protéine A simultanément.

qui s'applique au motif source d'un plongement, qui peut s'étendre au motif cible dans le groupe des échanges hétérogènes de sites, mais pas dans celui des échanges homogènes de sites.

Le motif source est constitué de deux occurrences de la protéine A, toutes deux dans une configuration dans laquelle le site x est phosphorylé, mais pas le site y. Les états de leurs sites z respectifs ne sont pas décrits. Le plongement ajoute ces deux sites tout en spécifiant qu'ils sont liés. L'exemple consiste à essayer d'étendre l'échange entre les sites x et y dans la première occurrence du motif source au motif cible du plongement. Ceci n'est possible que pour le groupe des échanges hétérogènes de sites. En effet, la difficulté vient du fait que les deux occurrences de la protéine A appartiennent à deux composantes connexes différentes dans le motif source du plongement, mais à la même composante connexe dans le motif cible. Avec le groupe des échanges de sites hétérogènes, ce n'est pas un soucis, puisque les choix d'échanger les états des sites x et y dans chacune des occurrences de la protéine A peuvent être faits de manière indépendante même dans le motif cible. Par contre, avec le groupe des échanges homogènes de sites, c'est tout simplement impossible puisqu'échanger les états des sites x et y dans la première occurrence de la protéine A sans échanger ceux-ci dans la seconde, n'est pas autorisé.

En conséquence, la propriété fondamentale (voir section 6.3.1.4, page 123) n'est pas réalisée pour tous les sous-groupes de symétries : les transformations ne peuvent pas toujours être propagées de gauche à droite ou de droite à gauche le long des pas de calculs. En effet, étant donnée une transformation qui s'applique au membre gauche d'un pas de calcul, celle-ci peut être restreinte à la partie commune entre le membre gauche et le membre droit du pas de calcul. Il s'agit juste de la restriction d'une transformation qui s'applique au motif cible d'un plongement à son motif source. Par contre, il n'est pas toujours possible d'étendre la transformation obtenue au membre droit du pas de calcul. Ainsi, même dans le cas d'un ensemble symétrique de règles pour un sous-groupe de transformations, les symétries correspondantes ne définissent pas toujours une bisimulation en avant. De la même manière, étant donnée une transformation qui s'applique au membre droit d'un pas de calcul, celle-ci peut être restreinte à la partie commune entre le membre gauche et le membre droit du pas de calcul, mais rien ne garanti en général qu'il soit possible d'étendre la transformation obtenue au membre gauche du pas de calcul. Ainsi, même dans le cas d'un ensemble symétrique de règles pour un sous-groupe de transformations, les symétries correspondantes ne définissent pas toujours une bisimulation en arrière.

Une question essentielle en suspens est d'identifier des sous-groupes d'échanges de sites intéressants, et pour
<figure><img src="image_140.png" /><figcaption>Figure 6.36: Un ensemble de règles dans lequel deux sites d'une protéine ont le même comportement dans les configurations de celle-ci dans lesquelles un troisième site est phophosrylé.</figcaption></figure>

chacun de caractériser les ensembles symétriques de règles pour lesquels ils engendrent des bisimulations en avant, des bisimulations en arrière ou des bisimulations avant-arrière.

**Symétries contextuelles.** Un autre exemple de sous-groupes de transformations important est celui des symétries contextuelles entre paires de sites. Elles apparaissent lorsque plusieurs sites ont des comportements identiques mais uniquement dans certaines configurations de leur protéine. Il est alors possible de spécifier un groupe de transformations pour échanger l'états de ces sites uniquement dans les configurations en question. Il reste à savoir si ce groupe induit une bisimulation avant-arrière, juste une bisimulation avant, juste une bisimulation arrière ou aucune bisimulation.

**Exemple 6.5.3** Le modèle donné en figure 6.36 comporte des symétries contextuelles. Il est constitué d'une seule protéine A qui comporte trois sites de phosphorylation. Chacun de ses trois sites peut se phosphoryler ou se déphosphoryler dans les occurrences des configurations de la protéine A sous certaines conditions sur l'état des autres sites. Les deux règles de la première ligne spécifient que le site h d'une occurrence de la protéine A peut se phosphoryler si elle est dans une configuration dans laquelle les deux sites g et d le sont et se déphosphoryler uniquement lorsqu'elle est dans sa configuration dans laquelle les deux sites g et d sont eux même non phosphorylés. En deuxième ligne, le site g d'une occurrence de la protéine A peut se phosphoryler si elle est dans une configuration dans laquelle les deux sites h et d sont non phosphorylés ou dans une configuration dans laquelle au moins le site h est phosphorylé. Ces deux conditions sont incompatibles, ce qui assure que deux règles ne peuvent jamais s'appliquer toutes les deux à la même occurrence d'une configuration de la protéine A. En troisième ligne, la déphosphorylation du site g est réalisée exactement sous les mêmes conditions que sa phosphorylation. En quatrième ligne, le site d d'une occurrence de la protéine A peut se phosphoryler si elle est dans une configuration dans laquelle soit le site h est non phosphorylé et le site g est phosphorylé, soit le site h est phosphorylé peu importe l'état du site g. En cinquième ligne, le site d d'une occurrence de la protéine A peut se faire déphosphoryler sans conditions. Les constantes d'interaction de chaque règle sont toutes fixées à 1.

Pour mieux appréhender le comportement des occurrences de la protéine A, un système de transitions est donné en figure 6.37 pour décrire leurs exécutions potentielles. Il s'agit d'une trace locale (voir page 40). Il apparaît que les occurrences des protéines fonctionnent selon deux modes selon que le site h soit phosphorylé ou non. Dans la partie basse du système de transitions, lorsque le site h n'est pas phosphorylé, les phosphorylations des sites g et d se font de manière séquentielle, tout comme leurs déphosphorylations mais dans l'ordre inverse. À l'opposé, dans la partie haute de ce système, lorsque le site h est phosphorylé, les phosphorylations des sites g et d sont indépendantes, de même que leurs déphosphorylations. Ainsi les sites g et d ont le même comportement uniquement dans les occurrences de configurations de la protéine A dans laquelle le site h est phosphorylé.

Dans ce modèle, il est possible de regrouper les occurrences de protéine dans les configurations dans lesquelles le site h est phosphorylé, ainsi qu'exactement un des deux autres sites. Ainsi les deux configurations suivantes :

<figure><img src="image_141.png" /></figure>
<figure><img src="image_142.png" /></figure>

Figure 6.37: Le système de transitions qui décrit les évolutions potentielles de la configuration d'une protéine. Dans la partie basse, lorsque le site *h* n'est pas phosphorylé, le site *g* est toujours phosphorylé avant le site *d*. Ils ne sont donc pas symétriques dans ce contexte. Dans la partie haute, lorsque le site *h* est phosphorylé, les sites *g* et *d* se phosphorylent et se déphosphorylent selon les même propensité. Ils sont indiscernables dans ce contexte. La question est de savoir si cette information permet de définir une relation de bisimulation avant-arrière, juste avant, juste arrière, ou ni l'une ni l'autre, en assimilant la configuration de la protéine dans laquelle les sites *h* et *g* uniquement sont phosphorylées et celle dans laquelle uniquement les sites *h* et *d* sont phosphorylées. Comme les règles ont toutes 1 comme constante cynétique et qu'il n'y a pas de conflits entre elles (une transition est toujours le raffinement d'au plus une règle), chaque transition est de propensité 1.

sont symétriques et forment une classe d'équivalence, mais pas les deux configurations suivantes :

<figure><img src="image_143.png" /></figure>

qui forment deux classes d'équivalence distinctes.

Cette relation d'équivalence engendre une bisimulation avant-arrière. Ceci tient essentiellement du fait que tout changement de l'état du site *h* dans une occurrence de la protéine *A* ne peut se faire que dans une configuration dans laquelle l'état des deux autres sites est le même.

Pour comprendre si des symétries contextuelles engendrent une bisimulation en avant, il faut examiner sous quelles conditions il est possible de casser le contexte dans lequel cette symétrie opère. Il faut, en effet, pouvoir déplacer les symétries de l'état juste avant l'application d'une règle d'interaction à l'état obtenu juste après avoir appliqué celle-ci. Comme les configurations de protéines qui ne satisfont les conditions contextuelles sont réduites à des singletons, cela revient à dire que l'application d'une règle d'interaction à deux configurations symétriques de protéines doit produire la même configuration de protéines, dès lors que cette règle brise la condition contextuelle.

**Exemple 6.5.4** Dans l'exemple des figures 6.36 et 6.37, s'il était possible de déphosphoryler le site *h* des occurrences de la protéine *A* sans condition, alors les deux configurations suivantes:

<figure><img src="image_144.png" /></figure>
n'auraient plus le même comportement vis à vis des classes d'équivalence de la relation (car la déphosphorylation du site h dans ces configurations donneraient deux configurations qui ne seraient pas dans la même classe d'équivalence). Celle-ci ne pourrait alors pas engendrer une bisimulation en avant.

Réciproquement, pour comprendre si des symétries contextuelles engendrent une bisimulation en arrière, il faut examiner sous quelles conditions il est possible de former le contexte dans lequel cette symétrie opère. Il faut, en effet, pouvoir déplacer les symétries de l'état juste après l'application d'une règle d'interaction à l'état juste avant d'avoir appliqué celle-ci. Comme les configurations de protéines qui ne satisfont les conditions contextuelles sont réduites à des singletons, cela revient à dire que l'application d'une règle d'interaction à deux configurations distinctes de protéines doit produire deux configurations symétriques de la protéines, dès lors que cette règle instaure la condition contextuelle.

**Exemple 6.5.5** Dans l'exemple des figures 6.36 et 6.37, les états des sites d et g dans les occurrences des configurations de la protéine A dans lesquelles le site h est non phosphorylé, ne sont pas indépendants. Si le site h pouvait se faire déphosphoryler sans condition, cette correlation induirait une corrélation entre les états des sites d et g dans les occurrences des configurations de la protéine A dans lesquelles le site h est phosphorylé. Il n'y aurait alors pas de bisimulation en arrière.

Étudier, inférer et exploiter les symétries contextuelles est une voie pleine de promesses. Il est possible de spécifier quels contextes distingués en dépliant la carte de contacts, comme cela l'a déjà été fait dans la section 4.6 pour la réduction de la sémantique différentielle. Cela reste néanmoins un paramètre que le concepteur du modèle doit fournir à la main. Il est sans doute possible de rendre cette paramétrisation automatique en construisant le dépliage de la carte de contacts à partir des motifs qui apparaissent dans les règles d'interaction. Des heuristiques sont à trouver pour trouver un compromis intéressant entre précision de l'analyse (et donc capacité de réduction) et temps de calcul de celle-ci.
# Chapitre 7

## Conclusion

Après un bref passage en revue de l'écosystème Kappa et de l'utilisation de l'interprétation abstraite pour extraire les propriétés des réseaux d'interactions biomoléculaires, le langage Kappa a été présenté plus en détail, ainsi qu'une analyse statique pour détecter parmi un ensemble de motifs d'intérêt lesquels peuvent potentiellement apparaître dans des configurations d'espèces biochimiques dans une trace d'exécution d'un modèle et des méthodes de réduction de modèles pour réduire la combinatoire de ces modèles.

Du point de vue de l'utilisateur, l'analyse statique permet de trouver – ou de retrouver – des propriétés structurelles sur les différentes configurations des occurrences des protéines au sein des complexes biochimiques : elle détecte quelles sont les relations entre l'état des sites des occurrences d'une protéine (Est-ce que tel site peut être lié sans que tel autre ne le soit ? Est-ce que ce site peut être lié sans être phosphorylé ?) ; elle permet de vérifier si deux occurrences de protéines liées entre-elles sont, oui ou non, nécessairement localisées au même endroit au sein d'une hiérarchie statique de compartiments ; elle analyse si une occurrence de protéines peut être doublement liée à une autre ou si elle peut être liée à deux occurrences différentes de protéines. En plus, de permettre la détection de règles mortes, qui ne pourront jamais être appliquées dans le modèle, le résultat est présenté graphiquement sous la forme de lemmes de raffinement, ce qui le rend compréhensible et facilement utilisable pour des analyses ultérieures. Il est ensuite possible de se concentrer sur le comportement des occurrences d'une protéine en particulier et d'obtenir un système de transitions pour décrire leurs changements potentiels de configuration. Cette analyse passe à l'échelle de grands modèles. Cependant, pour ceux-ci, le temps de calcul reste trop important pour permettre une analyse interactive et sans latence pendant l'écriture même des modèles. Une formulation du calcul du plus petit point fixe abstrait sous forme de résolution de clauses de Horn pourrait donner lieu à une analyse incrémentale. Celle-ci permettrait de mettre à jour très rapidement le résultat de l'analyse lorsque des règles sont retirées ou ajoutées à un modèle.

Par ailleurs, une collaboration étroite avec les modélisateurs est toujours nécessaire pour identifier des nouvelles familles de propriétés d'intérêt. Un autre axe de recherche est l'intégration de l'analyse statique dans des cycles de modélisations automatiques. En effet, les méthodes de fouille de la littérature basées sur l'intelligence artificielle et le traitement automatique des langages naturels pourront bénéficier de l'analyse statique d'une part pour évaluer le bien fondé d'une étape de raffinement de modèle et d'autre part pour orienter les méthodes automatiques dans leur recherche de nouvelles règles. En ce qui concerne la modélisation en Kappa, il est important de considérer non pas un réseau d'interactions biomoléculaires dans son individualité, mais une famille de réseaux d'interactions pouvant représenter un système dans différents contextes cellulaires et ses évolutions potentielles. Les travaux sur la plate-forme de modélisation Kami vont dans ce sens [92, 94]. Il est aussi important de proposer des méthodes pour assister le modélisateur dans la construction de modèles, afin d'agglomérer des informations partielles sur les interactions biomoléculaires en les raffinant progressivement. Une approche inspirée des approches déductives, qui assimile le processus de modélisation à une recherche de preuves assistée par ordinateur, est très prometteuse [98, 97]. Dans ce contexte, une analyse statique le plus tôt possible dans la chaîne de modélisation doit être développée pour aider au mieux le modélisateur dans sa tâche.

Améliorer l'interactivité des outils [14, 19] et un travail sur le rendu visuel des propriétés [82] sont des enjeux cruciaux pour créer des outils utilisables pour des modélisateurs non experts en langage formel. Il faut intéresser un spectre plus large d'utilisateurs. D'une part, c'est une source inépuisable de défis scientifiques. D'autre part, c'est nécessaire pour construire un nombre satisfaisant de modèles.

En ce qui concerne la réduction de modèles, deux approches ont été présentées.

1. La première se base sur l'étude des flots d'information. Il s'agit de détecter les états de quels sites influ-
encent l'évolution de tels autres dans les configurations des espèces biochimiques d'un modèle. De cette analyse, peuvent être déduits des découpages des configurations d'espèces biochimiques soit dont les états ne sont pas corrélés, soit dont la corrélation n'est pas importante pour suivre le comportement du modèle. Ceux-ci induisent des changements de variables qui réduisent la dimension des systèmes engendrés par les modèles. Cette approche se décline pour la sémantique différentielle et pour la sémantique stochastique. Cependant, alors qu'elle donne des résultats très prometteurs dans le cadre différentiel, elle ne réduit quasi-ment pas les modèles dans le cadre stochastique. Ceci est du à deux phénomènes. En stochastique, des pas de calculs peuvent agir de manière conjointe sur deux morceaux de configurations d'espèces biochimiques, ce qui impose d'en connaître les corrélations. Ceci ne pose aucun problème dans le cadre différentiel, où les actions s'appliquent, pour chacun des deux morceaux, sur une proportion de ceux-ci, indépendamment de leur distribution jointe. Par ailleurs, des termes de différents ordres de grandeur apparaissent dans la sémantique stochastique. Certains sont à l'origine de petits flots d'information qui établissent des cor-relations entre les états de différents morceaux de configurations des espèces biochimiques. Ces termes disparaissent dans la sémantique différentielle à la limite thermodynamique.

2. La seconde est basée sur l'étude des symétries entre les sites d'interaction des espèces biochimiques. Un cadre algébrique permet de définir quand plusieurs sites ont exactement le même comportement dans un modèle. Il en découle une relation de bisimulation avant-arrière qui permet de réduire les sémantiques différentielles et stochastiques des modèles en conséquence, essentiellement en imposant l'ordre selon lequel ces sites indiscernables sont activés. L'aspect bisimulation en avant assure que les états symétriques ont le même comportement vis à vis des classes de symétries des états. Alors que l'aspect bisimulation en arrière assure l'existence d'invariants quantitatifs quand les états initiaux ou les distributions initiales d'états satisfont eux aussi les symétries en question. Cette approche peut être étendue à des sous-groupes de symétries pour traiter des symétries plus exotiques comme celles rencontrées en stéréochimie ou comme les équivalences entre sites qui ne sont valables que sous certaines conditions sur l'état des autres sites. Dans ce cas, les symétries d'un modèle n'induisent pas forcément une bisimulation en avant, une bisimulation en arrière, ou une bisimulation avant-arrière. Il faut alors étudier si les transformations appliquées à la partie commune entre l'état juste avant d'appliquer chaque pas de calcul et celui juste après avoir appliqué celui-ci peuvent s'étendre à des transformations qui s'appliquent à l'état juste avant l'application de ce pas de calcul (pour la bisimulation arrière) ou juste après (pour la bisimulation en avant).

Tout comme l'analyse des symétries, l'analyse de flot peut être affinée en la rendant plus ou moins sensible au contexte, c'est à dire aux états des autres sites dans les occurrences des configurations des espèces biochimiques. La spécification de l'ensemble des contextes à distinguer reste alors à la charge de l'utilisateur. Il sera important de proposer des heuristiques pour automatiser ce paramètre, afin de proposer une large gamme de compromis entre le temps de l'analyse et sa capacité de réduction.

Les modèles sont de plus en plus grands, que ce soit en nombre de configurations d'espèces biochimiques différentes ou en nombre d'instances des complexes biochimiques. Évaluer leurs comportements est primordial, mais difficile. Les méthodes exactes de réduction de modèles sont utiles, mais limitées, pour ce type de mod-èles. Il est important de développer des méthodes numériques approchées pour les sémantiques différentielles et stochastiques des modèles qui permettront de trouver un encadrement garanti de l'évolution du nombre d'instances ou de la concentration, selon le choix de la sémantique, de motifs d'intérêt au cours du temps, sous la forme de paires de fonctions, elles-mêmes définies comme la solution d'un système différentiel ou comme les trajectoires d'un système stochastique. Des travaux préliminaires ont permis d'intégrer dans un cadre formel des méthodes de troncation de développement formel [123] ou des méthodes inspirées de la physique comme la tropicalisation [7], tout en fournissant des bornes évoluant au cours de l'exécution des modèles sur les erreurs numériques accumulées. Il devrait également être possible de définir une version quantitative de l'analyse de flot d'information entre sites des protéines, afin de négliger les petits flots d'information, au prix d'une perte de précision dans les modèles réduits. Un cadre formel pour l'exécution numériquement approchée des modèles permettra d'interfacer les sémantiques différentielles et stochastiques de Kappa pour concevoir une sémantique hybride, plus adaptée à la description des interactions entre des complexes biochimiques géants rares et des petits complexes présents en très grand nombre.
Références bibliographiques

[1] Wassim ABOU-JAoudé, Jérôme FERET et Denis THIEFFRY : Derivation of qualitative dynamical models from biochemical networks. In Olivier F. ROUX et Jérémie BOURDON, éditeurs : *Computational Methods in Systems Biology - 13th International Conference, CMSB 2015, Nantes, France, September 16-18, 2015*, *Proceedings*, volume 9308 de *Lecture Notes in Computer Science*, pages 195-207. Springer, 2015.

[2] Wassim ABOU-JAoudé, Denis THIEFFRY et Jérôme FERET : Formal derivation of qualitative dynamical models from biochemical networks. *Biosystems*, 149:70-112, 2016.

[3] Emilie ALLART, Joachim NIEHREN et Cristian VERSARI : Computing difference abstractions of metabolic networks under kinetic constraints. In Luca BORTOLUSSI et Guido SANGUINETTI, éditeurs : *Computational Methods in Systems Biology - 17th International Conference, CMSB 2019, Trieste, Italy, September 18-20, 2019, Proceedings*, volume 11773 de *Lecture Notes in Computer Science*, pages 266-285. Springer, 2019.

[4] Jakob L. ANDERSEN, Christoph FLAMM, Daniel MERKLE et Peter F. STADLER : A software package for chemically inspired graph transformation. In Rachid ECHAHED et Mark MINAS, éditeurs : *Graph Transformation - 9th International Conference, ICGT 2016, in Memory of Hartmut Ehrig, Held as Part of STAF 2016, Vienna, Austria, July 5-6, 2016, Proceedings*, volume 9761 de *Lecture Notes in Computer Science*, pages 73-88. Springer, 2016.

[5] Oana ANDREI et Hélène KIRCHNER : A rewriting calculus for multigraphs with ports. *Electr. Notes Theor. Comput. Sci.*, 219:67-82, 2008.

[6] Nicolas BEHR et Jean KRIVINE : Compositionality of rewriting rules with conditions. CoRR, abs/1904.09322, 2019.

[7] Andreea BEICA, Jérôme FERET et Tatjana PETROV : Tropical abstraction of biochemical reaction networks with guarantees. *Electr. Notes Theor. Comput. Sci.*, 350:3-32, 2020.

[8] Bruno BLANCHET, Patrick COUSOT, Radhia COUSOT, Jérôme FERET, Laurent MAUBORGNE, Antoine MINÉ, David MONNIAUX et Xavier RIVAL : A static analyzer for large safety-critical software. In Ron CYTRON et Rajiv GUPTA, éditeurs : *Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, San Diego, California, USA, June 9-11, 2003*, pages 196-207, 2003.

[9] Michael L. BLINOV, James R. FAEDER, Byron GOLDSTEIN et William S. HLAVACEK : Bionetgen: software for rule-based modeling of signal transduction based on the interactions of molecular domains. *Bioinformatics*, 20(17), 2004.

[10] Michael L. BLINOV, James R. FAEDER, Byron GOLDSTEIN et William S. HLAVACEK : A network model of early events in epidermal growth factor receptor signaling that accounts for combinatorial complexity. *BioSystems*, 83:136-151, 2006.

[11] Chiara BODEI, Linda BRODO, Roberta GORI, Diana HERMITH et Francesca LEVI : A global occurrence counting analysis for brane calculi. In Moreno FALASCHI, éditeur : *Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers*, volume 9527 de *Lecture Notes in Computer Science*, pages 179-200. Springer, 2015.
[12] Chiara BODEI, Pierpaolo DEGANO, Flemming NIELSON et Hanne Riis NIELSON : Control flow analysis for the pi-calculus. In Davide SANGIORGI et Robert de SIMONE, éditeurs : CONCUR '98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings, volume 1466 de Lecture Notes in Computer Science, pages 84–98. Springer, 1998.

[13] Nikolay M. BORISOV, Nick I. MARKEVICH, Boris N. KHOLODENKO et Ernst Dieter GILLES : Signaling through receptors and scaffolds: Independent interactions reduce combinatorial complexity. *Biophysical Journal*, 89, 2005.

[14] Pierre BOUTILLIER : The kappa simulator made interactive. In Luca BORTOLUSSI et Guido SANGUINETTI, éditeurs : Computational Methods in Systems Biology - 17th International Conference, CMSB 2019, Trieste, Italy, September 18-20, 2019, Proceedings, volume 11773 de Lecture Notes in Computer Science, pages 296–301. Springer, 2019.

[15] Pierre BOUTILLIER, Ferdinanda CAMPORESI, Jean COQUET, Jérôme FERET, Kim Quyên LÝ, Nathalie THÉRET et Pierre VIGNET : Kasa: A static analyzer for kappa. In Milan CESKA et David SAFRÁNEK, éditeurs : Computational Methods in Systems Biology - 16th International Conference, CMSB 2018, Brno, Czech Republic, September 12-14, 2018, Proceedings, volume 11095 de Lecture Notes in Computer Science, pages 285–291. Springer, 2018.

[16] Pierre BOUTILLIER, Ioana CRISTESCU et Jérôme FERET : Counters in kappa: Semantics, simulation, and static analysis. In Luís CAIRES, éditeur : Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 de Lecture Notes in Computer Science, pages 176–204. Springer, 2019.

[17] Pierre BOUTILLIER, Thomas EHRHARD et Jean KRIVINE : Incremental update for graph rewriting. In Hongseok YANG, éditeur : Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 de Lecture Notes in Computer Science, pages 201–228. Springer, 2017.

[18] Pierre BOUTILLIER, Aurélie FAURE DE PEBEYRE et Jérôme FERET : Proving the absence of unbounded polymers in rule-based models. In *Nine International Workshop on Static Analysis and Systems Biology (SASB'18)*, volume 350 de *ENTCS*, pages 33–56. elsevier, 2020.

[19] Pierre BOUTILLIER, Mutaamba MAASHA, Xing LI, Héctor F. MEDINA-ABARCA, Jean KRIVINE, Jérôme FERET, Ioana CRISTESCU, Angus G. FORBES et Walter FONTANA : The kappa platform for rule-based modeling. *Bioinformatics*, 34(13):i583–i592, 2018.

[20] Frances A. BRIGHTMAN et David A. FELL : Differential feedback regulation of the mapk cascade underlies the quantitative differences in egf and ngf signalling in pc12 cells. *FEBS Letters*, 482(3):169–174, 2000.

[21] Peter BUCHHOLZ : Exact and ordinary lumpability in finite markov chains. *Journal of Applied Probability*, 31(1):59–75, 1994.

[22] Peter BUCHHOLZ : Bisimulation relations for weighted automata. *TCS*, 393(1-3):109–123, 2008.

[23] Ferdinanda CAMPORESI : *Formal and exact reduction for differential models of signalling pathways in rule-based languages*. Thèse de doctorat, Paris Sciences et Lettres Research University, January 2017.

[24] Ferdinanda CAMPORESI et Jérôme FERET : Formal reduction for rule-based models. In Michael W. MISLOVE et Joël OUAKNINE, éditeurs : Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, May 25-28, 2011, volume 276 de Electronic Notes in Theoretical Computer Science, pages 29–59. Elsevier, 2011.

[25] Ferdinanda CAMPORESI et Jérôme FERET : Using alternated sums to express the occurrence number of extended patterns in site-graphs. In Jean YANG et John A. BACHMAN, éditeurs : SASB 2017 - The Eighth International Workshop on Static Analysis for Systems Biology, Static Analysis and Systems Biology, page 18, New York, United States, août 2017. Elsevier. To appear.
[26] Ferdinanda CAMPORESI, Jérôme FERET et Jonathan HAYMAN : Context-sensitive flow analyses: A hierarchy of model reductions. In Ashutosh GUPTA et Thomas A. HENZINGER, éditeurs : *Computational Methods in Systems Biology - 11th International Conference, CMSB 2013, Klosterneuburg, Austria, September 22-24, 2013. Proceedings*, volume 8130 de *Lecture Notes in Computer Science*, pages 220-233. Springer, 2013.

[27] Ferdinanda CAMPORESI, Jérôme FERET, Heinz KOEPPL et Tatjana PETROV : Combining model reductions. In *MFPSXXVI: Postproceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics*, volume 265 de *Electronic Notes in Theoretical Computer Science*, pages 73-96. Elsevier Science Publishers, 2010.

[28] Ferdinanda CAMPORESI, Jérôme FERET et Kim Quyên LÝ : KADE: a tool to compile kappa rules into (reduced) ode models: Supplementary information.

[29] Ferdinanda CAMPORESI, Jérôme FERET et Kim Quyên LÝ : Kade: A tool to compile kappa rules into (reduced) ODE models. In Jérôme FERET et Heinz KOEPPL, éditeurs : *Computational Methods in Systems Biology - 15th International Conference, CMSB 2017, Darmstadt, Germany, September 27-29, 2017, Proceedings*, volume 10545 de *Lecture Notes in Computer Science*, pages 291-299. Springer, 2017.

[30] Luca CARDELLI : Brane calculi. In Vincent DANOS et Vincent SCHÄCHTER, éditeurs : *Computational Methods in Systems Biology, International Conference, CMSB 2004, Paris, France, May 26-28, 2004, Revised Selected Papers*, volume 3082 de *Lecture Notes in Computer Science*, pages 257-278. Springer, 2004.

[31] Luca CARDELLI et Andrew D. GORDON : Mobile ambients. In Maurice NIVAT, éditeur : *Foundations of Software Science and Computation Structure, First International Conference, FoSSaCS'98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings*, volume 1378 de *Lecture Notes in Computer Science*, pages 140-155. Springer, 1998.

[32] Luca CARDELLI et Andrew D. GORDON : Mobile ambients. *Theor. Comput. Sci.*, 240(1):177-213, 2000.

[33] Luca CARDELLI, Giuseppe SQUILLACE, Mirco TRIBASTONE, Max TSCHAIKOWSKI et Andrea VANDIN : Formal lumping of polynomial differential equations through approximate equivalences. *J. Log. Algebraic Methods Program.*, 134:100876, 2023.

[34] Luca CARDELLI, Mirco TRIBASTONE, Max TSCHAIKOWSKI et Andrea VANDIN : Forward and backward bisimulations for chemical reaction networks. In Luca ACETO et David de FRUTOS-ESCRIG, éditeurs : *Proc. CONCUR'15*, volume 42 de *LIPIcs*, pages 226-239. Schloss Dagstuhl, 2015.

[35] Luca CARDELLI, Mirco TRIBASTONE, Max TSCHAIKOWSKI et Andrea VANDIN : Efficient syntax-driven lumping of differential equations. In Marsha CHECHIK et Jean-François RASKIN, éditeurs : *Proc. TACAS'16*, volume 9636 de *LNCS*, pages 93-111. Springer, 2016.

[36] Luca CARDELLI, Mirco TRIBASTONE, Max TSCHAIKOWSKI et Andrea VANDIN : Symbolic computation of differential equivalences. *Theor. Comput. Sci.*, 777:132-154, 2019.

[37] Federica CIOCCHETTA et Jane HILLSTON : Bio-PEPA: A framework for the modelling and analysis of biological systems. *Theoretical Computer Science*, 410(33-34):3065-3084, 2009. Concurrent Systems Biology: To Nadia Busi (1968-2007).

[38] Paul R. COHEN : DARPA's big mechanism program. *Physical Biology*, 12(4):045008, jul 2015.

[39] Holger CONZELMANN, Dirk FEY et Ernst D. GILLES : Exact model reduction of combinatorial reaction networks. *BMC Systems Biology*, 2:78, 2008.

[40] Holger CONZELMANN, Julio SAEZ-RODRIGUEZ, Thomas SAUTER, Boris N. KHOLODENKO et Ernst D. GILLES : A domain-oriented approach to the reduction of combinatorial complexity in signal transduction networks. *BMC Bioinformatics*, 7, 2006.
[41] Byron COOK, Jasmin FISHER, Elzbieta KREPSKA et Nir PITERMAN : Proving stabilization of biological systems. In Ranjit JHALA et David A. SCHMIDT, éditeurs : *Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011*. *Proceedings*, volume 6538, pages 134–149. Springer, 2011.

[42] Andrea CORRADINI, Tobias HEINDEL, Frank HERMANN et Barbara KÖNIG : Sesqui-pushout rewriting. In Andrea CORRADINI, Hartmut EHRIG, Ugo MONTANARI, Leila RIBEIRO et Grzegorz ROZENBERG, éditeurs : *Graph Transformations, Third International Conference, ICGT 2006, Natal, Rio Grande do Norte, Brazil, September 17-23, 2006, Proceedings*, volume 4178 de *Lecture Notes in Computer Science*, pages 30–45. Springer, 2006.

[43] Andrea CORRADINI, Ugo MONTANARI, Francesca ROSSI, Hartmut EHRIG, Reiko HECKEL et Michael LÖWE : Algebraic approaches to graph transformation - part I: basic concepts and double pushout approach. In Grzegorz ROZENBERG, éditeur : *Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations*, pages 163–246. World Scientific, 1997.

[44] Patrick COUSOT : The calculational design of a generic abstract interpreter. In M. BROY et R. STEINBRÜGGEN, éditeurs : *Calculational System Design*, pages 1–88. NATO ASI Series F. IOS Press, Amsterdam, 1999.

[45] Patrick COUSOT : Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. *Theoretical Computer Science*, 277(1-2):47-103, 2002.

[46] Patrick COUSOT et Radhia COUSOT : Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Robert M. GRAHAM, Michael A. HARRISON et Ravi SETHI, éditeurs : *Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977*, pages 238–252. ACM, 1977.

[47] Patrick COUSOT et Radhia COUSOT : Systematic design of program analysis frameworks. In Alfred V. AHO, Stephen N. ZILLES et Barry K. ROSEN, éditeurs : *Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979*, pages 269–282. ACM Press, 1979.

[48] Troels Christoffer DAMGAARD, Espen HØJSGAARD et Jean KRIVINE : Formal cellular machinery. *Electr. Notes Theor. Comput. Sci.*, 284:55-74, 2012.

[49] Werner DAMM et David HAREL : LSCs: Breathing life into message sequence charts. *Formal Methods in System Design*, 19(1):45-80, 2001.

[50] Vincent DANOS, Jérôme FERET, Walter FONTANA, Russell HARMER, Jonathan HAYMAN, Jean KRIVINE, Christopher D. THOMPSON-WALSH et Glynn WINSKEL : Graphs, rewriting and pathway reconstruction for rule-based models. In Deepak D'SOUZA, Telikepalli KAVITHA et Jaikumar RADHAKRISHNAN, éditeurs : *IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India*, volume 18 de *LIPIcs*, pages 276–288. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012.

[51] Vincent DANOS, Jérôme FERET, Walter FONTANA, Russell HARMER et Jean KRIVINE : Rule-based modelling of cellular signalling. In Luís CAIRES et Vasco Thudichum VASCONCELOS, éditeurs : *CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings*, volume 4703 de *Lecture Notes in Computer Science*, pages 17–41. Springer, 2007.

[52] Vincent DANOS, Jérôme FERET, Walter FONTANA, Russell HARMER et Jean KRIVINE : Rule-based modelling, symmetries, refinements. In Jasmin FISHER, éditeur : *Formal Methods in Systems Biology, First International Workshop, FMSB 2008, Cambridge, UK, June 4-5, 2008. Proceedings*, volume 5054 de *Lecture Notes in Computer Science*, pages 103–122. Springer, 2008.

[53] Vincent DANOS, Jérôme FERET, Walter FONTANA, Russell HARMER et Jean KRIVINE : Abstracting the differential semantics of rule-based models: Exact and automated model reduction. In *Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom*, pages 362–381. IEEE Computer Society, 2010.
[54] Vincent DANOS, Jérôme FERET, Walter FONTANA et Jean KRIVINE : Scalable simulation of cellular signaling networks. In Zhong SHAO, éditeur : *Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings*, volume 4807 de *Lecture Notes in Computer Science*, pages 139-157. Springer, 2007.

[55] Vincent DANOS, Jérôme FERET, Walter FONTANA et Jean KRIVINE : Scalable simulation of cellular signaling networks, invited paper. In *APLAS'07: Proceedings of the Fifth Asian Symposium on Programming Systems*, volume 4807 de *Lecture Notes in Computer Science*, pages 139–157. Springer, Berlin, Germany, 2007.

[56] Vincent DANOS, Jérôme FERET, Walter FONTANA et Jean KRIVINE : Abstract interpretation of cellular signalling networks. In Francesco LOGOZZO, Doron A. PELED et Lenore D. ZUCK, éditeurs : *Verification, Model Checking, and Abstract Interpretation, 9th International Conference, VMCAI 2008, San Francisco, USA, January 7-9, 2008, Proceedings*, volume 4905 de *Lecture Notes in Computer Science*, pages 83–97. Springer, 2008.

[57] Vincent DANOS, Ricardo HONORATO-ZIMMER, Se JARAMILLO-RIVERI et Sandro STUCKI : Rigid geometric constraints for Kappa models. In *SASB'12: PostProceedings of the 3rd International Workshop on Static Analysis and Systems Biology*, volume 313 de *ENTCS*, pages 23–46. Elsevier, 2015.

[58] Vincent DANOS et Cosimo LANEVE : Graphs for core molecular biology. In Corrado PRIAMI, éditeur : *Computational Methods in Systems Biology, First International Workshop, CMSB 2003, Roverto, Italy, February 24-26, 2003, Proceedings*, volume 2602 de *Lecture Notes in Computer Science*, pages 34–46. Springer, 2003.

[59] Vincent DANOS et Cosimo LANEVE : Formal molecular biology. *Theoretical Computer Science*, 325(1):69 – 110, 2004. Computational Systems Biology.

[60] Vincent DANOS et Sylvain PRADALIER : Projective brane calculus. In Vincent DANOS et Vincent SCHÄCHTER, éditeurs : *Computational Methods in Systems Biology, International Conference, CMSB 2004, Paris, France, May 26-28, 2004, Revised Selected Papers*, volume 3082 de *Lecture Notes in Computer Science*, pages 134–148. Springer, 2004.

[61] Tadeas DED, David SAFRÁNEK, Matej TROJÁK, Matej KLEMENT, Jakub SALAGOVIC et Lubos BRIM : Formal biochemical space with semantics in kappa and BNGL. *Electr. Notes Theor. Comput. Sci.*, 326:27–49, 2016.

[62] Lorenzo DEMATTÉ, Corrado PRIAMI et Alessandro ROMANEL : The blenx language: A tutorial. In Marco BERNARDO, Pierpaolo DEGANO et Gianluigi ZAVATTARO, éditeurs : *Formal Methods for Computational Systems Biology: 8th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2008 Bertinoro, Italy, June 2-7, 2008 Advanced Lectures*, pages 313–365, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.

[63] Josée DESHARNAIS, Vineet GUPTA, Radha JAGADEESAN et Prakash PANANGADEN : Metrics for labeled markov systems. In Jos C. M. BAETEN et Sjouke MAUW, éditeurs : *CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings*, volume 1664 de *Lecture Notes in Computer Science*, pages 258–273. Springer, 1999.

[64] Jacob L. DOOB : Markoff chains–denumerable case. *Transactions of the American Mathematical Society*, 58(3):455–473, 1945.

[65] James R. FAEDER, Michael L. BLINOV, Byron GOLDSTEIN et William S. HLAVACEK : Rule-based modeling of biochemical networks. *Complexity*, 10(4):22–41, 2005.

[66] Manuel FÄHNDRICH et Francesco LOGOZZO : Static contract checking with abstract interpretation. In Bernhard BECKERT et Claude MARCHÉ, éditeurs : *Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers*, volume 6528 de *LNCS*, pages 10–30. Springer, 2010.

[67] Martin FEINBERG : Lectures on chemical reaction networks, 1979. Notes of lectures given at the Mathematics Research Centre, University of Wisconsin, in 1979.
[68] Willy FELLER : On the integro-differential equations of purely discontinuous markoff processes. *Transactions of the American Mathematical Society*, 48(3):488-515, 1940.

[69] Jérôme FERET : Confidentiality analysis of mobile systems. In *Jens PALSBERG*, éditeur : *Static Analysis, 7th International Symposium, SAS 2000, Santa Barbara, CA, USA, June 29 - July 1, 2000, Proceedings*, volume 1824 de *Lecture Notes in Computer Science*, pages 135-154. Springer, 2000.

[70] Jérôme FERET : Occurrence counting analysis for the pi-calculus. *Electr. Notes Theor. Comput. Sci.*, 39(2):1-18, 2001.

[71] Jérôme FERET : Reachability analysis of biological signalling pathways by abstract interpretation. In *Proc. ICCMSE'07*, volume 963 de *AIP*, 2007.

[72] Jérôme FERET : Fragments-based model reduction: some case studies. In *Jean KRIVINE* et *Angelo TROINA*, éditeurs : *Préproceedings of the First International Workshop on Interactions between Computer Science and Biology, CS2Bio '2010*, volume 268 de *Electonic Notes in Theoretical Computer Science*, pages 77-96, Amsterdam, Netherlands, 10 June 2010. Elsevier Science Publishers.

[73] Jérôme FERET : An algebraic approach for inferring and using symmetries in rule-based models. In *Loïc PAULEVÉ* et *Heinz KOEPPL*, éditeurs : *5th International Workshop on Static Analysis and Systems Biology (SASB 2014)*, volume 316 de *ENTCS*, pages 45-65. Elsevier, 2014.

[74] Jérôme FERET, Vincent DANOS, Jean KRIVINE, Russ HARMER et Walter FONTANA : Internal coarse-graining of molecular systems. *PNAS*, 2009.

[75] Jérôme FERET, Thomas A. HENZINGER, Heinz KOEPPL et Tatjana PETROV : Lumpability abstractions of rule-based systems. *Theor. Comput. Sci.*, 431:137-164, 2012.

[76] Jérôme FERET, Heinz KOEPPL et Tatjana PETROV : Stochastic fragments: A framework for the exact reduction of the stochastic semantics of rule-based models. *Int. J. Software and Informatics*, 7(4):527-604, 2013.

[77] Jérôme FERET et Kim Quyên LÝ : Local traces: An over-approximation of the behaviour of the proteins in rule-based models. In *Ezio BARTOCCI*, Pietro Liò et Nicola PAOLETTI, éditeurs : *Computational Methods in Systems Biology - 14th International Conference, CMSB 2016, Cambridge, UK, September 21-23, 2016, Proceedings*, volume 9859 de *Lecture Notes in Computer Science*, pages 116-131. Springer, 2016.

[78] Jérôme FERET et Kim Quyên LÝ : Local traces: An over-approximation of the behavior of the proteins in rule-based models. *IEEE/ACM Transactions on Computational Biology and Bioinformatics*, 15(4):1124-1137, July-Aug. 2018.

[79] Jérôme FERET et Kim Quyên LÝ : Reachability analysis via orthogonal sets of patterns. *Electr. Notes Theor. Comput. Sci.*, 335:27-48, 2018.

[80] Norm FERNS, Prakash PANANGADEN et Doina PRECUP : Bisimulation metrics for continuous markov decision processes. *SIAM J. Comput.*, 40(6):1662-1714, 2011.

[81] Maxime FOLSCHETTE, Loïc PAULEVÉ, Morgan MAGNIN et Olivier F. ROUX : Under-approximation of reachability in multivalued asynchronous networks. *Electr. Notes Theor. Comput. Sci.*, 299:33-51, 2013.

[82] Angus Graeme FORBES, Andrew BURKS, Kristine LEE, Xing LI, Pierre BOUTILLIER, Jean KRIVINE et Walter FONTANA : Dynamic influence networks for rule-based models. *IEEE Trans. Vis. Comput. Graph.*, 24(1):184-194, 2018.

[83] Qian GAO, Fei LIU, David GILBERT, Monika HEINER et David TREE : A multiscale approach to modelling planar cell polarity in drosophila wing using hierarchically coloured petri nets. *In Proceedings of the 9th International Conference on Computational Methods in Systems Biology*, CMSB '11, pages 209-218, New York, NY, USA, 2011. ACM.

[84] Steven GAY, François FAGES, Thierry MARTINEZ, Sylvain SOLIMAN et Christine SOLNON : On the subgraph epimorphism problem. *Discrete Applied Mathematics*, 162:214-228, 2014.
[85] Colin S. GILLESPIE : Moment-closure approximations for mass-action models. *IET systems biology*, 3(1):52–58, 2009.

[86] Daniel T. GILLESPIE : Exact stochastic simulation of coupled chemical reactions. *The Journal of Physical Chemistry*, 81(25):2340–2361, 1977.

[87] Roberta GORI et Francesca LEVI : An analysis for proving temporal properties of biological systems. In Naoki KOBAYASHI, éditeur : *Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006, Proceedings*, volume 4279 de *Lecture Notes in Computer Science*, pages 234–252. Springer, 2006.

[88] Radu GROSU, Grégory BATT, Flavio H. FENTON, James GLIMM, Colas Le GUERNIC, Scott A. SMOLKA et Ezio BARTOCCI : From cardiac cells to genetic regulatory networks. In Ganesh GOPALAKRISHNAN et Shaz QADEER, éditeurs : *Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings*, volume 6806 de *Lecture Notes in Computer Science*, pages 396–411. Springer, 2011.

[89] Benjamin GYORI, John BACHMAN, Kartik SUBRAMANIAN, Jeremy MUHLICH, Lucian GALESCU et Peter SORGER : From word models to executable models of signaling networks using automated assembly. *Molecular Systems Biology*, 13, 2017.

[90] Joseph Y. HALPERN et Judea PEARL : Causes and explanations: A structural-model approach — part 1: Causes. *CoRR*, abs/1301.2275, 2013.

[91] Russ HARMER : Rule-based modelling and tunable resolution. In *DCM'09: Proceedings Fifth Workshop on Developments in Computational Models-Computational Models From Nature*, volume 9 de *EPTCS*, pages 65–72, 2009.

[92] Russ HARMER, Yves-Stan Le CORNEC, Sébastien LÉGARÉ et Eugenia OSHURKO : Bio-curation for cellular signalling: The KAMI project. *IEEE/ACM Trans. Comput. Biology Bioinform.*, 16(5):1562–1573, 2019.

[93] Russ HARMER, Vincent DANOS, Jérôme FERET, Jean KRIVINE et Walter FONTANA : Intrinsic information carriers in combinatorial dynamical systems. *Chaos*, 20, September 2010.

[94] Russ HARMER et Eugenia OSHURKO : Kamistudio: An environment for biocuration of cellular signalling knowledge. In Luca BORTOLUSSI et Guido SANGUINETTI, éditeurs : *Computational Methods in Systems Biology - 17th International Conference, CMSB 2019, Trieste, Italy, September 18-20, 2019, Proceedings*, volume 11773 de *Lecture Notes in Computer Science*, pages 322–328. Springer, 2019.

[95] Monika HEINER et Ina KOCH : Petri net based model validation in systems biology. In Jordi CORTADELLA et Wolfgang REISIG, éditeurs : *Applications and Theory of Petri Nets 2004: 25th International Conference, ICATPN 2004, Bologna, Italy, June 21-25, 2004. Proceedings*, pages 216–237. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004.

[96] Tobias HELMS, Tom WARNKE, Carsten MAUS et Adelinde M. UHRMACHER : Semantics and efficient simulation algorithms of an expressive multilevel modeling language. *ACM Trans. Model. Comput. Simul.*, 27(2):8:1–8:25, 2017.

[97] Adrien HUSSON : *Logical foundations of a modelling assistant for molecular biology*. Thèse de doctorat, Université de Paris, France, 2019.

[98] Adrien HUSSON et Jean KRIVINE : A tractable logic for molecular biology. In Bart BOGAERTS, Esra ERDEM, Paul FODOR, Andrea FORMISANO, Giovambattista IANNI, Daniela INCLEZAN, Germán VIDAL, Alicia VILLANUEVA, Marina De VOS et Fangkai YANG, éditeurs : *Proceedings 35th International Conference on Logic Programming (Technical Communications), ICLP 2019 Technical Communications, Las Cruces, NM, USA, September 20-25, 2019.*, volume 306 de *EPTCS*, pages 101–113, 2019.

[99] Edward L. INCE : *Ordinary Differential Equations*. Dover Publications, Inc., 1956.
[100] Mathias JOHN, Cédric LHOUSSAINE, Joachim NIEHREN et Cristian VERSARI : Biochemical reaction rules with constraints. *In Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings*, volume 6602 de *Lecture Notes in Computer Science*, pages 338-357. Springer, 2011.

[101] Mathias JOHN, Mirabelle NEBUT et Joachim NIEHREN : Knockout prediction for reaction networks with partial kinetic information. In Roberto GIACOBAZZI, Josh BERDINE et Isabella MASTROENI, éditeurs : *Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings*, volume 7737 de *Lecture Notes in Computer Science*, pages 355-374. Springer, 2013.

[102] Ozan KAHRAMANOGULLARI et Luca CARDELLI : An intuitive modelling interface for systems biology. *Int. J. Software and Informatics*, 7(4):655-674, 2013.

[103] Hannes KLARNER, Alexander BOCKMAYR et Heike SIEBERT : Computing maximal and minimal trap spaces of boolean networks. *Natural Computing*, 14(4):535-544, 2015.

[104] Agnes KÖHLER, Jean KRIVINE et Jakob VIDMAR : A rule-based model of base excision repair. In Pedro MENDES, Joseph O. DADA et Kieran SMALLBONE, éditeurs : *Computational Methods in Systems Biology - 12th International Conference, CMSB 2014, Manchester, UK, November 17-19, 2014, Proceedings*, volume 8859 de *Lecture Notes in Computer Science*, pages 173-195. Springer, 2014.

[105] Juraj KOLCÁK, David SAFRÁNEK, Stefan HAAR et Loïc PAULEVÉ : Parameter space abstraction and unfolding semantics of discrete regulatory networks. *Theor. Comput. Sci.*, 765:120-144, 2019.

[106] Andrey KOLMOGOROFF : Über die analytischen methoden in der wahrscheinlichkeitsrechnung. *Mathe-matische Annalen*, 104:415-458, 1931.

[107] Marta Z. KWIATKOWSKA, Gethin NORMAN et David PARKER : PRISM 4.0: Verification of probabilistic real-time systems. In Ganesh GOPALAKRISHNAN et Shaz QADEER, éditeurs : *Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings*, volume 6806 de *Lecture Notes in Computer Science*, pages 585-591. Springer, 2011.

[108] Jonathan LAURENT, Jean YANG et Walter FONTANA : Counterfactual resimulation for causal analysis of rule-based models. In Jérôme LANG, éditeur : *Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden.*, pages 1882-1890. ijcai.org, 2018.

[109] Michael LÖWE : Algebraic approach to single-pushout graph transformation. *Theor. Comput. Sci.*, 109(1&2):181-224, 1993.

[110] Antoni W. MAZURKIEWICZ : Traces, histories, graphs: Instances of a process monoid. In Michal CHYTIL et Václav KOUBEK, éditeurs : *Mathematical Foundations of Computer Science 1984, Praha, Czechoslovakia, September 3-7, 1984, Proceedings*, volume 176 de *Lecture Notes in Computer Science*, pages 115-133. Springer, 1984.

[111] Donald A. MCQUARRIE : Stochastic approach to chemical kinetics. *Journal of Applied Probability*, 4(3):pp. 413-478, 1967.

[112] Elaine MURPHY, Vincent DANOS, Jérôme FERET, Jean KRIVINE et Russell HARMER : *Elements of Computational Systems Biology*, chapitre Rule Based Modelling and Model Refinement. Wiley Book Series on Bioinformatics. John Wiley & Sons, Inc., 2010.

[113] Hanne Riis NIELSON et Flemming NIELSON : Shape analysis for mobile ambients. In Mark N. WEGMAN et Thomas W. REPS, éditeurs : *POPL 2000, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, January 19-21, 2000*, pages 142-154. ACM, 2000.

[114] Arnold NORDSIECK, Willis E. LAMB et George E. UHLENBECK : On the theory of cosmic-ray showers in the furry model and the fluctuation problem. *Physica*, 7(4):344-360, 1940.
[115] Loïc PAULEVÉ, Morgan MAGNIN et Olivier F. ROUX : Abstract interpretation of dynamics of biological regulatory networks. *Electr. Notes Theor. Comput. Sci.*, 272:43-56, 2011.

[116] Tatjana PETROV : *Formal reductions of stochastic rule-based models of biochemical systems*. Thèse de doctorat, Eth Zürich, 2013.

[117] Tatjana PETROV, Jérôme FERET et Heinz KOEPPL : Reconstructing species-based dynamics from reduced stochastic rule-based models. In Oliver ROSE et Adelinde M. UHRMACHER, éditeurs : *Winter Simulation Conference, WSC '12, Berlin, Germany, December 9-12, 2012*, pages 225:1-225:15. WSC, 2012.

[118] Brigitte PLATEAU : On the stochastic structure of parallelism and synchronization models for distributed algorithms. *SIGMETRICS Perform. Eval. Rev.*, 13(2):147-154, août 1985.

[119] Ovidiu RADULESCU, Alexander N. GORBAN, Andrei ZINOVYEV et Vincent NOEL : Reduction of dynamical biochemical reactions networks in computational biology. *Frontiers in Genetics*, 3:131, 2012.

[120] Ovidiu RADULESCU, Sergei VAKULENKO et Dima GRIGORIEV : Model reduction of biochemical reactions networks by tropical analysis methods. *Mathematical Modelling of Natural Phenomena*, 10(3):124-138, 2015.

[121] Aviv REGEV, E. M. PANINA, William SILVERMAN, Luca CARDELLI et E. Y. SHAPIRO : Bioambients: An abstraction for biological compartments. *TCS*, 325(1):141-167, 2004.

[122] Aviv REGEV, William SILVERMAN et Ehud SHAPIRO : Representation and simulation of biochemical processes using the pi-calculus process algebra. In R. B. ALTMAN, A. K. DUNKER, L. HUNTER et T. E. KLEIN, éditeurs : *Pacific Symposium on Biocomputing, Volume 6*, pages 459-470, Singapore, 2001.

[123] Ken Chanseau SAINT-GERMAIN et Jérôme FERET : Conservative numerical approximations of the differential semantics in biological rule-based models, 2016. Master thesis.

[124] Birgit SCHOEBERL, Claudia EICHLER-JONSSON, Ernst D. GILLES et Gertraud MÜLLER : Computational modeling of the dynamics of the map kinase cascade activated by surface and internalized egf receptors. *Nat Biotechnol*, 20(4):370-375, 2002.

[125] Donald STEWART : Spatial biomodelling, 2010. Master thesis, School of Informatics, University of Edinburgh.

[126] Ryan SUDERMAN et Eric J. DEEDS : Machines vs. ensembles: effective mapk signaling through heterogeneous sets of protein complexes. *PLoS Computational Biology*, 9, 2013.

[127] Alfred TARSKI : A lattice-theoretical fixpoint theorem and its applications. *Pacific J. Math.*, 5(2), 1955.
# Index

## A

automorphisme (de motifs), 18

automorphisme (de règles), 21

## C

carte de contacts, 13

chevauchements (de motifs), 33

composante fortement connexe, 44

composante fortement connexe terminale, 45

concrétisation, 30

concrétisation (fonction de), 30

configuration d'espèces biochimiques, 14

configuration d'espèces biochimiques (orbite), 125

configurations symétriques d'espèces biochimiques, 108

contre-partie abstraite, 32

correspondance de Galois, 30

## D

distribution d'états symétrique, 134

## E

ensemble de motifs orthogonaux, 35

ensemble élémentaire de traces, 70

ensemble symétrique de règles, 120

équation maîtresse, 70

état (réseau réactionnel), 27

état d'activation, 13

état de liaison, 13

états différentiels symétriques, 128

## F

flot d'information, 44

fragment, 57

## H

homomorphisme, 15

## I

isomorphes (motifs), 18

isomorphisme (entre motifs), 18

isomorphismes (entre règles), 21

## L

lemme de raffinement, 39

loi d'action de masse, 46

## M

meilleure approximation, 30

motif, 15

motifs (isomorphisme entre), 18

motifs (orbite), 121

motifs isomorphes, 18

motifs symétriques, 109

## O

observable, 51

orbite, 120

orbite d'un motif, 121

orbite d'une configuration d'espèces biochimiques, 125

orbite d'une règle d'interaction, 120

## P

pas de calcul, 71

plongement, 17

plongements (symétriques, 114

pré-fragment, 57

## R

raffinement (lemme de), 39

raffinement orthogonal, 57

raffinements de règles symétriques, 118

règle d'interaction, 19

règle d'interaction (orbite), 120

règle morte, 27

règle-réaction, 23

règles (automorphisme de), 21

règles (isomorphes), 21

règles (isomorphismes entre), 21

règles d'interaction symétriques, 111

rigidité, 18

## S

site d'interaction, 13

somme amalgamée, 61

sorte de protéines, 13

symétrique (ensemble de règles), 120

symétriques (configurations d'espèces biochimiques), 108

symétriques (de plongements), 114

symétriques (distribution d'états), 134

symétriques (états différentiels), 128

symétriques (motifs), 109

symétriques (raffinements de règles), 118
symétriques (règles d'interaction), 111

T

théorème de Tarski, 28

trace locale, 40

traces (ensemble élémentaire de), 70

transition (réseau réactionnel), 28

V

vue locale, 29
## RÉSUMÉ

Les sciences du logiciel ont un rôle à jouer pour décrire, organiser, exécuter et analyser les systèmes d'interactions moléculaires tels que les voies de signalisation biologiques. Ceux-ci impliquent une grande diversité d'entités biomoléculaires, alors que leurs dynamiques émergent de compétitions pour des ressources communes, d'interactions à différentes échelles de temps et de concentrations et de boucles de rétroactions non linéaires. Comprendre comment le comportement des populations des protéines émerge des interactions individuelles, le saint Graal de la biologie des systèmes, nécessite des langages dédiés offrant des niveaux d'abstractions adaptés et des outils efficaces.

Dans ce manuscrit, nous décrivons la conception d'outils formels pour Kappa, un langage de réécriture de graphes à sites inspiré de la biochimie. En particulier, nous présentons une analyse statique qui calcule des propriétés sur les entités biologiques qui peuvent se former dans les modèles, et ainsi, améliorer notre confiance en ces derniers. Nous présentons de plus une réduction de modèles, basée sur l'étude du flot d'information entre les différentes régions des entités biologiques et sur des symétries éventuelles. Cette approche s'applique à la fois dans le cadre différentiel et stochastique.

## ABSTRACT

Software sciences have a role to play in the description, the organization, the execution, and the analysis of the molecular interaction systems such as biological signaling pathways. These systems involve a huge diversity of bio-molecular entities whereas their dynamics may be driven by races for shared resources, interactions at different time- and concentration-scales, and non-linear feedback loops. Understanding how the behavior of the populations of proteins orchestrates itself from their individual interactions, which is the holy grail on systems biology, requires dedicated languages offering adapted levels of abstraction and efficient analysis tools.

In this manuscript, we describe the design of formal tools for Kappa, a site-graph rewriting language inspired by bio-chemistry. In particular, we introduce a static analysis to compute some properties on the biological entities that may arise in models, so as to increase our confidence in them. We also present a model reduction approach based on a study of the flow of information between the different regions of the biological entities and the potential symmetries. This approach is applied both in the differential and in the stochastic semantics.