{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:26:12Z","timestamp":1740122772348,"version":"3.37.3"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,8,28]],"date-time":"2019-08-28T00:00:00Z","timestamp":1566950400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,8,28]],"date-time":"2019-08-28T00:00:00Z","timestamp":1566950400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CPS 1329991"],"award-info":[{"award-number":["CPS 1329991"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-15-1-0059"],"award-info":[{"award-number":["FA9550-15-1-0059"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2019,11]]},"DOI":"10.1007\/s10703-019-00339-8","type":"journal-article","created":{"date-parts":[[2019,8,28]],"date-time":"2019-08-28T14:06:33Z","timestamp":1567001193000},"page":"145-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Statistical verification of PCTL using antithetic and stratified samples"],"prefix":"10.1007","volume":"54","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0431-1039","authenticated-orcid":false,"given":"Yu","family":"Wang","sequence":"first","affiliation":[]},{"given":"Nima","family":"Roohi","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"West","sequence":"additional","affiliation":[]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[]},{"given":"Geir E.","family":"Dullerud","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,28]]},"reference":[{"issue":"2","key":"339_CR1","first-page":"119","volume":"52","author":"A Agresti","year":"1998","unstructured":"Agresti A, Coull BA (1998) Approximate is better than \u201cexact\u201d for interval estimation of binomial proportions. Am Stat 52(2):119\u2013126","journal-title":"Am Stat"},{"key":"339_CR2","first-page":"1","volume-title":"Automated technology for verification and analysis","author":"EM Clarke","year":"2011","unstructured":"Clarke EM, Zuliani P (2011) Statistical model checking for cyber-physical systems. Automated technology for verification and analysis. Springer, Berlin, pp 1\u201312"},{"key":"339_CR3","unstructured":"D\u2019Argenio P, Jeannet B, Jensen H, Larsen K (2001) Reachability analysis of probabilistic systems by successive refinements. In: de\u00a0Alfaro L, Gilmore S (eds) Proceedings of 1st joint international workshop on process algebra and probabilistic methods, performance modelling and verification (PAPM\/PROBMIV\u201901). Springer, LNCS, vol 2165, pp 39\u201356"},{"issue":"6","key":"339_CR4","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1145\/3812.3818","volume":"28","author":"S Even","year":"1985","unstructured":"Even S, Goldreich O, Lempel A (1985) A randomized protocol for signing contracts. Commun ACM 28(6):637\u2013647","journal-title":"Commun ACM"},{"key":"339_CR5","unstructured":"Helmink L, Sellink M, Vaandrager F (1994) Proof-checking a data link protocol. In: Barendregt H, Nipkow T (eds) Proceedings of international workshop on types for proofs and programs (TYPES\u201993). Springer, LNCS, vol 806, pp 127\u2013165"},{"key":"339_CR6","doi-asserted-by":"crossref","unstructured":"Henriques D, Martins JG, Zuliani P, Platzer A, Clarke EM (2012) Statistical model checking for markov decision processes. In: 2012 Ninth international conference on quantitative evaluation of systems, pp 84\u201393","DOI":"10.1109\/QEST.2012.19"},{"key":"339_CR7","first-page":"1","volume":"8","author":"H Hermanns","year":"2012","unstructured":"Hermanns H, Nielson F, Jansen DN, Zhang L (2012) Efficient csl model checking using stratification. Log Methods Comput Sci 8:1\u201318","journal-title":"Log Methods Comput Sci"},{"key":"339_CR8","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: Verification of probabilistic real-time systems. In: International conference on computer aided verification. Springer, pp 585\u2013591"},{"key":"339_CR9","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-47166-2_1","volume-title":"Leveraging applications of formal methods, verification and validation: foundational techniques","author":"KG Larsen","year":"2016","unstructured":"Larsen KG, Legay A (2016) Statistical model checking: past, present, and future. Leveraging applications of formal methods, verification and validation: foundational techniques. Springer, Cham, pp 3\u201315"},{"key":"339_CR10","volume-title":"Monte Carlo strategies in scientific computing","author":"J Liu","year":"2008","unstructured":"Liu J (2008) Monte Carlo strategies in scientific computing. Springer, Cham"},{"key":"339_CR11","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1016\/j.jcp.2016.06.019","volume":"322","author":"PA Maginnis","year":"2016","unstructured":"Maginnis PA, West M, Dullerud GE (2016) Variance-reduced simulation of lattice discrete-time markov chains with applications in reaction networks. J Comput Phys 322:400\u2013414","journal-title":"J Comput Phys"},{"issue":"6","key":"339_CR12","doi-asserted-by":"publisher","first-page":"561","DOI":"10.3233\/JCS-2006-14604","volume":"14","author":"G Norman","year":"2006","unstructured":"Norman G, Shmatikov V (2006) Analysis of probabilistic contract signing. J Comput Secur 14(6):561\u2013589","journal-title":"J Comput Secur"},{"issue":"1","key":"339_CR13","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"M Reiter","year":"1998","unstructured":"Reiter M, Rubin A (1998) Crowds: anonymity for web transactions. ACM Trans Inf Syst Secur (TISSEC) 1(1):66\u201392","journal-title":"ACM Trans Inf Syst Secur (TISSEC)"},{"key":"339_CR14","doi-asserted-by":"crossref","unstructured":"Roohi N, Wang Y, West M, Dullerud GE, Viswanathan M (2017) Statistical verification of the Toyota powertrain control verification benchmark. In: Proceedings of the 20th international conference on hybrid systems: computation and control. ACM, pp 65\u201370","DOI":"10.1145\/3049797.3049804"},{"key":"339_CR15","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"Koushik Sen","year":"2004","unstructured":"Sen K, Viswanathan M, Agha G (2004) Statistical model checking of black-box probabilistic systems. In: Alur R, Peled DA (eds) computer aided verification. Springer, Berlin, Heidelberg, no. 3114 in Lecture Notes in Computer Science, pp 202\u2013215"},{"key":"339_CR16","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"Koushik Sen","year":"2005","unstructured":"Sen K, Viswanathan M, Agha G (2005) On statistical model checking of stochastic systems. In: Etessami K, Rajamani SK (eds) Computer aided verification. Springer, Berlin, Heidelberg, no. 3576 in Lecture Notes in Computer Science, pp 266\u2013280"},{"key":"339_CR17","doi-asserted-by":"crossref","unstructured":"Sen K, Viswanathan M, Agha G (2005) Vesta: A statistical model-checker and analyzer for probabilistic systems. In: Second international conference on the quantitative evaluation of systems, 2005, pp 251\u2013252","DOI":"10.1109\/QEST.2005.42"},{"key":"339_CR18","doi-asserted-by":"crossref","unstructured":"Shmatikov V (2002) Probabilistic analysis of anonymity. In: Proceedings of the 15th IEEE computer security foundations workshop (CSFW\u201902). IEEE Computer Society Press, pp 119\u2013128","DOI":"10.1109\/CSFW.2002.1021811"},{"issue":"3\/4","key":"339_CR19","doi-asserted-by":"publisher","first-page":"355","DOI":"10.3233\/JCS-2004-123-403","volume":"12","author":"V Shmatikov","year":"2004","unstructured":"Shmatikov V (2004) Probabilistic model checking of an anonymity system. J Comput Secur 12(3\/4):355\u2013377","journal-title":"J Comput Secur"},{"issue":"1","key":"339_CR20","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/j.jspi.2004.01.005","volume":"131","author":"T Tony Cai","year":"2005","unstructured":"Tony Cai T (2005) One-sided confidence intervals in discrete distributions. J Stat Plan Inference 131(1):63\u201388","journal-title":"J Stat Plan Inference"},{"issue":"27","key":"339_CR21","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/j.ifacol.2015.11.186","volume":"48","author":"Y Wang","year":"2015","unstructured":"Wang Y, Roohi N, West M, Viswanathan M, Dullerud GE (2015) A mori-zwanzig and mitl based approach to statistical verification of continuous-time dynamical systems. IFAC-PapersOnLine 48(27):267\u2013273","journal-title":"IFAC-PapersOnLine"},{"key":"339_CR22","doi-asserted-by":"crossref","unstructured":"Wang Y, Roohi N, West M, Viswanathan M, Dullerud GE (2015) Statistical verification of dynamical systems using set oriented methods. In: Proceedings of the 18th international conference on hybrid systems: computation and control. ACM, New York, HSCC \u201915, pp 169\u2013178","DOI":"10.1145\/2728606.2728627"},{"key":"339_CR23","doi-asserted-by":"crossref","unstructured":"Wang Y, Roohi N, West M, Viswanathan M, Dullerud GE (2016) Verifying continuous-time stochastic hybrid systems via mori-zwanzig model reduction. In: 2016 IEEE 55th conference on decision and control (CDC), pp 3012\u20133017","DOI":"10.1109\/CDC.2016.7798719"},{"issue":"16","key":"339_CR24","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/j.ifacol.2018.08.015","volume":"51","author":"Y Wang","year":"2018","unstructured":"Wang Y, Roohi N, West M, Viswanathan M, Dullerud GE (2018) Statistical verification of pctl using stratified samples. IFAC-PapersOnLine 51(16):85\u201390","journal-title":"IFAC-PapersOnLine"},{"key":"339_CR25","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Computer Aided Verification","author":"H\u00e5kan L. S. Younes","year":"2005","unstructured":"Younes HLS (2005) Ymer: a statistical model checker. In: Etessami K, Rajamani SK (eds) Computer aided verification. Springer, Berlin, no. 3576 in Lecture Notes in Computer Science, pp 429\u2013433"},{"issue":"9","key":"339_CR26","doi-asserted-by":"publisher","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"HLS Younes","year":"2006","unstructured":"Younes HLS, Simmons RG (2006) Statistical probabilistic model checking with a focus on time-bounded properties. Inf Comput 204(9):1368\u20131409","journal-title":"Inf Comput"},{"key":"339_CR27","doi-asserted-by":"crossref","unstructured":"Zuliani P, Baier C, Clarke EM (2012) Rare-event verification for stochastic hybrid systems. In: Proceedings of the 15th ACM international conference on hybrid systems: computation and control. ACM, New York, HSCC \u201912, pp 217\u2013226","DOI":"10.1145\/2185632.2185665"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00339-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-019-00339-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00339-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,26]],"date-time":"2020-08-26T23:39:05Z","timestamp":1598485145000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-019-00339-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,28]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,11]]}},"alternative-id":["339"],"URL":"https:\/\/doi.org\/10.1007\/s10703-019-00339-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2019,8,28]]},"assertion":[{"value":"28 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}