Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates

In this paper we apply the Abstract Interpretation approach [P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. Proc. of POPL'77, 238–252, 1977; P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. Proc. of POPL'79, 269–282, 1979] for approximating the behavior of biological systems, modeled specifically using the Chemical Ground Form calculus [L. Cardelli. On Process Rate Semantics. Theoretical Computer Science, 391 190–215, 2008], 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