{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T16:23:40Z","timestamp":1792254220483,"version":"4.4.0"},"publisher-location":"Cham","reference-count":93,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032057914","type":"print"},{"value":"9783032057921","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:00:00Z","timestamp":1759363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:00:00Z","timestamp":1759363200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-05792-1_11","type":"book-chapter","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T10:31:33Z","timestamp":1759314693000},"page":"195-218","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["What Are the\u00a0Odds? Improving Statistical Model Checking of\u00a0Markov Decision Processes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1712-2165","authenticated-orcid":false,"given":"Tobias","family":"Meggendorfer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0163-2152","authenticated-orcid":false,"given":"Maximilian","family":"Weininger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8047-4094","authenticated-orcid":false,"given":"Patrick","family":"Wienh\u00f6ft","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,10,2]]},"reference":[{"key":"11_CR1","unstructured":"Agarwal, A., Kakade, S.M., Yang, L.F.: Model-based reinforcement learning with a generative model is minimax optimal. In: COLT. Proceedings of Machine Learning Research, vol.\u00a0125, pp. 67\u201383. PMLR (2020). http:\/\/proceedings.mlr.press\/v125\/agarwal20b.html"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-13188-2_1","volume-title":"Computer Aided Verification","author":"C Agarwal","year":"2022","unstructured":"Agarwal, C., Guha, S., K\u0159et\u00ednsk\u1ef3, J., Muruganandham, P.: PAC statistical model checking of mean payoff in discrete-and continuous-time MDP. In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13372, pp. 3\u201325. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_1"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018). https:\/\/doi.org\/10.1145\/3158668","DOI":"10.1145\/3158668"},{"issue":"2","key":"11_CR4","first-page":"119","volume":"52","author":"A Agresti","year":"1998","unstructured":"Agresti, A., Coull, B.A.: Approximate is better than \u201cexact\u2019\u2019 for interval estimation of binomial proportions. Am. Stat. 52(2), 119\u2013126 (1998)","journal-title":"Am. Stat."},{"key":"11_CR5","unstructured":"Aitkin, M., Anderson, D., Francis, B., Hinde, J.: Statistical modelling in GLIM, pp. 112\u2013118 (1988)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: AAAI, pp. 2669\u20132678. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.11797"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Anthony, M., Bartlett, P.L.: General Lower Bounds on Sample Complexity, pp. 59\u201373. Cambridge University Press (1999)","DOI":"10.1017\/CBO9780511624216.006"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-030-25540-4_29","volume-title":"Computer Aided Verification","author":"P Ashok","year":"2019","unstructured":"Ashok, P., K\u0159et\u00ednsk\u00fd, J., Weininger, M.: PAC statistical model checking for Markov decision processes and stochastic games. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 497\u2013519. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_29"},{"key":"11_CR9","unstructured":"Ashok, P., Kret\u00ednsk\u00fd, J., Weininger, M.: PAC statistical model checking for Markov decision processes and stochastic games. CoRR abs\/1905.04403 (2019). http:\/\/arxiv.org\/abs\/1905.04403"},{"key":"11_CR10","unstructured":"Auer, P., Jaksch, T., Ortner, R.: Near-optimal regret bounds for reinforcement learning. In: Advances in Neural Information Processing Systems, vol. 21 (2008)"},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1613\/jair.1.14253","volume":"76","author":"TS Badings","year":"2023","unstructured":"Badings, T.S., et al.: Robust control for dynamical systems with non-gaussian noise via formal abstractions. J. Artif. Intell. Res. 76, 341\u2013391 (2023)","journal-title":"J. Artif. Intell. Res."},{"issue":"3","key":"11_CR12","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/s10009-023-00704-3","volume":"25","author":"TS Badings","year":"2023","unstructured":"Badings, T.S., Sim\u00e3o, T.D., Suilen, M., Jansen, N.: Decision-making under uncertainty: beyond probabilities. Int. J. Softw. Tools Technol. Transf. 25(3), 375\u2013391 (2023)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-031-33170-1_6","volume-title":"NASA Formal Methods","author":"C Baier","year":"2023","unstructured":"Baier, C., Dubslaff, C., Wienh\u00f6ft, P., Kiebel, S.J.: Strategy synthesis in Markov decision processes under limited sampling access. In: Rozier, K.Y., Chaudhuri, S. (eds.) NFM 2023. LNCS, vol. 13903, pp. 86\u2013103. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_6"},{"key":"11_CR14","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008). https:\/\/mitpress.mit.edu\/books\/principles-model-checking"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-030-53291-8_17","volume-title":"Computer Aided Verification","author":"H Bazille","year":"2020","unstructured":"Bazille, H., Genest, B., Jegourel, C., Sun, J.: Global PAC bounds for learning discrete time Markov chains. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 304\u2013326. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_17"},{"issue":"297","key":"11_CR16","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1080\/01621459.1962.10482149","volume":"57","author":"G Bennett","year":"1962","unstructured":"Bennett, G.: Probability inequalities for the sum of independent random variables. J. Am. Stat. Assoc. 57(297), 33\u201345 (1962)","journal-title":"J. Am. Stat. Assoc."},{"key":"11_CR17","unstructured":"Bernstein, S.: On a modification of Chebyshev\u2019s inequality and of the error formula of Laplace. Ann. Sci. Inst. Sav. Ukraine Sect. Math 1(4), 38\u201349 (1924)"},{"issue":"381","key":"11_CR18","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1080\/01621459.1983.10477938","volume":"78","author":"CR Blyth","year":"1983","unstructured":"Blyth, C.R., Still, H.A.: Binomial confidence intervals. J. Am. Stat. Assoc. 78(381), 108\u2013116 (1983)","journal-title":"J. Am. Stat. Assoc."},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Boucheron, S., Lugosi, G., Massart, P.: Concentration Inequalities: A Nonasymptotic Theory of Independence. Oxford University Press (2013) https:\/\/doi.org\/10.1093\/acprof:oso\/9780199535255.001.0001","DOI":"10.1093\/acprof:oso\/9780199535255.001.0001"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., et al.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"issue":"2","key":"11_CR21","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1214\/ss\/1009213286","volume":"16","author":"LD Brown","year":"2001","unstructured":"Brown, L.D., Cai, T.T., DasGupta, A.: Interval estimation for a binomial proportion. Stat. Sci. 16(2), 101\u2013133 (2001). https:\/\/doi.org\/10.1214\/ss\/1009213286","journal-title":"Stat. Sci."},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., et al.: Learning algorithms for verification of Markov decision processes. TheoretiCS 4, 10 (2025). https:\/\/doi.org\/10.46298\/theoretics.25.10","DOI":"10.46298\/theoretics.25.10"},{"issue":"7","key":"11_CR23","doi-asserted-by":"publisher","first-page":"1726","DOI":"10.1109\/TSE.2024.3392720","volume":"50","author":"H Bu","year":"2024","unstructured":"Bu, H., Sun, M.: Clopper-Pearson algorithms for efficient statistical model checking estimation. IEEE Trans. Software Eng. 50(7), 1726\u20131746 (2024). https:\/\/doi.org\/10.1109\/TSE.2024.3392720","journal-title":"IEEE Trans. Software Eng."},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-69483-2_3","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"CE Budde","year":"2017","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A.: Better automated importance splitting for transient rare events. In: Larsen, K.G., Sokolsky, O., Wang, J. (eds.) SETTA 2017. LNCS, vol. 10606, pp. 42\u201358. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-69483-2_3"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Carlos, E.B., Arnd, H., Tobias, M., Maximilian, W., Patrick, W.: Sound statistical model checking for probabilities and expected rewards. In: Arie, G., Marijn., H. (ed.) Tools and Algorithms for the Construction and Analysis of Systems-31st International Conference, Held as Part of the International Joint Conferences on Theory and Practice of Software, Hamilton, ON, Canada, Proceedings, Part I, Lecture Notes in Computer Science, vol. 15696, pp.167\u2014190. Springer, (2025). https:\/\/doi.org\/10.1007\/978-3-031-90643-5_9","DOI":"10.1007\/978-3-031-90643-5_9"},{"key":"11_CR26","unstructured":"Casella, G., McCulloch, C.E.: Confidence intervals for discrete distributions (1984)"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"issue":"4","key":"11_CR28","doi-asserted-by":"publisher","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(4), 404\u2013413 (1934)","journal-title":"Biometrika"},{"issue":"2","key":"11_CR29","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1214\/ss\/1009213286","volume":"16","author":"C Corcoran","year":"2001","unstructured":"Corcoran, C., Mehta, C.: Comment on \u201cinterval estimation for a binomial proportion\u2019\u2019. Stat. Sci. 16(2), 120\u2013122 (2001). https:\/\/doi.org\/10.1214\/ss\/1009213286","journal-title":"Stat. Sci."},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Daca, P., Henzinger, T.A., Kret\u00ednsk\u00fd, J., Petrov, T.: Faster statistical model checking for unbounded temporal properties. ACM Trans. Comput. Log. 18(2), 12:1\u201312:25 (2017)","DOI":"10.1145\/3060139"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Dagum, P., Karp, R., Luby, M., Ross, S.: An optimal algorithm for Monte Carlo estimation. In: Proceedings of IEEE 36th Annual Foundations of Computer Science, pp. 142\u2013149 (1995). https:\/\/doi.org\/10.1109\/SFCS.1995.492471","DOI":"10.1109\/SFCS.1995.492471"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-030-03421-4_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"PR D\u2019Argenio","year":"2018","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: Lightweight statistical model checking in nondeterministic continuous time. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 336\u2013353. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_22"},{"issue":"4","key":"11_CR33","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/S10009-015-0383-0","volume":"17","author":"PR D\u2019Argenio","year":"2015","unstructured":"D\u2019Argenio, P.R., Legay, A., Sedwards, S., Traonouez, L.: Smart sampling for lightweight verification of Markov decision processes. Int. J. Softw. Tools Technol. Transf. 17(4), 469\u2013484 (2015). https:\/\/doi.org\/10.1007\/S10009-015-0383-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR34","unstructured":"De\u00a0Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University (1997). https:\/\/exhibits.stanford.edu\/cs\/catalog\/xz681dy7227"},{"issue":"4","key":"11_CR35","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1093\/jssam\/smv024","volume":"3","author":"N Dean","year":"2015","unstructured":"Dean, N., Pagano, M.: Evaluating confidence interval methods for binomial proportions in clustered surveys. J. Surv. Stat. Methodol. 3(4), 484\u2013503 (2015)","journal-title":"J. Surv. Stat. Methodol."},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Duffy, D.E., Santner, T.J.: Confidence intervals for a binomial parameter based on multistage tests. Biometrics 81\u201393 (1987)","DOI":"10.2307\/2531951"},{"issue":"3","key":"11_CR37","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1214\/aoms\/1177728174","volume":"27","author":"A Dvoretzky","year":"1956","unstructured":"Dvoretzky, A., Kiefer, J., Wolfowitz, J.: Asymptotic minimax character of the sample distribution function and of the classical multinomial estimator. Ann. Math. Stat. 27(3), 642\u2013669 (1956). https:\/\/doi.org\/10.1214\/aoms\/1177728174","journal-title":"Ann. Math. Stat."},{"key":"11_CR38","doi-asserted-by":"publisher","unstructured":"Fu, J., Topcu, U.: Probably approximately correct MDP learning and control with temporal logic constraints. In: Robotics: Science and Systems (2014). https:\/\/doi.org\/10.15607\/RSS.2014.X.039","DOI":"10.15607\/RSS.2014.X.039"},{"key":"11_CR39","unstructured":"Ghavamzadeh, M., Petrik, M., Chow, Y.: Safe policy improvement by minimizing robust baseline regret. In: Lee, D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, pp. 2298\u20132306 (2016). https:\/\/proceedings.neurips.cc\/paper\/2016\/hash\/9a3d458322d70046f63dfd8b0153ece4-Abstract.html"},{"issue":"1\u20132","key":"11_CR40","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0004-3702(00)00047-3","volume":"122","author":"R Givan","year":"2000","unstructured":"Givan, R., Leach, S., Dean, T.: Bounded-parameter Markov decision processes. Artif. Intell. 122(1\u20132), 71\u2013109 (2000)","journal-title":"Artif. Intell."},{"key":"11_CR41","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111\u2013131 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2016.12.003","journal-title":"Theor. Comput. Sci."},{"key":"11_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-030-17462-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EM Hahn","year":"2019","unstructured":"Hahn, E.M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., Wojtczak, D.: Omega-regular objectives in model-free reinforcement learning. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 395\u2013412. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_27"},{"key":"11_CR43","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., Wojtczak, D.: Mungojerrie: linear-time objectives in model-free reinforcement learning. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13993, pp. 527\u2013545. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_27","DOI":"10.1007\/978-3-031-30823-9_27"},{"key":"11_CR44","doi-asserted-by":"publisher","unstructured":"HasanzadeZonuzy, A., Bura, A., Kalathil, D.M., Shakkottai, S.: Learning with safety constraints: sample complexity of reinforcement learning for constrained MDPs. In: AAAI, pp. 7667\u20137674. AAAI Press (2021). https:\/\/doi.org\/10.1609\/AAAI.V35I9.16937","DOI":"10.1609\/AAAI.V35I9.16937"},{"key":"11_CR45","doi-asserted-by":"publisher","unstructured":"Henriques, D., Martins, J.G., Zuliani, P., Platzer, A., Clarke, E.M.: Statistical model checking for Markov decision processes. In: Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012, London, United Kingdom, 17\u201320 September 2012, pp. 84\u201393. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/QEST.2012.19","DOI":"10.1109\/QEST.2012.19"},{"issue":"301","key":"11_CR46","doi-asserted-by":"publisher","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":"11_CR47","unstructured":"Huber, M.: An unbiased estimate for the mean of a 0, 1 random variable with relative error distribution independent of the mean. CoRR abs\/1309.5413 (2013). https:\/\/arxiv.org\/abs\/1309.5413"},{"key":"11_CR48","doi-asserted-by":"publisher","unstructured":"Huber, M.: Tight relative estimation in the mean of Bernoulli random variables. CoRR abs\/2210.12861 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2210.12861","DOI":"10.48550\/ARXIV.2210.12861"},{"key":"11_CR49","doi-asserted-by":"publisher","unstructured":"J\u00e9gourel, C., Sun, J., Dong, J.S.: Sequential schemes for frequentist estimation of properties in statistical model checking. ACM Trans. Model. Comput. Simul. 29(4), 25:1\u201325:22 (2019). https:\/\/doi.org\/10.1145\/3310226","DOI":"10.1145\/3310226"},{"key":"11_CR50","unstructured":"Jin, C., Krishnamurthy, A., Simchowitz, M., Yu, T.: Reward-free exploration for reinforcement learning. In: ICML. Proceedings of Machine Learning Research, vol.\u00a0119, pp. 4870\u20134879. PMLR (2020). http:\/\/proceedings.mlr.press\/v119\/jin20d.html"},{"key":"11_CR51","doi-asserted-by":"publisher","unstructured":"Klein, J., Phung, H., Hajnal, M., \u0160afr\u00e1nek, D., Petrov, T.: Combining formal methods and Bayesian approach for inferring discrete-state stochastic models from steady-state data. PLOS ONE 18(11), 1\u201326 (2023). https:\/\/doi.org\/10.1371\/journal.pone.0291151","DOI":"10.1371\/journal.pone.0291151"},{"key":"11_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-319-47166-2_3","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"J K\u0159et\u00ednsk\u00fd","year":"2016","unstructured":"K\u0159et\u00ednsk\u00fd, J.: Survey of statistical verification of linear unbounded properties: model checking and distances. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 27\u201345. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_3"},{"key":"11_CR53","unstructured":"Kret\u00ednsk\u00fd, J., Michel, F., Michel, L., P\u00e9rez, G.A.: Finite-memory near-optimal learning for Markov decision processes with long-run average reward. In: UAI. Proceedings of Machine Learning Research, vol.\u00a0124, pp. 1149\u20131158. AUAI Press (2020)"},{"key":"11_CR54","unstructured":"K\u0159et\u00ednsk\u00fd, J., P\u00e9rez, G.A., Raskin, J.F.: Learning-based mean-payoff optimization in an unknown MDP under omega-regular constraints. In: CONCUR, pp. 8:1\u20138:18. Dagstuhl (2018)"},{"key":"11_CR55","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST, pp. 203\u2013204. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/QEST.2012.14","DOI":"10.1109\/QEST.2012.14"},{"key":"11_CR56","doi-asserted-by":"publisher","unstructured":"Lange, S., Gabel, T., Riedmiller, M.A.: Batch reinforcement learning. In: Wiering, M., van Otterlo, M. (eds.) Reinforcement Learning. Adaptation, Learning, and Optimization, vol.\u00a012, pp. 45\u201373. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27645-3_2","DOI":"10.1007\/978-3-642-27645-3_2"},{"key":"11_CR57","doi-asserted-by":"publisher","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate planning and verification for large Markov decision processes. In: SAC, pp. 1314\u20131319. ACM (2012). https:\/\/doi.org\/10.1145\/2245276.2231984","DOI":"10.1145\/2245276.2231984"},{"issue":"4","key":"11_CR58","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/S10009-014-0344-Z","volume":"17","author":"R Lassaigne","year":"2015","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate planning and verification for large Markov decision processes. Int. J. Softw. Tools Technol. Transf. 17(4), 457\u2013467 (2015). https:\/\/doi.org\/10.1007\/S10009-014-0344-Z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122\u2013135. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_11"},{"key":"11_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-319-91908-9_23","volume-title":"Computing and Software Science","author":"A Legay","year":"2019","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 478\u2013504. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_23"},{"key":"11_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-319-15201-1_23","volume-title":"Software Engineering and Formal Methods","author":"A Legay","year":"2015","unstructured":"Legay, A., Sedwards, S., Traonouez, L.-M.: Scalable verification of Markov decision processes. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 350\u2013362. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15201-1_23"},{"key":"11_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-319-47166-2_6","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"A Legay","year":"2016","unstructured":"Legay, A., Sedwards, S., Traonouez, L.-M.: Plasma lab: a modular statistical model checking platform. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 77\u201393. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_6"},{"key":"11_CR63","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., et al.: ARES: adaptive receding-horizon synthesis of optimal plans. In: Legay, A., Margaria, T. (eds.) TACAS 2017, Part II. LNCS, vol. 10206, pp. 286\u2013302. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_17"},{"key":"11_CR64","doi-asserted-by":"publisher","unstructured":"Massart, P.: The tight constant in the Dvoretzky-Kiefer-Wolfowitz inequality. Ann. Probab. 18(3), 1269\u20131283 (1990). https:\/\/doi.org\/10.1214\/aop\/1176990746","DOI":"10.1214\/aop\/1176990746"},{"key":"11_CR65","unstructured":"Maurer, A., Pontil, M.: Empirical Bernstein bounds and sample-variance penalization. In: COLT (2009). http:\/\/www.cs.mcgill.ca\/%7Ecolt2009\/papers\/012.pdf#page=1"},{"key":"11_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-031-65633-0_16","volume-title":"Computer Aided Verification","author":"T Meggendorfer","year":"2024","unstructured":"Meggendorfer, T., Weininger, M.: Playing games with your PET: extending the partial exploration tool to stochastic games. In: Gurfinkel, A., Ganesh, V. (eds.) CAV 2024. LNCS, vol. 14683, pp. 359\u2013372. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_16"},{"key":"11_CR67","doi-asserted-by":"publisher","unstructured":"Meggendorfer, T., Weininger, M., Wienh\u00f6ft, P.: What are the odds? Improving the foundations of statistical model checking. CoRR abs\/2404.05424 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2404.05424","DOI":"10.48550\/ARXIV.2404.05424"},{"key":"11_CR68","doi-asserted-by":"crossref","unstructured":"Meggendorfer, T., Weininger, M., Wienh\u00f6ft, P.: Solving robust Markov decision processes: generic, reliable, efficient. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a039, pp. 26631\u201326641 (2025). https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/download\/34865\/37020","DOI":"10.1609\/aaai.v39i25.34865"},{"key":"11_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-030-60327-4_14","volume-title":"Computational Methods in Systems Biology","author":"GW Molyneux","year":"2020","unstructured":"Molyneux, G.W., Abate, A.: ABC(SMC)$$^2$$: simultaneous inference and model checking of chemical reaction networks. In: Abate, A., Petrov, T., Wolf, V. (eds.) CMSB 2020. LNCS, vol. 12314, pp. 255\u2013279. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60327-4_14"},{"issue":"8","key":"11_CR70","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1002\/(SICI)1097-0258(19980430)17:8<857::AID-SIM777>3.0.CO;2-E","volume":"17","author":"RG Newcombe","year":"1998","unstructured":"Newcombe, R.G.: Two-sided confidence intervals for the single proportion: comparison of seven methods. Stat. Med. 17(8), 857\u2013872 (1998). https:\/\/doi.org\/10.1002\/(SICI)1097-0258(19980430)17:8<857::AID-SIM777>3.0.CO;2-E","journal-title":"Stat. Med."},{"key":"11_CR71","unstructured":"Office of Emergency and Remedial Response U.S. Environmental Protection Agency: Calculating upper confidence limits for exposure point concentrations at hazardous waste sites (2002)"},{"issue":"1","key":"11_CR72","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(1), 29\u201335 (1959). https:\/\/doi.org\/10.1007\/bf02883985","journal-title":"Ann. Inst. Stat. Math."},{"key":"11_CR73","doi-asserted-by":"publisher","unstructured":"Perez, M., Somenzi, F., Trivedi, A.: A PAC learning algorithm for LTL and omega-regular objectives in MDPs. In: AAAI, pp. 21510\u201321517. AAAI Press (2024). https:\/\/doi.org\/10.1609\/AAAI.V38I19.30148","DOI":"10.1609\/AAAI.V38I19.30148"},{"key":"11_CR74","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley (1994)","DOI":"10.1002\/9780470316887"},{"issue":"4","key":"11_CR75","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/S10009-014-0350-1","volume":"17","author":"D Reijsbergen","year":"2015","unstructured":"Reijsbergen, D., de Boer, P., Scheinhardt, W.R.W., Haverkort, B.R.: On hypothesis testing for statistical model checking. Int. J. Softw. Tools Technol. Transf. 17(4), 377\u2013395 (2015). https:\/\/doi.org\/10.1007\/S10009-014-0350-1","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-89366-2_20","volume-title":"Foundations of Software Science and Computation Structures","author":"S Le Roux","year":"2018","unstructured":"Le Roux, S., P\u00e9rez, G.A.: The complexity of graph-based reductions for reachability in Markov decision processes. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 367\u2013383. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_20"},{"issue":"2","key":"11_CR77","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1214\/ss\/1009213286","volume":"16","author":"TJ Santner","year":"2001","unstructured":"Santner, T.J.: Comment on \u201cinterval estimation for a binomial proportion\u2019\u2019. Stat. Sci. 16(2), 126\u2013128 (2001). https:\/\/doi.org\/10.1214\/ss\/1009213286","journal-title":"Stat. Sci."},{"key":"11_CR78","unstructured":"Shi, L., Li, G., Wei, Y., Chen, Y., Chi, Y.: Pessimistic Q-learning for offline reinforcement learning: towards optimal sample complexity. In: ICML. Proceedings of Machine Learning Research, vol.\u00a0162, pp. 19967\u201320025. PMLR (2022). https:\/\/proceedings.mlr.press\/v162\/shi22c.html"},{"key":"11_CR79","doi-asserted-by":"crossref","unstructured":"Strehl, A.L., Littman, M.L.: An empirical evaluation of interval estimation for Markov decision processes. In: 16th IEEE International Conference on Tools with Artificial Intelligence, pp. 128\u2013135. IEEE (2004)","DOI":"10.1109\/ICTAI.2004.28"},{"key":"11_CR80","doi-asserted-by":"crossref","unstructured":"Student: the probable error of a mean. Biometrika 1\u201325 (1908)","DOI":"10.2307\/2331554"},{"key":"11_CR81","doi-asserted-by":"crossref","unstructured":"Suilen, M., Sim\u00e3o, T.D., Parker, D., Jansen, N.: Robust anytime learning of Markov decision processes. In: NeurIPS (2022)","DOI":"10.52202\/068431-2087"},{"issue":"1\u20132","key":"11_CR82","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/0377-0427(92)90244-R","volume":"41","author":"NM Temme","year":"1992","unstructured":"Temme, N.M.: Asymptotic inversion of the incomplete beta function. J. Comput. Appl. Math. 41(1\u20132), 145\u2013157 (1992)","journal-title":"J. Comput. Appl. Math."},{"key":"11_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-642-02742-0_22","volume-title":"Network Performance Engineering","author":"M Vill\u00e9n-Altamirano","year":"2011","unstructured":"Vill\u00e9n-Altamirano, M., Vill\u00e9n-Altamirano, J.: The rare event simulation method RESTART: efficiency analysis and guidelines for its application. In: Kouvatsos, D.D. (ed.) Network Performance Engineering. LNCS, vol. 5233, pp. 509\u2013547. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-02742-0_22"},{"key":"11_CR84","unstructured":"Wagenmaker, A.J., Simchowitz, M., Jamieson, K.: Beyond no regret: instance-dependent PAC reinforcement learning. In: COLT. Proceedings of Machine Learning Research, vol.\u00a0178, pp. 358\u2013418. PMLR (2022). https:\/\/proceedings.mlr.press\/v178\/wagenmaker22a.html"},{"issue":"2","key":"11_CR85","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). https:\/\/doi.org\/10.1214\/aoms\/1177731118","journal-title":"Ann. Math. Stat."},{"issue":"3","key":"11_CR86","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1080\/09296174.2013.799918","volume":"20","author":"S Wallis","year":"2013","unstructured":"Wallis, S.: Binomial confidence intervals and contingency tests: mathematical fundamentals and the evaluation of alternative methods. J. Quant. Linguistics 20(3), 178\u2013208 (2013). https:\/\/doi.org\/10.1080\/09296174.2013.799918","journal-title":"J. Quant. Linguistics"},{"key":"11_CR87","doi-asserted-by":"publisher","unstructured":"Weininger, M., Grover, K., Misra, S., Kret\u00ednsk\u00fd, J.: Guaranteed trade-offs in dynamic information flow tracking games. In: CDC, pp. 3786\u20133793. IEEE (2021). https:\/\/doi.org\/10.1109\/CDC45484.2021.9683447","DOI":"10.1109\/CDC45484.2021.9683447"},{"key":"11_CR88","unstructured":"Weissman, T., Ordentlich, E., Seroussi, G., Verdu, S., Weinberger, M.J.: Inequalities for the L1 deviation of the empirical distribution. Technical report, Hewlett-Packard Labs (2003)"},{"issue":"10","key":"11_CR89","doi-asserted-by":"publisher","first-page":"5055","DOI":"10.1109\/TAC.2021.3115080","volume":"67","author":"M Wen","year":"2022","unstructured":"Wen, M., Topcu, U.: Probably approximately correct learning in adversarial environments with temporal logic specifications. IEEE Trans. Autom. Control 67(10), 5055\u20135070 (2022). https:\/\/doi.org\/10.1109\/TAC.2021.3115080","journal-title":"IEEE Trans. Autom. Control"},{"key":"11_CR90","doi-asserted-by":"crossref","unstructured":"Wienh\u00f6ft, P., Suilen, M., Sim\u00e3o, T.D., Dubslaff, C., Baier, C., Jansen, N.: More for less: safe policy improvement with stronger performance guarantees. arXiv preprint arXiv:2305.07958 (2023)","DOI":"10.24963\/ijcai.2023\/490"},{"key":"11_CR91","doi-asserted-by":"publisher","unstructured":"Wienh\u00f6ft, P., Suilen, M., Sim\u00e3o, T.D., Dubslaff, C., Baier, C., Jansen, N.: More for less: safe policy improvement with stronger performance guarantees. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI) (2023). https:\/\/doi.org\/10.24963\/ijcai.2023\/490","DOI":"10.24963\/ijcai.2023\/490"},{"issue":"158","key":"11_CR92","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1080\/01621459.1927.10502953","volume":"22","author":"EB Wilson","year":"1927","unstructured":"Wilson, E.B.: Probable inference, the law of succession, and statistical inference. J. Am. Stat. Assoc. 22(158), 209\u2013212 (1927)","journal-title":"J. Am. Stat. Assoc."},{"key":"11_CR93","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). https:\/\/doi.org\/10.1007\/3-540-45657-0_17"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05792-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T22:39:06Z","timestamp":1787006346000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05792-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,2]]},"ISBN":["9783032057914","9783032057921"],"references-count":93,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05792-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,2]]},"assertion":[{"value":"2 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"QEST+FORMATS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aarhus","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 August 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 August 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"qest2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.qest-formats.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}