{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T19:17:04Z","timestamp":1792264624095,"version":"4.4.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319919072","type":"print"},{"value":"9783319919089","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-319-91908-9_23","type":"book-chapter","created":{"date-parts":[[2019,10,4]],"date-time":"2019-10-04T05:05:00Z","timestamp":1570165500000},"page":"478-504","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":96,"title":["Statistical Model Checking"],"prefix":"10.1007","author":[{"given":"Axel","family":"Legay","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anna","family":"Lukina","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Louis Marie","family":"Traonouez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Junxing","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Radu","family":"Grosu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,10,5]]},"reference":[{"issue":"6","key":"23_CR1","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.R., 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":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-13464-7_4","volume-title":"Formal Techniques for Distributed Systems","author":"A Basu","year":"2010","unstructured":"Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. In: Hatcliff, J., Zucca, E. (eds.) FMOODS\/FORTE - 2010. LNCS, vol. 6117, pp. 32\u201346. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-13464-7_4"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-642-16612-9_25","volume-title":"Runtime Verification","author":"A Basu","year":"2010","unstructured":"Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A., Sifakis, E.: Verification of an AFDX infrastructure using simulations and probabilities. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 330\u2013344. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-16612-9_25"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-40196-1_12","volume-title":"Quantitative Evaluation of Systems","author":"B Boyer","year":"2013","unstructured":"Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: a flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160\u2013164. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-40196-1_12"},{"key":"23_CR5","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1007\/s11222-011-9231-6","volume":"22","author":"F C\u00e9rou","year":"2012","unstructured":"C\u00e9rou, F., Del Moral, P., Furon, T., Guyader, A.: Sequential Monte Carlo for rare event estimation. Stat. Comput 22, 795\u2013808 (2012)","journal-title":"Stat. Comput"},{"key":"23_CR6","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1080\/07362990601139628","volume":"25","author":"F C\u00e9rou","year":"2007","unstructured":"C\u00e9rou, F., Guyader, A.: Adaptive multilevel splitting for rare event analysis. Stoch. Anal. Appl. 25, 417\u2013443 (2007)","journal-title":"Stoch. Anal. Appl."},{"key":"23_CR7","unstructured":"Ciesinski, F., Baier, C.: Liquor: a tool for qualitative and quantitative linear time analysis of reactive systems. In: Proceedings of 3rd International Conference on Quantitative Evaluation of Systems (QEST), pp. 131\u2013132. IEEE (2006)"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-24611-4_5","volume-title":"Validation of Stochastic Systems","author":"F Ciesinski","year":"2004","unstructured":"Ciesinski, F., Gr\u00f6\u00dfer, M.: On probabilistic computation tree logic. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 147\u2013188. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24611-4_5"},{"issue":"4","key":"23_CR9","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-642-22110-1_27","volume-title":"Computer Aided Verification","author":"A David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349\u2013355. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22110-1_27"},{"key":"23_CR11","series-title":"Probability and Its Applications","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9393-1","volume-title":"Feynman-Kac Formulae: Genealogical and Interacting Particle Systems with Applications","author":"P Moral Del","year":"2004","unstructured":"Del Moral, P.: Feynman-Kac Formulae: Genealogical and Interacting Particle Systems with Applications. Probability and Its Applications. Springer, New York (2004). \n                      https:\/\/doi.org\/10.1007\/978-1-4684-9393-1"},{"key":"23_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3437-9","volume-title":"Sequential Monte Carlo Methods in Practice","author":"A Doucet","year":"2001","unstructured":"Doucet, A., de Freitas, N., Gordon, N.: Sequential Monte Carlo Methods in Practice. Springer, New York (2001). \n                      https:\/\/doi.org\/10.1007\/978-1-4757-3437-9"},{"issue":"3","key":"23_CR13","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/0005-1098(89)90002-2","volume":"25","author":"CE Garca","year":"1989","unstructured":"Garca, C.E., Prett, D.M., Morari, M.: Model predictive control: theory and practice - a survey. Automatica 25(3), 335\u2013348 (1989)","journal-title":"Automatica"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-70918-3_18","volume-title":"STACS 2007","author":"H Gimbert","year":"2007","unstructured":"Gimbert, H.: Pure stationary optimal strategies in Markov decision processes. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 200\u2013211. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-70918-3_18"},{"issue":"4","key":"23_CR15","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1287\/opre.47.4.585","volume":"47","author":"P Glasserman","year":"1999","unstructured":"Glasserman, P., Heidelberger, P., Shahabuddin, P., Zajic, T.: Multilevel splitting for estimating rare event probabilities. Oper. Res. 47(4), 585\u2013600 (1999)","journal-title":"Oper. Res."},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-31980-1_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Grosu","year":"2005","unstructured":"Grosu, R., Smolka, S.A.: Monte Carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 271\u2013286. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/978-3-540-31980-1_18"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-642-19829-8_10","volume-title":"Formal Methods: Foundations and Applications","author":"HLS Younes","year":"2011","unstructured":"Younes, H.L.S., Clarke, E.M., Zuliani, P.: Statistical verification of probabilistic properties with unbounded until. In: Davies, J., Silva, L., Simao, A. (eds.) SBMF 2010. LNCS, vol. 6527, pp. 144\u2013160. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-19829-8_10"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342\u2013356. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-46002-0_24"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-77966-7_9","volume-title":"Hardware and Software: Verification and Testing","author":"DN Jansen","year":"2008","unstructured":"Jansen, D.N., Katoen, J.-P., Oldenkamp, M., Stoelinga, M., Zapreev, I.: How fast and fat is your probabilistic model checker? An experimental performance comparison. In: Yorav, K. (ed.) HVC 2007. LNCS, vol. 4899, pp. 69\u201385. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-77966-7_9"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/978-3-642-39799-8_38","volume-title":"Computer Aided Verification","author":"C Jegourel","year":"2013","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 576\u2013591. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-39799-8_38"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-662-45231-8_11","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications","author":"C Jegourel","year":"2014","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: An effective heuristic for adaptive importance splitting in statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 143\u2013159. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-662-45231-8_11"},{"key":"23_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2016.08.009","volume":"649","author":"C J\u00e9gourel","year":"2016","unstructured":"J\u00e9gourel, C., Legay, A., Sedwards, S.: Command-based importance sampling for statistical model checking. Theoret. Comput. Sci. 649, 1\u201324 (2016)","journal-title":"Theoret. Comput. Sci."},{"key":"23_CR23","unstructured":"Kahn, H.: Stochastic (Monte Carlo) attenuation analysis. Technical report P-88, Rand Corporation, July 1949"},{"issue":"5","key":"23_CR24","first-page":"27","volume":"6","author":"H Kahn","year":"1950","unstructured":"Kahn, H.: Random sampling (Monte Carlo) techniques in neutron attenuation problems. Nucleonics 6(5), 27 (1950)","journal-title":"Nucleonics"},{"key":"23_CR25","unstructured":"Kahn, H., Harris, T.E.: Estimation of particle transmission by random sampling. In: Applied Mathematics. Series 12, vol. 5. National Bureau of Standards (1951)"},{"issue":"5","key":"23_CR26","first-page":"263","volume":"1","author":"H Kahn","year":"1953","unstructured":"Kahn, H., Marshall, A.W.: Methods of reducing sample size in Monte Carlo computations. Oper. Res. 1(5), 263\u2013278 (1953)","journal-title":"Oper. Res."},{"key":"23_CR27","unstructured":"Kennedy, J., Eberhart, R.: Particle swarm optimization. In: Proceedings of 1995 IEEE International Conference on Neural Networks, pp. 1942\u20131948 (1995)"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism 2.0: a tool for probabilistic model checking. In: QEST, pp. 322\u2013323. IEEE (2004)","DOI":"10.1109\/QEST.2004.1348048"},{"key":"23_CR29","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"23_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-662-54580-5_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Lukina","year":"2017","unstructured":"Lukina, A., Esterle, L., Hirsch, C., Bartocci, E., Yang, J., Tiwari, A., Smolka, S.A., Grosu, R.: ARES: adaptive receding-horizon synthesis of optimal plans. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 286\u2013302. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54580-5_17"},{"key":"23_CR31","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BF02883985","volume":"10","author":"M Okamoto","year":"1959","unstructured":"Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10, 29\u201335 (1959)","journal-title":"Ann. Inst. Stat. Math."},{"issue":"2","key":"23_CR32","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1063\/1.1741967","volume":"23","author":"MN Rosenbluth","year":"1955","unstructured":"Rosenbluth, M.N., Rosenbluth, A.W.: Monte Carlo calculation of the average extension of molecular chains. J. Chem. Phys. 23(2), 356\u2013359 (1955)","journal-title":"J. Chem. Phys."},{"key":"23_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"K Sen","year":"2004","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202\u2013215. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-27813-9_16"},{"key":"23_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"K Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266\u2013280. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11513988_26"},{"key":"23_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-319-68167-2_29","volume-title":"Automated Technology for Verification and Analysis","author":"A Tiwari","year":"2017","unstructured":"Tiwari, A., Smolka, S.A., Esterle, L., Lukina, A., Yang, J., Grosu, R.: Attacking the V: on the resiliency of adaptive-horizon MPC. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 446\u2013462. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-68167-2_29"},{"issue":"2","key":"23_CR36","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945)","journal-title":"Ann. Math. Stat."},{"key":"23_CR37","unstructured":"Yang, J., Grosu, R., Smolka, S.A., Tiwari, A.: Love thy neighbor: V-formation as a problem of model predictive control. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 59. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016)"},{"key":"23_CR38","unstructured":"Yang, J., Grosu, R., Smolka, S.A., Tiwari, A.: V-formation as optimal control. In: Proceedings of Biological Distributed Algorithms Workshop 2016 (2016)"},{"key":"23_CR39","unstructured":"Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon University (2005)"},{"key":"23_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/11609773_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"HLS Younes","year":"2005","unstructured":"Younes, H.L.S.: Error control for probabilistic model checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 142\u2013156. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11609773_10"},{"key":"23_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223\u2013235. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45657-0_17"},{"key":"23_CR42","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Baier, C., Clarke, E.M.: Rare-event verification for stochastic hybrid systems. In: Proceedings of 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2012, pp. 217\u2013226. ACM, New York (2012)","DOI":"10.1145\/2185632.2185665"}],"container-title":["Lecture Notes in Computer Science","Computing and Software Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91908-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,5]],"date-time":"2019-10-05T20:03:59Z","timestamp":1570305839000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91908-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783319919072","9783319919089"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91908-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}