# Formal Model Reduction

Jérôme Feret

► To cite this version:

Jérôme Feret. Formal Model Reduction. Static Analysis Symposium, Sep 2011, Venice, Italy. pp.6, 10.1007/978-3-642-23702-7_5. inria-00626640

HAL Id: inria-00626640

https://inria.hal.science/inria-00626640v1

Submitted on 16 Feb 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
Formal Model Reduction*

Jérôme Feret

Laboratoire d'informatique de l'École normale supérieure
(INRIA/ÉNS/CNRS)
www.di.ens.fr/~feret

Modelers of molecular signaling networks must cope with the combinatorial
explosion of protein states generated by post-translational modifications and
complex formations. Rule-based models provide a powerful alternative to ap-
proaches that require an explicit enumeration of all possible molecular species
of a system [1, 2]. Such models consist of formal rules stipulating the (partial)
contexts for specific protein-protein interactions to occur. The behavior of the
models can be formally described by stochastic or differential semantics. Yet, the
naive computation of these semantics does not scale to large systems, because it
does not exploit the lower resolution at which rules specify interactions.

We present a formal framework for constructing coarse-grained systems. We
instantiate this framework with two abstract domains. The first one tracks the
flow of information between the different regions of chemical species, so as to
detect and abstract away some useless correlations between the state of sites
of molecular species. The second one detects pairs of sites having the same
capabilities of interactions, and abstract away any distinction between them.

The result of our abstraction is a set of molecular patterns, called fragments,
and a system which describes exactly the concentration (or population) evolution
of these fragments. The method never requires the execution of the concrete
rule-based model and the soundness of the approach is described and proved
by abstract interpretation [3]. Unlike our previous analysis [4], our fragments
are heterogeneous. The cutting of a protein into portions may depend on its
position within the molecular species. This matches more closely with the flow
of information. Indeed, within a molecular species, the behavior of a protein may
be driven by the state of a site without being driven by the state of the same
site in other instances of the protein. Our new analysis exploits this efficiently.

(Joint work with F. Camporesi, V. Danos, W. Fontana, R. Harmer, and
J. Krivine.)

References

1. Danos, V., Laneve, C.: Formal molecular biology. TCS **325**(1) (2004)

2. Blinov, M.L., Faeder, J.R., Hlavacek, W.S.: BioNetGen: software for rule-based modeling of signal transduction based on the interactions of molecular domains. Bioinformatics **20** (2004)

3. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)

<footnote>* This work has been partially supported by ANR Chair of Excellence AbstractCell.</footnote>
4. Feret, J., Danos, V., Krivine, J., Harmer, R., Fontana, W.: Internal coarse-graining of molecular systems. PNAS (2009)