{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:42:46Z","timestamp":1746006166412},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496732"},{"type":"electronic","value":"9783662496749"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_7","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"112-129","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Faster Statistical Model Checking for Unbounded Temporal Properties"],"prefix":"10.1007","author":[{"given":"Przemys\u0142aw","family":"Daca","sequence":"first","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]},{"given":"Tatjana","family":"Petrov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"7_CR1","unstructured":"Tool for the paper. \n                      http:\/\/pub.ist.ac.at\/~przemek\/pa_tool.html"},{"key":"7_CR2","unstructured":"Daca, P., Henzinger, T.A., Kret\u00ednsk\u00fd, J., Petrov, T.: Faster statistical model checking for unbounded temporal properties. In: CoRR, abs\/1504.05739 (2015)"},{"key":"7_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmel\u00edk, M., Forejt, V., K\u0159et\u00ednsk\u00fd, J., Kwiatkowska, M., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Heidelberg (2014)"},{"key":"7_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.4204\/EPTCS.85.1","volume":"85","author":"Peter Bulychev","year":"2012","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Poulsen, D.B., Legay, A., Wang, Z.: UPPAAL-SMC: statistical model checking for priced timed automata. In: QAPL, pp. 1\u201316 (2012)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-642-28729-9_18","volume-title":"Foundations of Software Science and Computational Structures","author":"K Chatterjee","year":"2012","unstructured":"Chatterjee, K.: Robustness of structurally equivalent concurrent parity games. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 270\u2013285. Springer, Heidelberg (2012)"},{"issue":"4","key":"7_CR7","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT 17(4), 397\u2013415 (2015)","journal-title":"STTT"},{"key":"7_CR8","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)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"He, R., Jennings, P., Basu, S, Ghosh, A.P., Wu, H.: A bounded statistical approach for model checking of unbounded until properties. In: ASE, pp. 225\u2013234 (2010)","DOI":"10.1145\/1858996.1859043"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73\u201384. Springer, Heidelberg (2004)"},{"key":"7_CR11","unstructured":"Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: 3rd International Workshop on the Numerical Solution of Markov Chains, pp. 188\u2013207. Citeseer (1999)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/978-3-642-28756-5_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Jegourel","year":"2012","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking \u2013 PLASMA. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 498\u2013503. Springer, Heidelberg (2012)"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-03845-7_15","volume-title":"Computational Methods in Systems Biology","author":"SK Jha","year":"2009","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A Bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218\u2013234. Springer, Heidelberg (2009)"},{"key":"7_CR14","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)"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: QUEST, pp. 203\u2013204 (2012)","DOI":"10.1109\/QEST.2012.14"},{"issue":"1\u20133","key":"7_CR16","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1016\/j.apal.2007.11.006","volume":"152","author":"R Lassaigne","year":"2008","unstructured":"Lassaigne, R., Peyronnet, S.: Probabilistic verification and approximation. Ann. Pure Appl. Logic 152(1\u20133), 122\u2013131 (2008)","journal-title":"Ann. Pure Appl. Logic"},{"key":"7_CR17","volume-title":"Markov Chains","author":"JR Norris","year":"1998","unstructured":"Norris, J.R.: Markov Chains. Cambridge University Press, Cambridge (1998)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-19811-3_10","volume-title":"Fundamental Approaches to Software Engineering","author":"J Oudinet","year":"2011","unstructured":"Oudinet, J., Denise, A., Gaudel, M.-C., Lassaigne, R., Peyronnet, S.: Uniform monte-carlo model checking. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 127\u2013140. Springer, Heidelberg (2011)"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-04761-9_11","volume-title":"Automated Technology for Verification and Analysis","author":"D Rabih El","year":"2009","unstructured":"El Rabih, D., Pekergin, N.: Statistical model checking using perfect simulation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 120\u2013134. Springer, Heidelberg (2009)"},{"key":"7_CR21","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)"},{"key":"7_CR22","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)"},{"issue":"4","key":"7_CR23","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1023\/B:JOTP.0000011995.28536.ef","volume":"16","author":"E Solan","year":"2003","unstructured":"Solan, E.: Continuity of the value of competitive Markov decision processes. J. Theor. Probab. 16(4), 831\u2013845 (2003)","journal-title":"J. Theor. Probab."},{"issue":"2","key":"7_CR24","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":"7_CR25","unstructured":"Younes, H.L.S.: Planning and verification for stochastic processes with asynchronous events. In: AAAI, pp. 1001\u20131002 (2004)"},{"key":"7_CR26","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. (ed.) SBMF 2010. LNCS, vol. 6527, pp. 144\u2013160. Springer, Heidelberg (2011)"},{"issue":"3","key":"7_CR27","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"HLS Younes","year":"2006","unstructured":"Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. STTT 8(3), 216\u2013228 (2006)","journal-title":"STTT"},{"key":"7_CR28","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)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T01:13:17Z","timestamp":1585012397000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}