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 finitely 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.
This research is supported by a Royal Society Research Professorship and ERC AdG VERIWARE. LB is supported by EU-FET project QUANTICOL (nr 600708).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The Gaussian process obtained by linear noise approximation is Markov, as it is the solution of a linear Fokker-Planck equation (stochastic differential equation) [25].
References
Anderson, D.F., Kurtz, T.G.: Continuous time Markov chain models for chemical reaction networks. In: Koeppl, H., Setti, G., di Bernardo, M., Densmore, D. (eds.) Design and Analysis of Biomolecular Circuits, pp. 3–42. Springer, New York (2011)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic (TOCL) 1(1), 162–170 (2000)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Software Eng. 29(6), 524–541 (2003)
Billingsley, P.: Convergence of probability measures. Wiley, Hoboken (1999)
Bortolussi, L., Hillston, J.: Fluid model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 333–347. Springer, Heidelberg (2012)
Bortolussi, L., Lanciani, R.: Model checking Markov population models by central limit approximation. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 123–138. Springer, Heidelberg (2013)
Bortolussi, L., Lanciani, R.: Stochastic approximation of global reachability probabilities of Markov population models. In: Horváth, A., Wolter, K. (eds.) EPEW 2014. LNCS, vol. 8721, pp. 224–239. Springer, Heidelberg (2014)
Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous-time Markov chains. Information and Computation (2016)
Bujorianu, L.M.: Stochastic Reachability Analysis of Hybrid Systems. Springer, London (2012)
Cardelli, L.: On process rate semantics. Theoret. Comput. Sci. 391(3), 190–215 (2008)
Cardelli, L., Kwiatkowska, M., Laurenti, L.: Stochastic analysis of chemical reaction networks using linear noise approximation. In: Roux, O., Bourdon, J. (eds.) CMSB 2015. LNCS, vol. 9308, pp. 64–76. Springer, Heidelberg (2015)
Csikász-Nagy, A., Cardelli, L., Soyer, O.S.: Response dynamics of phosphorelays suggest their potential utility in cell signalling. J. R. Soc. Interface 8(57), 480–488 (2011)
Eldar, A., Elowitz, M.B.: Functional roles for noise in genetic circuits. Nature 467(7312), 167–173 (2010)
Ethier, S.N., Kurtz, T.G.: Markov Processes: Characterization and Convergence, vol. 282. Wiley, New York (2009)
Fedoroff, N., Fontana, W.: Small numbers of big molecules. Science 297(5584), 1129–1131 (2002)
Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81(25), 2340–2361 (1977)
Gillespie, D.T.: A rigorous derivation of the chemical master equation. Phys. A Stat. Mech. Appl. 188(1), 404–425 (1992)
Gillespie, D.T.: The chemical Langevin equation. J. Chem. Phys. 113(1), 297–306 (2000)
Grima, R.: Linear-noise approximation and the chemical master equation agree up to second-order moments for a class of chemical systems. Phys. Rev. E 92(4), 042–124 (2015)
Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Munsky, B., Khammash, M.: The finite state projection algorithm for the solution of the chemical master equation. J. Chem. Phys. 124(4), 044–104 (2006)
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science 1977, pp. 46–57. IEEE (1977)
Van Kampen, N.G.: Stochastic Processes in Physics and Chemistry, vol. 1. Elsevier, Amsterdam (1992)
Wallace, E., Gillespie, D., Sanft, K., Petzold, L.: Linear noise approximation is valid over limited times for any chemical system that is sufficiently large. IET Syst. Biol. 6(4), 102–115 (2012)
Wolf, V., Goel, R., Mateescu, M., Henzinger, T.A.: Solving the chemical master equation using sliding windows. BMC Syst. Biol. 4(1), 1 (2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Bortolussi, L., Cardelli, L., Kwiatkowska, M., Laurenti, L. (2016). Approximation of Probabilistic Reachability for Chemical Reaction Networks Using the Linear Noise Approximation. In: Agha, G., Van Houdt, B. (eds) Quantitative Evaluation of Systems. QEST 2016. Lecture Notes in Computer Science(), vol 9826. Springer, Cham. https://doi.org/10.1007/978-3-319-43425-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-43425-4_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-43424-7
Online ISBN: 978-3-319-43425-4
eBook Packages: Computer ScienceComputer Science (R0)