{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:30:31Z","timestamp":1750221031928,"version":"3.41.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2019,7,16]],"date-time":"2019-07-16T00:00:00Z","timestamp":1563235200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"EU-FET project QUANTICOL","award":["600708"],"award-info":[{"award-number":["600708"]}]},{"name":"Royal Society Research Professorship"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3331452","type":"journal-article","created":{"date-parts":[[2019,7,16]],"date-time":"2019-07-16T12:39:01Z","timestamp":1563280741000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Central Limit Model Checking"],"prefix":"10.1145","volume":"20","author":[{"given":"Luca","family":"Bortolussi","sequence":"first","affiliation":[{"name":"Department of Mathematics and Geosciences, University of Trieste, Trieste, Italy"}]},{"given":"Luca","family":"Cardelli","sequence":"additional","affiliation":[{"name":"Microsoft Research 8 University of Oxford, Cambridge, United Kingdom"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}]},{"given":"Luca","family":"Laurenti","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2019,7,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.16.624-641"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Robert J. Adler. 2010. The Geometry of Random Fields. SIAM.  Robert J. Adler. 2010. The Geometry of Random Fields. SIAM.","DOI":"10.1137\/1.9780898718980"},{"volume-title":"{n.d.}. Stochastic Analysis of Biochemical Systems","author":"Anderson David F.","key":"e_1_2_1_3_1","unstructured":"David F. Anderson and Thomas G. Kurtz . {n.d.}. Stochastic Analysis of Biochemical Systems . Springer . David F. Anderson and Thomas G. Kurtz. {n.d.}. Stochastic Analysis of Biochemical Systems. Springer."},{"key":"e_1_2_1_4_1","volume-title":"Kurtz","author":"Anderson David F.","year":"2011","unstructured":"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. 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."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-008-0059-z"},{"volume-title":"Computer Aided Verification","author":"Aziz Adnan","key":"e_1_2_1_6_1","unstructured":"Adnan Aziz , Kumud Sanwal , Vigyan Singhal , and Robert Brayton . 1996. Verifying continuous time Markov chains . In Computer Aided Verification . Springer , 269--276. Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert Brayton. 1996. Verifying continuous time Markov chains. In Computer Aided Verification. Springer, 269--276."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.733948"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_10_1","unstructured":"Christel Baier Joost-Pieter Katoen etal 2008. Principles of Model Checking. Vol. 26202649. MIT Press Cambridge MA.  Christel Baier Joost-Pieter Katoen et al. 2008. Principles of Model Checking. Vol. 26202649. MIT Press Cambridge MA."},{"key":"e_1_2_1_11_1","volume-title":"Bertsekas and Steven Shreve","author":"Dimitir","year":"2004","unstructured":"Dimitir P. Bertsekas and Steven Shreve . 2004 . Stochastic Optimal Control: The Discrete-time Case . Dimitir P. Bertsekas and Steven Shreve. 2004. Stochastic Optimal Control: The Discrete-time Case."},{"volume-title":"Convergence of Probability Measures","author":"Billingsley Patrick","key":"e_1_2_1_12_1","unstructured":"Patrick Billingsley . 2013. Convergence of Probability Measures . John Wiley 8 Sons. Patrick Billingsley. 2013. Convergence of Probability Measures. John Wiley 8 Sons."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.12.001"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43425-4_5"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_24"},{"key":"e_1_2_1_16_1","volume-title":"Efficient checking of individual rewards properties in Markov population models. arXiv preprint arXiv:1509.08561","author":"Bortolussi Luca","year":"2015","unstructured":"Luca Bortolussi and Jane Hillston . 2015. Efficient checking of individual rewards properties in Markov population models. arXiv preprint arXiv:1509.08561 ( 2015 ). Luca Bortolussi and Jane Hillston. 2015. Efficient checking of individual rewards properties in Markov population models. arXiv preprint arXiv:1509.08561 (2015)."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.01.001"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40196-1_9"},{"volume-title":"Computer Performance Engineering","author":"Bortolussi Luca","key":"e_1_2_1_19_1","unstructured":"Luca Bortolussi and Roberta Lanciani . 2014. Stochastic approximation of global reachability probabilities of Markov population models . In Computer Performance Engineering . Springer , 224--239. Luca Bortolussi and Roberta Lanciani. 2014. Stochastic approximation of global reachability probabilities of Markov population models. In Computer Performance Engineering. Springer, 224--239."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.01.004"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_20"},{"key":"e_1_2_1_22_1","first-page":"656","article-title":"The cell cycle switch computes approximate majority. Sci","volume":"2","author":"Cardelli Luca","year":"2012","unstructured":"Luca Cardelli and Attila Csik\u00e1sz-Nagy . 2012 . The cell cycle switch computes approximate majority. Sci . Rep. 2 (2012), 656 . Luca Cardelli and Attila Csik\u00e1sz-Nagy. 2012. The cell cycle switch computes approximate majority. Sci. Rep. 2 (2012), 656.","journal-title":"Rep."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.biosystems.2016.09.004"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45177-0_10"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11047-017-9667-5"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04761-9_10"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.02.037"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2688907"},{"key":"e_1_2_1_29_1","volume-title":"Kurtz","author":"Ethier Stewart N.","year":"2009","unstructured":"Stewart N. Ethier and Thomas G . Kurtz . 2009 . Markov Processes : Characterization and Convergence, Vol. 282 . John Wiley 8 Sons. Stewart N. Ethier and Thomas G. Kurtz. 2009. Markov Processes: Characterization and Convergence, Vol. 282. John Wiley 8 Sons."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3084454"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1021\/j100540a008"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0378-4371(92)90283-V"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevE.92.042124"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00285-013-0711-5"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.11.013"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1839764.1839772"},{"volume-title":"A Compositional Approach to Performance Modelling","author":"Hillston Jane","key":"e_1_2_1_37_1","unstructured":"Jane Hillston . 2005. A Compositional Approach to Performance Modelling . Vol. 12 . Cambridge University Press . Jane Hillston. 2005. A Compositional Approach to Performance Modelling. Vol. 12. Cambridge University Press."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"S. Krantz and P. R. Harold. 2002. A Primer of Real Analytic Functions (2nd ed.). Birk\u00e1\u00ffauser.  S. Krantz and P. R. Harold. 2002. A Primer of Real Analytic Functions (2nd ed.). Birk\u00e1\u00ffauser.","DOI":"10.1007\/978-0-8176-8134-0"},{"volume-title":"Formal Methods for Performance Evaluation","author":"Kwiatkowska Marta","key":"e_1_2_1_40_1","unstructured":"Marta Kwiatkowska , Gethin Norman , and David Parker . 2007. Stochastic model checking . In Formal Methods for Performance Evaluation . Springer , 220--270. Marta Kwiatkowska, Gethin Norman, and David Parker. 2007. Stochastic model checking. In Formal Methods for Performance Evaluation. Springer, 220--270."},{"volume-title":"Computer Aided Verification","author":"Kwiatkowska Marta","key":"e_1_2_1_41_1","unstructured":"Marta Kwiatkowska , Gethin Norman , and David Parker . 2011. PRISM 4.0 : Verification of probabilistic real-time systems . In Computer Aided Verification . Springer , 585--591. Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Computer Aided Verification. Springer, 585--591."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3049797.3049812"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.bpj.2018.05.009"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01843554"},{"volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"Maler Oded","key":"e_1_2_1_45_1","unstructured":"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. 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."},{"key":"e_1_2_1_46_1","volume-title":"Probabilistic model checking for continuous time Markov chains via sequential bayesian inference. arXiv preprint arXiv:1711.01863","author":"Milios Dimitrios","year":"2017","unstructured":"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 ). 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)."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.2145882"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"volume-title":"Integrals and Martingales","author":"Schilling Ren\u00e9 L.","key":"e_1_2_1_50_1","unstructured":"Ren\u00e9 L. Schilling . 2017. Measures , Integrals and Martingales . Cambridge University Press . Ren\u00e9 L. Schilling. 2017. Measures, Integrals and Martingales. Cambridge University Press."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.119.210601"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.0803850105"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.151588598"},{"volume-title":"Stochastic Processes in Physics and Chemistry","author":"Van Kampen Nicolaas Godfried","key":"e_1_2_1_54_1","unstructured":"Nicolaas Godfried Van Kampen . 1992. Stochastic Processes in Physics and Chemistry . Vol. 1 . Elsevier . Nicolaas Godfried Van Kampen. 1992. Stochastic Processes in Physics and Chemistry. Vol. 1. Elsevier."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1049\/iet-syb.2011.0038"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1186\/1752-0509-4-42"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331452","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3331452","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:29Z","timestamp":1750207409000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331452"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,16]]},"references-count":56,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3331452"],"URL":"https:\/\/doi.org\/10.1145\/3331452","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2019,7,16]]},"assertion":[{"value":"2018-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}