Central Limit Model Checking

Abstract

We consider probabilistic model checking for continuous-time Markov chains (CTMCs) induced from Stochastic Reaction Networks against a fragment of Continuous Stochastic Logic (CSL) extended with reward operators. Classical numerical algorithms for CSL model checking based on uniformisation are limited to finite CTMCs and suffer from exponential growth of the state space with respect to the number of species. However, approximate techniques such as mean-field approximations and simulations combined with statistical inference are more scalable but can be time-consuming and do not support the full expressiveness of CSL. In this article, we employ a continuous-space approximation of the CTMC in terms of a Gaussian process based on the Central Limit Approximation, also known as the Linear Noise Approximation, whose solution requires solving a number of differential equations that is quadratic in the number of species and independent of the population size. We then develop efficient and scalable approximate model checking algorithms on the resulting Gaussian process, where we restrict the target regions for probabilistic reachability to convex polytopes. This allows us to derive an abstraction in terms of a time-inhomogeneous discrete-time Markov chain (DTMC), whose dimension is independent of the number of species, on which model checking is performed. Using results from probability theory, we prove the convergence in distribution of our algorithms to the corresponding measures on the original CTMC. We implement the techniques and, on a set of examples, demonstrate that they allow us to overcome the state space explosion problem, while still correctly characterizing the stochastic behaviour of the system. Our methods can be used for formal analysis of a wide range of distributed stochastic systems, including biochemical systems, sensor networks, and population protocols.

References

1. Alessandro Abate, Joost-Pieter Katoen, John Lygeros, and Maria Prandini. 2010. Approximate model checking of stochastic hybrid systems. Eur. J. Contr. 16, 6 (2010), 624--641.
2. Robert J. Adler. 2010. The Geometry of Random Fields. SIAM.
3. David F. Anderson and Thomas G. Kurtz. {n.d.}. Stochastic Analysis of Biochemical Systems. Springer.
4. David F. Anderson and Thomas G. Kurtz. 2011. Continuous time Markov chain models for chemical reaction networks. In Design and Analysis of Biomolecular Circuits. Springer, 3--42.
5. Dana Angluin, James Aspnes, and David Eisenstat. 2008. A simple population protocol for fast robust approximate majority. Distrib. Comput. 21, 2 (2008), 87--102.
6. Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert Brayton. 1996. Verifying continuous time Markov chains. In Computer Aided Verification. Springer, 269--276.
7. Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert Brayton. 2000. Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic 1, 1 (2000), 162--170.
8. Christel Baier, Boudewijn Haverkort, Holger Hermanns, and Joost-Pieter Katoen. 2000. Model checking continuous-time Markov chains by transient analysis. In Proceedings of the International Conference on Computer Aided Verification. Springer, 358--372.
9. Christel Baier, Boudewijn Haverkort, Holger Hermanns, and Joost-Pieter Katoen. 2003. Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29, 6 (2003), 524--541.
10. Christel Baier, Joost-Pieter Katoen, et al. 2008. Principles of Model Checking. Vol. 26202649. MIT Press, Cambridge, MA.
11. Dimitir P. Bertsekas and Steven Shreve. 2004. Stochastic Optimal Control: The Discrete-time Case.
12. Patrick Billingsley. 2013. Convergence of Probability Measures. John Wiley 8 Sons.
13. Luca Bortolussi. 2016. Hybrid behaviour of Markov population models. Inf. Comput. 247 (2016), 37--86.
14. Luca Bortolussi, Luca Cardelli, Marta Kwiatkowska, and Luca Laurenti. 2016. Approximation of probabilistic reachability for chemical reaction networks using the linear noise approximation. In Proceedings of the International Conference on Quantitative Evaluation of Systems. Springer, 72--88.
15. Luca Bortolussi and Jane Hillston. 2012. Fluid model checking. In Proceedings of the International Conference on Concurrency Theory (CONCUR’12). Springer, 333--347.
16. Luca Bortolussi and Jane Hillston. 2015. Efficient checking of individual rewards properties in Markov population models. arXiv preprint arXiv:1509.08561 (2015).
17. Luca Bortolussi, Jane Hillston, Diego Latella, and Mieke Massink. 2013. Continuous approximation of collective system behaviour: A tutorial. Perf. Eval. 70, 5 (2013), 317--349.
18. Luca Bortolussi and Roberta Lanciani. 2013. Model checking Markov population models by central limit approximation. In Quantitative Evaluation of Systems. Springer, 123--138.
19. Luca Bortolussi and Roberta Lanciani. 2014. Stochastic approximation of global reachability probabilities of Markov population models. In Computer Performance Engineering. Springer, 224--239.
20. Luca Bortolussi, Dimitrios Milios, and Guido Sanguinetti. 2016. Smoothed model checking for uncertain continuous-time Markov chains. Information and Computation 247 (2016), 235--253.
21. Luca Cardelli, Milan Češka, Martin Fränzle, Marta Kwiatkowska, Luca Laurenti, Nicola Paoletti, and Max Whitby. 2017. Syntax-guided optimal synthesis for chemical reaction networks. In Proceedings of the International Conference on Computer Aided Verification. Springer, 375--395.
22. Luca Cardelli and Attila Csikász-Nagy. 2012. The cell cycle switch computes approximate majority. Sci. Rep. 2 (2012), 656.
23. Luca Cardelli, Marta Kwiatkowska, and Luca Laurenti. 2016. Stochastic analysis of chemical reaction networks using linear noise approximation. Biosystems 149 (2016), 26--33.
24. Luca Cardelli, Marta Kwiatkowska, and Luca Laurenti. 2016. A stochastic hybrid approximation for chemical kinetics based on the linear noise approximation. In Proceedings of the International Conference on Computational Methods in Systems Biology. Springer, 147--167.
25. Luca Cardelli, Marta Kwiatkowska, and Luca Laurenti. 2018. Programming discrete distributions with chemical reaction networks. Nat. Comput. 17, 1 (2018), 131--145.
26. Taolue Chen, Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre. 2009. LTL model checking of time-inhomogeneous Markov chains. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis. Springer, 104--119.
27. Federica Ciocchetta and Jane Hillston. 2009. Bio-PEPA: A framework for the modelling and analysis of biological systems. Theor. Comput. Sci. 410, 33--34 (2009), 3065--3084.
28. Frits Dannenberg, Ernst Moritz Hahn, and Marta Kwiatkowska. 2015. Computing cumulative rewards using fast adaptive uniformization. ACM Trans. Model. Comput. Simul. 25, 2, Article 9 (Feb. 2015), 23 pages.
29. Stewart N. Ethier and Thomas G. Kurtz. 2009. Markov Processes: Characterization and Convergence, Vol. 282. John Wiley 8 Sons.
30. N. Gast. 2017. Expected values estimated via mean-field approximation are 1/N-accurate. Proc. ACM Meas. Anal. Comput. Syst. 1, 1 (2017), 17:1--17:26.
31. Daniel T. Gillespie. 1977. Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81, 25 (1977), 2340--2361.
32. Daniel T. Gillespie. 1992. A rigorous derivation of the chemical master equation. Physica A 188, 1 (1992), 404--425.
33. Ramon Grima. 2015. 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 (2015), 042124.
34. J. Hasenauer, V. Wolf, A. Kazeroonian, and F. J. Theis. 2014. Method of conditional moments (MCM) for the chemical master equation. J. Math. Biol. 69, 3 (2014), 687--735.
35. John Heath, Marta Kwiatkowska, Gethin Norman, David Parker, and Oksana Tymchyshyn. 2008. Probabilistic model checking of complex biological pathways. Theor. Comput. Sci. 391, 3 (2008), 239--257.
36. Thomas A. Henzinger, Linar Mikeev, Maria Mateescu, and Verena Wolf. 2010. Hybrid numerical solution of the chemical master equation. In Proceedings of the 8th International Conference on Computational Methods in Systems Biology. ACM, 55--65.
37. Jane Hillston. 2005. A Compositional Approach to Performance Modelling. Vol. 12. Cambridge University Press.
38. Richard M. Karp and Raymond E. Miller. 1969. Parallel program schemata. J. Comput. Syst. Sci. 3, 2 (1969), 147--195.
39. S. Krantz and P. R. Harold. 2002. A Primer of Real Analytic Functions (2nd ed.). Birkáÿauser.
40. Marta Kwiatkowska, Gethin Norman, and David Parker. 2007. Stochastic model checking. In Formal Methods for Performance Evaluation. Springer, 220--270.
41. Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Computer Aided Verification. Springer, 585--591.
42. Luca Laurenti, Alessandro Abate, Luca Bortolussi, Luca Cardelli, Milan Ceska, and Marta Kwiatkowska. 2017. Reachability computation for switching diffusions: Finite abstractions with certifiable and tuneable precision. In Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control. ACM, 55--64.
43. Luca Laurenti, Attila Csikasz-Nagy, Marta Kwiatkowska, and Luca Cardelli. 2018. Molecular filters for noise reduction. Biophys. J. 114, 12 (2018), 3000--3011.
44. M. A. Lifshits. 1984. Absolute continuity of functionals of “supremum” type for Gaussian processes. J. Math. Sci. 27, 5 (1984), 3103--3112.
45. Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 152--166.
46. Dimitrios Milios, Guido Sanguinetti, and David Schnoerr. 2017. Probabilistic model checking for continuous time Markov chains via sequential bayesian inference. arXiv preprint arXiv:1711.01863 (2017).
47. Brian Munsky and Mustafa Khammash. 2006. The finite state projection algorithm for the solution of the chemical master equation. J. Chem. Phys. 124, 4 (2006), 044104.
48. Tadao Murata. 1989. Petri nets: Properties, analysis and applications. Proc. IEEE 77, 4 (1989), 541--580.
49. Amir Pnueli. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science 1977. IEEE, 46--57.
50. René L. Schilling. 2017. Measures, Integrals and Martingales. Cambridge University Press.
51. David Schnoerr, Botond Cseke, Ramon Grima, and Guido Sanguinetti. 2017. Efficient low-order approximation of first-passage time distributions. Phys. Rev. Lett. 119, 21 (2017), 210601.
52. Vahid Shahrezaei and Peter S. Swain. 2008. Analytical distributions for stochastic gene expression. Proc. Natl. Acad. Sci. U.S.A. 105, 45 (2008), 17256--17261.
53. Mukund Thattai and Alexander Van Oudenaarden. 2001. Intrinsic noise in gene regulatory networks. Proc. Natl Acad. Sci. U.S.A. 98, 15 (2001), 8614--8619.
54. Nicolaas Godfried Van Kampen. 1992. Stochastic Processes in Physics and Chemistry. Vol. 1. Elsevier.
55. E. W. J. Wallace, D. T. Gillespie, K. R. Sanft, and L. R. Petzold. 2012. Linear noise approximation is valid over limited times for any chemical system that is sufficiently large. IET Syst. Biol. 6, 4 (2012), 102--115.
56. Verena Wolf, Rushil Goel, Maria Mateescu, and Thomas A. Henzinger. 2010. Solving the chemical master equation using sliding windows. BMC Syst. Biol. 4, 1 (2010), 1.

Index Terms

• Mathematics of computing

  • Probability and statistics

• Theory of computation

  • Logic

    • Logic and verification