{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T23:30:14Z","timestamp":1769815814446,"version":"3.49.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319663340","type":"print"},{"value":"9783319663357","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66335-7_23","type":"book-chapter","created":{"date-parts":[[2017,8,10]],"date-time":"2017-08-10T03:53:48Z","timestamp":1502337228000},"page":"333-350","source":"Crossref","is-referenced-by-count":6,"title":["Sequential Schemes for Frequentist Estimation of Properties in Statistical Model Checking"],"prefix":"10.1007","author":[{"given":"Cyrille","family":"Jegourel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,11]]},"reference":[{"issue":"2","key":"23_CR1","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/0022-0000(79)90045-X","volume":"18","author":"D Angluin","year":"1979","unstructured":"Angluin, D., Valiant, L.: Fast probabilistic algorithms for Hamiltonian circuits and matchings. J. Comput. Syst. Sci. 18(2), 155\u2013193 (1979)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"23_CR2","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1214\/ss\/1009213286","volume":"16","author":"L Brown","year":"2001","unstructured":"Brown, L., Cai, T., DasGupta, A.: Interval estimation for a binomial proportion. Stat. Sci. 16(2), 101\u2013133 (2001)","journal-title":"Stat. Sci."},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Chen, J.: Properties of a new adaptive sampling method with applications to scalable learning. In: WI, pp. 9\u201315, Atlanta (2013)","DOI":"10.1109\/WI-IAT.2013.3"},{"issue":"4","key":"23_CR4","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1214\/aoms\/1177729330","volume":"23","author":"H Chernoff","year":"1952","unstructured":"Chernoff, H.: A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations. Ann. Math. Stat. 23(4), 493\u2013507 (1952)","journal-title":"Ann. Math. Stat."},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-24372-1_1","volume-title":"Automated Technology for Verification and Analysis","author":"EM Clarke","year":"2011","unstructured":"Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1\u201312. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24372-1_1"},{"key":"23_CR6","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1093\/biomet\/26.4.404","volume":"26","author":"CJ Clopper","year":"1934","unstructured":"Clopper, C.J., Pearson, E.S.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26, 404\u2013413 (1934)","journal-title":"Biometrika"},{"issue":"5","key":"23_CR7","doi-asserted-by":"crossref","first-page":"1484","DOI":"10.1137\/S0097539797315306","volume":"29","author":"P Dagum","year":"2000","unstructured":"Dagum, P., Karp, R., Luby, M., Ross, S.: An optimal algorithm for Monte Carlo estimation. SIAM J. Comput. 29(5), 1484\u20131496 (2000)","journal-title":"SIAM J. Comput."},{"issue":"4","key":"23_CR8","doi-asserted-by":"crossref","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"},{"issue":"3","key":"23_CR9","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1198\/tast.2010.09140","volume":"64","author":"J Frey","year":"2010","unstructured":"Frey, J.: Fixed-width sequential confidence intervals for a proportion. Am. Stat. 64(3), 242\u2013249 (2010)","journal-title":"Am. Stat."},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-662-45231-8_16","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications","author":"R Grosu","year":"2014","unstructured":"Grosu, R., Peled, D., Ramakrishnan, C.R., Smolka, S.A., Stoller, S.D., Yang, J.: Using statistical model checking for measuring systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 223\u2013238. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-45231-8_16"},{"key":"23_CR11","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). doi: 10.1007\/978-3-540-24622-0_8"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"H\u00e9rault, T., Lassaigne, R., Peyronnet, S.: APMC 3.0: approximate verification of discrete and continuous time Markov chains. In: QEST, pp. 129\u2013130 (2006)","DOI":"10.1109\/QEST.2006.5"},{"issue":"301","key":"23_CR13","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","volume":"58","author":"W Hoeffding","year":"1963","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13\u201330 (1963)","journal-title":"J. Am. Stat. Assoc."},{"key":"23_CR14","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). doi: 10.1007\/978-3-642-28756-5_37"},{"key":"23_CR15","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). doi: 10.1007\/978-3-642-39799-8_38"},{"key":"23_CR16","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_CR17","doi-asserted-by":"crossref","first-page":"1269","DOI":"10.1214\/aop\/1176990746","volume":"18","author":"P Massart","year":"1990","unstructured":"Massart, P.: The tight constant in the Dvoretzky-Kiefer-Wolfowitz inequality. Ann. Prob. 18, 1269\u20131283 (1990)","journal-title":"Ann. Prob."},{"issue":"247","key":"23_CR18","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1080\/01621459.1949.10483310","volume":"44","author":"N Metropolis","year":"1949","unstructured":"Metropolis, N., Ulam, S.: The Monte Carlo method. J. Am. Stat. Assoc. 44(247), 335\u2013341 (1949)","journal-title":"J. Am. Stat. Assoc."},{"key":"23_CR19","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/BF02883985","volume":"10","author":"M Okamoto","year":"1958","unstructured":"Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Statis. Math. 10, 29\u201335 (1958)","journal-title":"Ann. Inst. Statis. Math."},{"issue":"2","key":"23_CR20","doi-asserted-by":"crossref","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_CR21","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.tcs.2005.09.003","volume":"348","author":"O Watanabe","year":"2005","unstructured":"Watanabe, O.: Sequential sampling techniques for algorithmic learning theory. Theoret. Comput. Sci. 348, 3\u201314 (2005)","journal-title":"Theoret. Comput. Sci."},{"key":"23_CR22","unstructured":"Younes, H.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon University (2004)"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-540-24730-2_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"HLS Younes","year":"2004","unstructured":"Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking: an empirical study. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 46\u201360. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24730-2_4"},{"issue":"2","key":"23_CR24","first-page":"338","volume":"43","author":"P Zuliani","year":"2013","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to stateflow\/simulink verification. FMSD 43(2), 338\u2013367 (2013)","journal-title":"FMSD"}],"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-66335-7_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T21:38:05Z","timestamp":1750801085000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66335-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319663340","9783319663357"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66335-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}