Formal derivation of qualitative dynamical models from biochemical networks.

As technological advances allow a better identification of cellular networks, large-scale molecular data are swiftly produced, allowing the construction of large and detailed molecular interaction maps. One approach to unravel the dynamical properties of such complex systems consists in deriving coarse-grained dynamical models from these maps, which would make the salient properties emerge. We present here a method to automatically derive such models, relying on the abstract interpretation framework to formally relate model behaviour at different levels of description. We illustrate our approach on two relevant case studies: the formation of a complex involving a protein adaptor, and a race between two competing biochemical reactions. States and traces of reaction networks are first abstracted by sampling the number of instances of chemical species within a finite set of intervals. We show that the qualitative models induced by this abstraction are too coarse to reproduce properties of interest. We then refine our approach by taking into account additional constraints, the mass invariants and the limiting resources for interval crossing, and by introducing information on the reaction kinetics. The resulting qualitative models are able to capture sophisticated properties of interest, such as a sequestration effect, which arise in the case studies and, more generally, participate in shaping the dynamics of cell signaling and regulatory networks. Our methodology offers new trade-offs between complexity and accuracy, and clarifies the implicit assumptions made in the process of qualitative modelling of biological networks.