Approximating Probabilistic Behaviours of Biological Systems using Abstract Interpretation

In this paper we apply the Abstract Interpretation approach for approximating the behavior of biological systems, modeled specifically using the Chemical Ground Form calculus, a new stochastic calculus rich enough to model the dynamics of biochemical reactions. Our analysis computes an Interval Markov Chain (IMC) that safely approximates the Discrete-Time Markov Chain, describing the probabilistic behavior of the system, and reports both lower and upper bounds for probabilistic temporal properties. Our analysis has several advantages: (i) the method is effective (even for infinite state systems) and allows us to systematically derive an IMC from an abstract labeled transition system; (ii) using intervals for abstracting the multiplicity of reagents allows us to achieve conservative bounds for the concrete probabilities of a set of concrete experiments which differs only for initial concentrations.