Formal abstraction of quantitative semantics for protein-protein interaction cellular network models.
Objectives and challenges
We want to investigate formal foundations and computational aspects of both the stochastic and differential approximate semantics for rule-based models: we will relate these semantics formally, then we will design sound approximations for each of these semantics (by abstract interpretation) and investigate scalable algorithms to compute the properties of both the stochastic and the differential semantics. Our approximations focus only on certain projections, thereby reducing the dimension of semantics.
Using formal methods provides several benefits:
- Firstly, it provides a clear separation between the design of models and the computation of model properties. This separation between model hypotheses and model approximation enables a better confidence level in the properties that are being computed. Moreover, it enables a better reusability of the model.
- Secondly, formal approaches allow for a better understanding of abstraction mechanisms, which will enable the design of new
abstraction techniques for rule-based protein-protein interaction models. We believe that our framework will lead to a greater reduction factor than existing methods, while ensuring the soundness of the approach.
Yet, we have to face several challenges:
- It is difficult to compute the trajectories of protein-protein interaction networks. Firstly, the number of non-isomorphic chemical species can be very large which prevents us from writing or integrating differential systems (each chemical species is denoted by a variable). Secondly, one can use agent-based simulation and describe each protein of the biological mixture explicitly. However, this approach does not scale when the size of mixture is too large.
- Besides, there is a lack of practical abstraction tools for reducing the dimension of differential or stochastic systems. Existing frameworks are purely theoretic and have no concrete example of applications yet.