Oxford logo
[BCKL16] L. Bortolussi, L. Cardelli, M. Kwiatkowska and L. Laurenti. Approximation of Probabilistic Reachability for Chemical Reaction Networks using the Linear Noise Approximation. In Proc. 13th International Conference on Quantitative Evaluation of SysTems (QEST 2016), Springer. To appear. 2016. [pdf] [bib]
Downloads:  pdf pdf (437 KB)  bib bib
Notes: The original publication is available at link.springer.com.
Abstract. We study time-bounded probabilistic reachability for Chemical Reaction Networks (CRNs) using the Linear Noise Approximation (LNA). The LNA approximates the discrete stochastic semantics of a CRN in terms of a continuous space Gaussian process. We consider reachability regions expressed as intersections of fi nitely many linear inequalities over the species of a CRN. This restriction allows us to derive an abstraction of the original Gaussian process as a time-inhomogeneous discrete-time Markov chain (DTMC), such that the dimensionality of its state space is independent of the number of species of the CRN, ameliorating the state space explosion problem. We formulate an algorithm for approximate computation of time-bounded reachability probabilities on the resulting DTMC and show how to extend it to more complex temporal properties. We implement the algorithm and demonstrate on two case studies that it permits fast and scalable computation of reachability properties with controlled accuracy.