Automaton-ABC: A statistical method to estimate the probability of spatio-temporal properties for parametric Markov population models.

We present an adaptation of the Approximate Bayesian Computation method to estimate the satisfaction probability function of a temporal logic property for Markov Population Models. In this paper, we tackle the problem of estimating the satisfaction probability function of a temporal logic property w.r.t. a parametric Markovian model of Chemical Reaction Network. We want to assess the probability with which the trajectories generated by a parametric Markov Population Model (MPM) satisfy a logical formula over the whole parameter space. In the first step of the work, we formally define a distance between a trajectory of an MPM and a logical property. If the distance is 0, the trajectory satisfies the property. The larger the distance is, further the trajectory is from satisfying the property. In the second step, we adapt the Approximate Bayesian Computation method using the distance defined in the first step. This adaptation yields a new algorithm, called automaton-ABC, whose output is a density function that directly leads to the estimation of the desired satisfaction probability function. We apply our methodology to several examples and models, and we compare it to state-of-the-art techniques. We show that the sequential version of our algorithm relying on ABC-SMC leads to an efficient exploration of the parameter space with respect to the formula and gives good approximations of the satisfaction probability function at a reduced computational cost. • We develop the notion of satisfiability distance for the path of a Markov Population Model from an MITL property. • We detail how Linear Hybrid Automata computes such satisfiability distances. • We develop a new method called automaton-ABC that estimates the satisfaction probability function of a parametric MPM. • We test it on several models of biochemical networks to show the efficiency of the method. [ABSTRACT FROM AUTHOR]