Abstract Interpretation for Probabilistic Termination of Biological Systems

TL;DR

This paper extends an abstract interpretation framework to analyze probabilistic termination in biological systems, providing conservative bounds using refined models based on Interval Markov Chains.

Contribution

It introduces a refined abstract semantics and probabilistic abstraction method for analyzing termination in biological systems modeled with Chemical Ground Form.

Findings

Provides safe approximation of probabilistic termination

Reports conservative bounds for termination probabilities

Refines previous abstract interpretation approach

Abstract

In a previous paper the authors applied the Abstract Interpretation approach for approximating the probabilistic semantics of biological systems, modeled specifically using the Chemical Ground Form calculus. 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. The abstract probabilistic model safely approximates a set of concrete experiments and reports conservative lower and upper bounds for probabilistic termination.