{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T20:48:11Z","timestamp":1757450891551,"version":"3.41.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319991535"},{"type":"electronic","value":"9783319991542"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99154-2_18","type":"book-chapter","created":{"date-parts":[[2018,8,14]],"date-time":"2018-08-14T18:14:35Z","timestamp":1534270475000},"page":"289-305","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference"],"prefix":"10.1007","author":[{"given":"Dimitrios","family":"Milios","sequence":"first","affiliation":[]},{"given":"Guido","family":"Sanguinetti","sequence":"additional","affiliation":[]},{"given":"David","family":"Schnoerr","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,15]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Computer Aided Verification","author":"A Aziz","year":"1996","unstructured":"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\u2013276. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_75"},{"issue":"1","key":"18_CR2","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic 1(1), 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Logic"},{"issue":"6","key":"18_CR3","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1049\/iet-syb.2011.0013","volume":"5","author":"P Azunre","year":"2011","unstructured":"Azunre, P., Gomez-Uribe, C., Verghese, G.: Mass fluctuation kinetics: analysis and computation of equilibria and local dynamics. IET Syst. Biol. 5(6), 325\u2013335 (2011)","journal-title":"IET Syst. Biol."},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/10722167_28","volume-title":"Computer Aided Verification","author":"C Baier","year":"2000","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model checking continuous-time Markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 358\u2013372. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_28"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-45798-4_12","volume-title":"Performance Evaluation of Complex Systems: Techniques and Tools","author":"C Baier","year":"2002","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Automated performance and dependability evaluation using model checking. In: Calzarossa, M.C., Tucci, S. (eds.) Performance 2002. LNCS, vol. 2459, pp. 261\u2013289. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45798-4_12"},{"issue":"6","key":"18_CR6","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: Proceedings of QEST 2006, pp. 125\u2013126. IEEE Computer Society (2006)","DOI":"10.1109\/QEST.2006.59"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-319-43425-4_5","volume-title":"Quantitative Evaluation of Systems","author":"L Bortolussi","year":"2016","unstructured":"Bortolussi, L., Cardelli, L., Kwiatkowska, M., Laurenti, L.: Approximation of probabilistic reachability for chemical reaction networks using the linear noise approximation. In: Agha, G., Van Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 72\u201388. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43425-4_5"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-32940-1_24","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"L Bortolussi","year":"2012","unstructured":"Bortolussi, L., Hillston, J.: Fluid model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 333\u2013347. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_24"},{"issue":"C","key":"18_CR10","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.ic.2015.03.002","volume":"242","author":"L Bortolussi","year":"2015","unstructured":"Bortolussi, L., Hillston, J.: Model checking single agent behaviours by fluid approximation. Inf. Comput. 242(C), 183\u2013226 (2015)","journal-title":"Inf. Comput."},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-40196-1_9","volume-title":"Quantitative Evaluation of Systems","author":"L Bortolussi","year":"2013","unstructured":"Bortolussi, L., Lanciani, R.: Model checking Markov population models by central limit approximation. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 123\u2013138. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40196-1_9"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-319-10885-8_16","volume-title":"Computer Performance Engineering","author":"L Bortolussi","year":"2014","unstructured":"Bortolussi, L., Lanciani, R.: Stochastic approximation of global reachability probabilities of Markov population models. In: Horv\u00e1th, A., Wolter, K. (eds.) EPEW 2014. LNCS, vol. 8721, pp. 224\u2013239. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10885-8_16"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Lanciani, R., Nenzi, L.: Model checking Markov population models by stochastic approximations. CoRR, abs\/1711.03826 (2017)","DOI":"10.1016\/j.ic.2018.09.004"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/j.ic.2016.01.004","volume":"247","author":"L Bortolussi","year":"2016","unstructured":"Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous time Markov chains. Inform. Comput. 247, 235\u2013253 (2016)","journal-title":"Inform. Comput."},{"key":"18_CR15","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1109\/TSE.2012.1","volume":"39","author":"JT Bradley","year":"2013","unstructured":"Bradley, J.T., Hayden, R.A., Clark, A.: Performance specification and evaluation with unified stochastic probes and fluid analysis. IEEE Trans. Softw. Eng. 39, 97\u2013118 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"18_CR16","unstructured":"Cseke, B., Opper, M., Sanguinetti, G.: Approximate inference in latent Gaussian-Markov models from continuous time observations. In: Proceedings of NIPS, pp. 971\u2013979. Curran Associates Inc. (2013)"},{"issue":"49","key":"18_CR17","doi-asserted-by":"publisher","first-page":"494002","DOI":"10.1088\/1751-8113\/49\/49\/494002","volume":"49","author":"B Cseke","year":"2016","unstructured":"Cseke, B., Schnoerr, D., Opper, M., Sanguinetti, G.: Expectation propagation for continuous-time stochastic processes. J. Phys. A-Math. Theor. 49(49), 494002 (2016)","journal-title":"J. Phys. A-Math. Theor."},{"key":"18_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-3615-7","volume-title":"Essentials of Stochastic Processes","author":"R Durrett","year":"2012","unstructured":"Durrett, R.: Essentials of Stochastic Processes. Springer, New York (2012)"},{"issue":"4","key":"18_CR19","doi-asserted-by":"publisher","first-page":"26:1","DOI":"10.1145\/2883608","volume":"26","author":"C Feng","year":"2016","unstructured":"Feng, C., Hillston, J., Galpin, V.: Automatic moment-closure approximation of spatially distributed collective adaptive systems. ACM Trans. Model. Comput. Simul. 26(4), 26:1\u201326:22 (2016)","journal-title":"ACM Trans. Model. Comput. Simul."},{"key":"18_CR20","volume-title":"Handbook of Stochastic Methods","author":"CW Gardiner","year":"1985","unstructured":"Gardiner, C.W.: Handbook of Stochastic Methods, vol. 3. Springer, Berlin (1985)"},{"issue":"2","key":"18_CR21","doi-asserted-by":"publisher","first-page":"212","DOI":"10.2307\/3001852","volume":"9","author":"LA Goodman","year":"1953","unstructured":"Goodman, L.A.: Population growth of the sexes. Biometrics 9(2), 212\u2013225 (1953)","journal-title":"Biometrics"},{"issue":"5","key":"18_CR22","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512\u2013535 (1994)","journal-title":"Form. Asp. Comput."},{"issue":"15","key":"18_CR23","doi-asserted-by":"publisher","first-page":"6959","DOI":"10.1063\/1.1505860","volume":"117","author":"EL Haseltine","year":"2002","unstructured":"Haseltine, E.L., Rawlings, J.B.: Approximate simulation of coupled fast and slow reactions for stochastic chemical kinetics. J. Chem. Phys. 117(15), 6959 (2002)","journal-title":"J. Chem. Phys."},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Hayden, R.A., Stefanek, A., Bradley, J.T.: Fluid computation of passage-time distributions in large Markov models. In: Proceedings of QAPL, vol. 413, pp. 106\u2013141 (2012)","DOI":"10.1016\/j.tcs.2011.07.017"},{"key":"18_CR25","unstructured":"Hespanha, J.P.: StochDynTools \u2013 a MATLAB toolbox to compute moment dynamics for stochastic networks of bio-chemical reactions"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P., Khattri, M., Zapreevt, I.S.: A Markov reward model checker. In: Proceedings of QEST, pp. 243\u2013244. IEEE Computer Society (2005)","DOI":"10.1109\/QEST.2005.2"},{"issue":"3","key":"18_CR27","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1093\/bioinformatics\/18.3.470","volume":"18","author":"AM Kierzek","year":"2002","unstructured":"Kierzek, A.M.: STOCKS: STOChastic Kinetic Simulations of biochemical systems with Gillespie algorithm. Bioinformatics 18(3), 470\u2013481 (2002)","journal-title":"Bioinformatics"},{"key":"18_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"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\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"18_CR29","volume-title":"Stochastic Models, Estimation, and Control","author":"PS Maybeck","year":"1982","unstructured":"Maybeck, P.S.: Stochastic Models, Estimation, and Control. Academic Press, New York (1982)"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Milios, D., Sanguinetti, G., Schnoerr, D.: Probabilistic model checking for continuous-time Markov chains via sequential Bayesian inference. CoRR ArXiv, abs\/1711.01863v2 (2018)","DOI":"10.1007\/978-3-319-99154-2_18"},{"key":"18_CR31","unstructured":"Minka, T.P.: A family of algorithms for approximate Bayesian inference. Ph.D. thesis, MIT (2001)"},{"key":"18_CR32","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810633","volume-title":"Markov Chains","author":"JR Norris","year":"1997","unstructured":"Norris, J.R.: Markov Chains. Cambridge University Press, Cambridge (1997)"},{"key":"18_CR33","doi-asserted-by":"publisher","first-page":"210601","DOI":"10.1103\/PhysRevLett.119.210601","volume":"119","author":"D Schnoerr","year":"2017","unstructured":"Schnoerr, D., Cseke, B., Grima, R., Sanguinetti, G.: Efficient low-order approximation of first-passage time distributions. Phys. Rev. Lett. 119, 210601 (2017)","journal-title":"Phys. Rev. Lett."},{"issue":"8","key":"18_CR34","doi-asserted-by":"publisher","first-page":"08B616\\_1","DOI":"10.1063\/1.4892838","volume":"141","author":"D Schnoerr","year":"2014","unstructured":"Schnoerr, D., Sanguinetti, G., Grima, R.: Validity conditions for moment closure approximations in stochastic chemical kinetics. J. Chem. Phys. 141(8), 08B616\\_1 (2014)","journal-title":"J. Chem. Phys."},{"issue":"18","key":"18_CR35","doi-asserted-by":"publisher","first-page":"11B610\\_1","DOI":"10.1063\/1.4934990","volume":"143","author":"D Schnoerr","year":"2015","unstructured":"Schnoerr, D., Sanguinetti, G., Grima, R.: Comparison of different moment-closure approximations for stochastic chemical kinetics. J. Chem. Phys. 143(18), 11B610\\_1 (2015)","journal-title":"J. Chem. Phys."},{"issue":"9","key":"18_CR36","doi-asserted-by":"publisher","first-page":"093001","DOI":"10.1088\/1751-8121\/aa54d9","volume":"50","author":"D Schnoerr","year":"2017","unstructured":"Schnoerr, D., Sanguinetti, G., Grima, R.: Approximation and inference methods for stochastic biochemical kinetics - a tutorial review. J. Phys. A 50(9), 093001 (2017)","journal-title":"J. Phys. A"},{"issue":"9","key":"18_CR37","doi-asserted-by":"publisher","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"HL Younes","year":"2006","unstructured":"Younes, H.L., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368\u20131409 (2006)","journal-title":"Inf. Comput."},{"key":"18_CR38","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Simulink\/Stateflow verification. In: Proceedings of HSCC, pp. 243\u2013252. ACM (2010)","DOI":"10.21236\/ADA531406"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99154-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T10:15:34Z","timestamp":1751796934000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99154-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319991535","9783319991542"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99154-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}