Réduction formelle et exacte de modèles différentiels de voies de signalisation en Kappa

The behaviour of a cell is driven by its capability to receive, propagate and communicate signals. Proteins can bind together on some binding sites. Post-translational modifications can reveal or hide some sites, so new interactions can be allowed or existing ones can be inhibited. Due to the huge number of different bio-molecular complexes, we can no longer derive or integrate ODE models. A compact way to describe these systems is supplied by rule-based languages. However combinatorial complexity raises again when one attempt to describe formally the behaviour of the models. This motivates the use of abstractions. We propose two methods to reduce the size of the models, that exploit respectively the presence of symmetries between sites and the lack of correlation between different parts of the system. The symmetries relates pairs of sites having the same capability of interactions. We show that this relation induces a bisimulation which can be used to reduce the size of the original model. The information flow analysis detects, for each site, which parts of the system influence its behaviour. This allows us to cut the molecular species in smaller pieces and to write a new system. Moreover we show how this analysis can be tuned with respect to a context. Both approaches can be combined. The analytical solution of the reduced model is the exact projection of the original one. The computation of the reduced model is performed at the level of rules, without the need of executing the original model.Le comportement d'une cellule dépend de sa capacité à recevoir, propager et intégrer des signaux, constituant ainsi des voies de signalisations. Les protéines s'associent entre elles sur des sites de liaisons, puis modifient la structure spatiale des protéines voisines, ce qui a pour effet de cacher ou de découvrir leurs autres sites de liaisons, et donc d'empêcher ou de faciliter d'autres interactions. En raison du grand nombre de différents complexes bio-moléculaires, nous ne pouvons pas écrire ou générer les systèmes différentiels sous-jacents. Les langages de réécritures de graphes à sites offrent un bon moyen de décrire ces systèmes complexes. Néanmoins la complexité combinatoire resurgit lorsque l'on cherche à calculer de manière effective ce comportement. Ceci justifie l'utilisation d'abstractions. Nous proposons deux méthodes pour réduire la taille des modèles de voies de signalisation, décrits en Kappa. Ces méthodes utilisent respectivement la présence de symétries parmi certains sites et le fait que certaines corrélations entre l'état de différentes parties des complexes biomoléculaires n'ont pas d'impact sur la dynamique du système global. Des sites qui ont la même capacité d'interaction sont liés par une relation de symétrie. Nous montrons que cette relation induit une bisimulation qui peut être utilisée pour réduire la taille du modèle initial. L'analyse du flot d'information détecte les parties du système qui influencent le comportement de chaque site. Ceci nous autorise à couper les espèces moléculaires en petits morceaux pour écrire un nouveau système. Enfin, nous montrons comment raffiner cette analyse pour tenir compte d'information contextuelle. Les deux méthodes peuvent être combinées. La solution analytique du modèle réduit est la projection exacte de la solution originelle. Le calcul du modèle réduit se fait au niveau des règles, en évitant l'exécution du modèle initial