Abstract Interpretation for Probabilistic Termination of Biological Systems

In [5] the authors applied the Abstract Interpretation approach for approximating the probabilistic semantics of biological systems, modeled specifically using the Chemical Ground Form calculus [3]. The methodology is based on the idea of representing a set of experiments, which differ only for the initial concentrations, by abstracting the multiplicity of reagents present in a solution, using intervals. In this paper, we refine the approach in order to address probabilistic termination properties. More in details, we introduce a refinement of the abstract LTS semantics and we abstract the probabilistic semantics using a variant of Interval Markov Chains [34, 13, 19]. The abstract probabilistic model safely approximates a set of concrete experiments and reports conservative lower and upper bounds for probabilistic termination.