{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T16:23:45Z","timestamp":1792254225227,"version":"4.4.0"},"publisher-location":"Cham","reference-count":84,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906428","type":"print"},{"value":"9783031906435","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use <jats:italic>unsound<\/jats:italic> statistical methods that produce incorrect results more often than they claim. In this paper, we provide a comprehensive overview of tools and their correctness, as well as of sound methods available for estimating probabilities from the literature. For expected rewards, we investigate how to bound the path reward distribution to apply sound statistical methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz inequality that has not been used in SMC so far. We prove that even reachability rewards can be bounded in theory, and formalise the concept of limit-PAC procedures for a practical solution. The <jats:sc>modes<\/jats:sc> SMC tool implements our methods and recommendations, which we use to experimentally confirm our results.<\/jats:p>","DOI":"10.1007\/978-3-031-90643-5_9","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:16Z","timestamp":1745993296000},"page":"167-190","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Sound Statistical Model Checking for Probabilities and Expected Rewards"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8807-1548","authenticated-orcid":false,"given":"Carlos E.","family":"Budde","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1712-2165","authenticated-orcid":false,"given":"Tobias","family":"Meggendorfer","sequence":"additional","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,5,1]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Agarwal, C., Guha, S., Kret\u00ednsk\u00fd, J., Muruganandham, P.: PAC statistical model checking of mean payoff in discrete- and continuous-time MDP. In: CAV (2). Lecture Notes in Computer Science, vol. 13372, pp. 3\u201325. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_1","DOI":"10.1007\/978-3-031-13188-2_1"},{"key":"9_CR2","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"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Agresti, A., Coull, B.A.: Approximate is better than \u201cexact\u201d for interval estimation of binomial proportions. The American Statistician 52(2), 119\u2013126 (1998). https:\/\/doi.org\/10.2307\/2685469","DOI":"10.2307\/2685469"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Anderson, T.W.: Confidence limits for the value of an arbitrary bounded random variable with a continuous distribution function. Bulletin of The International and Statistical Institute 43, 249\u2013251 (1969)","DOI":"10.21236\/AD0696676"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Ashok, P., Butkova, Y., Hermanns, H., Kret\u00ednsk\u00fd, J.: Continuous-time Markov decisions based on partial exploration. In: Lahiri, S.K., Wang, C. (eds.) 16th International Symposium on Automated Technology for Verification and Analysis (ATVA). Lecture Notes in Computer Science, vol. 11138, pp. 317\u2013334. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_19","DOI":"10.1007\/978-3-030-01090-4_19"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Ashok, P., Chatterjee, K., Daca, P., Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Value iteration for long-run average reward in Markov decision processes. In: CAV (1). Lecture Notes in Computer Science, vol. 10426, pp. 201\u2013221. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_10","DOI":"10.1007\/978-3-319-63387-9_10"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Ashok, P., Daca, P., Kret\u00ednsk\u00fd, J., Weininger, M.: Statistical model checking: Black or white? In: Margaria, T., Steffen, B. (eds.) 9th International Symposium on Leveraging Applications of Formal Methods (ISoLA). Lecture Notes in Computer Science, vol. 12476, pp. 331\u2013349. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_19","DOI":"10.1007\/978-3-030-61362-4_19"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Ashok, P., Kret\u00ednsk\u00fd, J., Weininger, M.: PAC statistical model checking for markov decision processes and stochastic games. In: CAV (1). Lecture Notes in Computer Science, vol. 11561, pp. 497\u2013519. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_29","DOI":"10.1007\/978-3-030-25540-4_29"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Azeem, M., Evangelidis, A., Kret\u00ednsk\u00fd, J., Slivinskiy, A., Weininger, M.: Optimistic and topological value iteration for simple stochastic games. In: ATVA. Lecture Notes in Computer Science, vol. 13505, pp. 285\u2013302. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_18","DOI":"10.1007\/978-3-031-19992-9_18"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Baier, C.: Probabilistic model checking. In: Esparza, J., Grumberg, O., Sickert, S. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series \u2013 D: Information and Communication Security, vol.\u00a045, pp. 1\u201323. IOS Press (2016). https:\/\/doi.org\/10.3233\/978-1-61499-627-9-1","DOI":"10.3233\/978-1-61499-627-9-1"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Baier, C., de\u00a0Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 963\u2013999. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76\u201385 (2010). https:\/\/doi.org\/10.1145\/1810891.1810912","DOI":"10.1145\/1810891.1810912"},{"key":"9_CR13","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: Interval iteration for Markov decision processes. In: CAV (1). Lecture Notes in Computer Science, vol. 10426, pp. 160\u2013180. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Ballarini, P., Barbot, B., Duflot, M., Haddad, S., Pekergin, N.: HASL: A new approach for performance evaluation and model checking from concepts to experimentation. Performance Evaluation 90, 53\u201377 (2015). https:\/\/doi.org\/10.1016\/j.peva.2015.04.003","DOI":"10.1016\/j.peva.2015.04.003"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Bennett, G.: Probability inequalities for the sum of independent random variables. Journal of the American Statistical Association 57(297), 33\u201345 (1962). https:\/\/doi.org\/10.1080\/01621459.1962.10482149","DOI":"10.1080\/01621459.1962.10482149"},{"key":"9_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)"},{"key":"9_CR18","unstructured":"Bernstein, S.: Theory of Probability. 2 edn. (1934)"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.P.: MoDeST: A compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng. 32(10), 812\u2013830 (2006). https:\/\/doi.org\/10.1109\/TSE.2006.104","DOI":"10.1109\/TSE.2006.104"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kret\u00ednsk\u00fd, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.F. (eds.) 12th International Symposium on Automated Technology for Verification and Analysis (ATVA). Lecture Notes in Computer Science, vol.\u00a08837, pp. 98\u2013114. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Bu, H., Sun, M.: Clopper-pearson algorithms for efficient statistical model checking estimation. IEEE Transactions on Software Engineering (01), 1\u201320 (2024). https:\/\/doi.org\/10.1109\/TSE.2024.3392720","DOI":"10.1109\/TSE.2024.3392720"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Budde, C.E.: FIG: the Finite Improbability Generator v1.3. SIGMETRICS Perform. Evaluation Rev. 49(4), 59\u201364 (2022). https:\/\/doi.org\/10.1145\/3543146.3543160","DOI":"10.1145\/3543146.3543160"},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Budde, C.E.: Using statistical model checking for cybersecurity analysis. In: Skarmeta, A.F., Canavese, D., Lioy, A., Matheu, S.N. (eds.) First International Workshop on Digital Sovereignty in Cyber Security: New Challenges in Future Vision (CyberSec4Europe). Communications in Computer and Information Science, vol.\u00a01807, pp. 16\u201332. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-36096-1_2","DOI":"10.1007\/978-3-031-36096-1_2"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: An efficient statistical model checker for nondeterminism and rare events. Int. J. Softw. Tools Technol. Transf. 22(6), 759\u2013780 (2020). https:\/\/doi.org\/10.1007\/S10009-020-00563-2","DOI":"10.1007\/S10009-020-00563-2"},{"key":"9_CR25","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: Quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 10206, pp. 151\u2013168 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Hartmanns, A., Klauck, M., Kret\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Turrini, A., Zhang, Z.: On correctness, precision, and performance in quantitative verification \u2013 qcomp 2020 competition report. In: Margaria, T., Steffen, B. (eds.) 9th International Symposium on Leveraging Applications of Formal Methods (ISoLA). Lecture Notes in Computer Science, vol. 12479, pp. 216\u2013241. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-83723-5_15","DOI":"10.1007\/978-3-030-83723-5_15"},{"key":"9_CR27","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Hartmanns, A., Meggendorfer, T., Weininger, M., Wienh\u00f6ft, P.: Sound statistical model checking for probabilities and expected rewards. CoRR abs\/2411.00559 (2024). https:\/\/doi.org\/10.48550\/arXiv.2411.00559","DOI":"10.48550\/arXiv.2411.00559"},{"key":"9_CR28","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Hartmanns, A., Meggendorfer, T., Weininger, M., Wienh\u00f6ft, P.: Sound statistical model checking for probabilities and expected rewards (experimental reproduction package) (2025). https:\/\/doi.org\/10.5281\/zenodo.14743520","DOI":"10.5281\/zenodo.14743520"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Casella, G.: Refining binomial confidence intervals. Canadian Journal of Statistics 14(2), 113\u2013129 (1986). https:\/\/doi.org\/10.2307\/3314658","DOI":"10.2307\/3314658"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Chen, J.: Properties of a new adaptive sampling method with applications to scalable learning. Web Intell. 13(4), 215\u2013227 (2015). https:\/\/doi.org\/10.3233\/WEB-150322","DOI":"10.3233\/WEB-150322"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Chenoy, A., Duchene, F., Given-Wilson, T., Legay, A.: C-SMC: A hybrid statistical model checking and concrete runtime engine for analyzing C programs. In: Laarman, A., Sokolova, A. (eds.) 27th International Symposium on Model Checking Software (SPIN). Lecture Notes in Computer Science, vol. 12864, pp. 101\u2013119. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-84629-9_6","DOI":"10.1007\/978-3-030-84629-9_6"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"Chernoff, H.: A Measure of Asymptotic Efficiency for Tests of a Hypothesis Based on the sum of Observations. The Annals of Mathematical Statistics 23(4), 493\u2013507 (1952). https:\/\/doi.org\/10.1214\/aoms\/1177729330","DOI":"10.1214\/aoms\/1177729330"},{"key":"9_CR33","doi-asserted-by":"publisher","unstructured":"Chow, Y.S., Robbins, H.: On the Asymptotic Theory of Fixed-Width Sequential Confidence Intervals for the Mean. The Annals of Mathematical Statistics 36(2), 457\u2013462 (1965). https:\/\/doi.org\/10.1214\/aoms\/1177700156","DOI":"10.1214\/aoms\/1177700156"},{"key":"9_CR34","doi-asserted-by":"publisher","unstructured":"Clopper, C., Pearson, E.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26(4), 404\u2013413 (1934). https:\/\/doi.org\/10.1093\/biomet\/26.4.404","DOI":"10.1093\/biomet\/26.4.404"},{"key":"9_CR35","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3060139","DOI":"10.1145\/3060139"},{"key":"9_CR36","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Monti, R.E.: Input\/output stochastic automata with urgency: Confluence and weak determinism. In: Fischer, B., Uustalu, T. (eds.) 15th International Colloquium on Theoretical Aspects of Computing (ICTAC). Lecture Notes in Computer Science, vol. 11187, pp. 132\u2013152. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-02508-3_8","DOI":"10.1007\/978-3-030-02508-3_8"},{"key":"9_CR37","doi-asserted-by":"publisher","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015). https:\/\/doi.org\/10.1007\/S10009-014-0361-Y","DOI":"10.1007\/S10009-014-0361-Y"},{"key":"9_CR38","doi-asserted-by":"publisher","unstructured":"Domingo, C., Gavald\u00e0, R., Watanabe, O.: Adaptive sampling methods for scaling up knowledge discovery algorithms. In: Discovery Science. Lecture Notes in Computer Science, vol.\u00a01721, pp. 172\u2013183. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-46846-3_16","DOI":"10.1007\/3-540-46846-3_16"},{"key":"9_CR39","doi-asserted-by":"publisher","unstructured":"Dvoretzky, A., Kiefer, J., Wolfowitz, J.: Asymptotic Minimax Character of the Sample Distribution Function and of the Classical Multinomial Estimator. The Annals of Mathematical Statistics 27(3), 642\u2013669 (1956). https:\/\/doi.org\/10.1214\/aoms\/1177728174","DOI":"10.1214\/aoms\/1177728174"},{"key":"9_CR40","doi-asserted-by":"publisher","unstructured":"Eisentraut, J., Kelmendi, E., Kret\u00ednsk\u00fd, J., Weininger, M.: Value iteration for simple stochastic games: Stopping criterion and learning algorithm. Inf. Comput. 285(Part), 104886 (2022). https:\/\/doi.org\/10.1016\/j.ic.2022.104886","DOI":"10.1016\/j.ic.2022.104886"},{"key":"9_CR41","doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM). Lecture Notes in Computer Science, vol.\u00a06659, pp. 53\u2013113. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-21455-4_3","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"9_CR42","doi-asserted-by":"crossref","unstructured":"Frey, J.: Fixed-width sequential confidence intervals for a proportion. The American Statistician 64(3), 242\u2013249 (2010), http:\/\/www.jstor.org\/stable\/20799919","DOI":"10.1198\/tast.2010.09140"},{"key":"9_CR43","doi-asserted-by":"publisher","unstructured":"Gilmore, S., Reijsbergen, D., Vandin, A.: Transient and steady-state statistical analysis for discrete event simulators. In: IFM. pp. 145\u2013160. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_10","DOI":"10.1007\/978-3-319-66845-1_10"},{"key":"9_CR44","doi-asserted-by":"publisher","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","DOI":"10.1016\/J.TCS.2016.12.003"},{"key":"9_CR45","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013). https:\/\/doi.org\/10.1007\/S10703-012-0167-Z","DOI":"10.1007\/S10703-012-0167-Z"},{"key":"9_CR46","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: An integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol.\u00a08413, pp. 593\u2013598. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"9_CR47","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: Lahiri, S.K., Wang, C. (eds.) 32nd International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 12225, pp. 488\u2013511. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"9_CR48","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 11427, pp. 344\u2013350. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"9_CR49","doi-asserted-by":"publisher","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol.\u00a02937, pp. 73\u201384. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_8","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"9_CR50","doi-asserted-by":"publisher","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. Journal of the American Statistical Association 58(301), 13\u201330 (1963). https:\/\/doi.org\/10.1080\/01621459.1963.10500830","DOI":"10.1080\/01621459.1963.10500830"},{"key":"9_CR51","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":"9_CR52","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J.: Survey of statistical verification of linear unbounded properties: Model checking and distances. In: ISoLA (1). Lecture Notes in Computer Science, vol.\u00a09952, pp. 27\u201345 (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_3","DOI":"10.1007\/978-3-319-47166-2_3"},{"key":"9_CR53","doi-asserted-by":"crossref","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Of cores: A partial-exploration framework for Markov decision processes. Log. Methods Comput. Sci. 16(4) (2020), https:\/\/lmcs.episciences.org\/6833","DOI":"10.23638\/LMCS-16(4:3)2020"},{"key":"9_CR54","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Weininger, M.: Stopping criteria for value iteration on stochastic games with quantitative objectives. In: 38th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023. pp. 1\u201314. IEEE (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175771","DOI":"10.1109\/LICS56636.2023.10175771"},{"key":"9_CR55","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) 23rd International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol.\u00a06806, pp. 585\u2013591. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"9_CR56","doi-asserted-by":"publisher","unstructured":"Lampacrescia, M., Klauck, M., Palmas, M.: Towards verifying robotic systems using statistical model checking in STORM. In: Steffen, B. (ed.) Second International Conference on Bridging the Gap Between AI and Reality (AISoLA). Lecture Notes in Computer Science, vol. 15217, pp. 446\u2013467. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-75434-0_28","DOI":"10.1007\/978-3-031-75434-0_28"},{"key":"9_CR57","doi-asserted-by":"publisher","unstructured":"Lanotte, R., Merro, M., Zannone, N.: Impact analysis of coordinated cyber-physical attacks via statistical model checking: A case study. In: Huisman, M., Ravara, A. (eds.) 43rd IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE). Lecture Notes in Computer Science, vol. 13910, pp. 75\u201394. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-35355-0_6","DOI":"10.1007\/978-3-031-35355-0_6"},{"key":"9_CR58","unstructured":"Learned-Miller, E.G., Thomas, P.S.: A new confidence interval for the mean of a bounded random variable. CoRR abs\/1905.06208 (2019), http:\/\/arxiv.org\/abs\/1905.06208"},{"key":"9_CR59","doi-asserted-by":"publisher","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Steffen, B., Woeginger, G.J. (eds.) Computing and Software Science \u2013 State of the Art and Perspectives, Lecture Notes in Computer Science, vol. 10000, pp. 478\u2013504. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_23","DOI":"10.1007\/978-3-319-91908-9_23"},{"key":"9_CR60","doi-asserted-by":"publisher","unstructured":"Legay, A., Sedwards, S., Traonouez, L.M.: Plasma Lab: A modular statistical model checking platform. In: Margaria, T., Steffen, B. (eds.) 7th International Symposium on Leveraging Applications of Formal Methods (ISoLA). Lecture Notes in Computer Science, vol.\u00a09952, pp. 77\u201393 (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_6","DOI":"10.1007\/978-3-319-47166-2_6"},{"key":"9_CR61","doi-asserted-by":"crossref","unstructured":"Levin, D.A., Peres, Y.: Markov chains and mixing times, vol.\u00a0107. American Mathematical Soc. (2017)","DOI":"10.1090\/mbk\/107"},{"key":"9_CR62","doi-asserted-by":"publisher","unstructured":"Massart, P.: The tight constant in the Dvoretzky-Kiefer-Wolfowitz inequality. The Annals of Probability 18(3), 1269\u20131283 (1990). https:\/\/doi.org\/10.1214\/aop\/1176990746","DOI":"10.1214\/aop\/1176990746"},{"key":"9_CR63","doi-asserted-by":"publisher","unstructured":"Mazurek, F., Tschand, A., Wang, Y., Pajic, M., Sorin, D.J.: Rigorous evaluation of computer processors with statistical model checking. In: 56th Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO). pp. 1242\u20131254. ACM (2023). https:\/\/doi.org\/10.1145\/3613424.3623785","DOI":"10.1145\/3613424.3623785"},{"key":"9_CR64","doi-asserted-by":"publisher","unstructured":"Meggendorfer, T., Weininger, M.: Playing games with your PET: Extending the partial exploration tool to stochastic games. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. Lecture Notes in Computer Science, vol. 14683, pp. 359\u2013372. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_16","DOI":"10.1007\/978-3-031-65633-0_16"},{"key":"9_CR65","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":"9_CR66","doi-asserted-by":"publisher","unstructured":"Mnih, V., Szepesv\u00e1ri, C., Audibert, J.Y.: Empirical Bernstein stopping. In: Cohen, W.W., McCallum, A., Roweis, S.T. (eds.) 25th International Conference on Machine Learning (ICML). ACM International Conference Proceeding Series, vol.\u00a0307, pp. 672\u2013679. ACM (2008). https:\/\/doi.org\/10.1145\/1390156.1390241","DOI":"10.1145\/1390156.1390241"},{"key":"9_CR67","doi-asserted-by":"crossref","unstructured":"Newcombe, R.G.: Two-sided confidence intervals for the single proportion: Comparison of seven methods. Statistics in medicine 17(8), 857\u2013872 (1998)","DOI":"10.1002\/(SICI)1097-0258(19980430)17:8<857::AID-SIM777>3.0.CO;2-E"},{"key":"9_CR68","doi-asserted-by":"publisher","unstructured":"Niehage, M., Pilch, C., Remke, A.: Simulating hybrid Petri nets with general transitions and non-linear differential equations. In: 13th EAI International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS). pp. 88\u201395. ACM (2020). https:\/\/doi.org\/10.1145\/3388831.3388842","DOI":"10.1145\/3388831.3388842"},{"key":"9_CR69","doi-asserted-by":"publisher","unstructured":"Nouri, A., Mediouni, B.L., Bozga, M., Combaz, J., Bensalem, S., Legay, A.: Performance evaluation of stochastic real-time systems with the $$\\cal{S}$$BIP framework. International Journal of Critical Computer-Based Systems 8(3-4), 340\u2013370 (2018). https:\/\/doi.org\/10.1504\/IJCCBS.2018.096439","DOI":"10.1504\/IJCCBS.2018.096439"},{"key":"9_CR70","doi-asserted-by":"crossref","unstructured":"Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Annals of the Institute of Statistical Mathematics 10(1), 29\u201335 (1959)","DOI":"10.1007\/BF02883985"},{"key":"9_CR71","doi-asserted-by":"publisher","unstructured":"Parmentier, M., Legay, A.: Adaptive stopping algorithms based on concentration inequalities. In: Steffen, B. (ed.) Second International Conference on Bridging the Gap Between AI and Reality (AISoLA). Lecture Notes in Computer Science, vol. 15217, pp. 336\u2013353. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-75434-0_23","DOI":"10.1007\/978-3-031-75434-0_23"},{"key":"9_CR72","unstructured":"Phan, M., Thomas, P.S., Learned-Miller, E.G.: Towards practical mean bounds for small samples. In: Meila, M., Zhang, T. (eds.) 38th International Conference on Machine Learning (ICML). Proceedings of Machine Learning Research, vol.\u00a0139, pp. 8567\u20138576. PMLR (2021), http:\/\/proceedings.mlr.press\/v139\/phan21a.html"},{"key":"9_CR73","doi-asserted-by":"publisher","unstructured":"Pilch, C., Edenfeld, F., Remke, A.: HYPEG: Statistical model checking for hybrid Petri nets: Tool paper. In: Marin, A., Houdt, B.V., Casale, G., Petriu, D.C., Rossi, S. (eds.) 11th EAI International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS). pp. 186\u2013191. ACM (2017). https:\/\/doi.org\/10.1145\/3150928.3150956","DOI":"10.1145\/3150928.3150956"},{"key":"9_CR74","doi-asserted-by":"publisher","unstructured":"Pilch, C., Remke, A.: Statistical model checking for hybrid petri nets with multiple general transitions. In: DSN. pp. 475\u2013486. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/DSN.2017.41","DOI":"10.1109\/DSN.2017.41"},{"key":"9_CR75","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.P.: Sound value iteration. In: Chockler, H., Weissenbacher, G. (eds.) 30th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 10981, pp. 643\u2013661. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"9_CR76","doi-asserted-by":"publisher","unstructured":"Reijsbergen, D., de\u00a0Boer, 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","DOI":"10.1007\/S10009-014-0350-1"},{"key":"9_CR77","doi-asserted-by":"publisher","unstructured":"Roberts, R., Lewis, B., Hartmanns, A., Basu, P., Roy, S., Chakraborty, K., Zhang, Z.: Probabilistic verification for reliability of a two-by-two network-on-chip system. In: Lluch-Lafuente, A., Mavridou, A. (eds.) 26th International Conference on Formal Methods for Industrial Critical Systems (FMICS). Lecture Notes in Computer Science, vol. 12863, pp. 232\u2013248. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_16","DOI":"10.1007\/978-3-030-85248-1_16"},{"key":"9_CR78","doi-asserted-by":"publisher","unstructured":"Rubino, G., Tuffin, B. (eds.): Rare Event Simulation using Monte Carlo Methods. Wiley (2009). https:\/\/doi.org\/10.1002\/9780470745403","DOI":"10.1002\/9780470745403"},{"key":"9_CR79","doi-asserted-by":"publisher","unstructured":"Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: Horv\u00e1th, A., Buchholz, P., Cortellessa, V., Muscariello, L., Squillante, M.S. (eds.) 7th International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS). pp. 310\u2013315. ICST\/ACM (2013). https:\/\/doi.org\/10.4108\/ICST.VALUETOOLS.2013.254377","DOI":"10.4108\/ICST.VALUETOOLS.2013.254377"},{"key":"9_CR80","doi-asserted-by":"publisher","unstructured":"Wald, A.: Sequential Tests of Statistical Hypotheses. The Annals of Mathematical Statistics 16(2), 117\u2013186 (1945). https:\/\/doi.org\/10.1214\/aoms\/1177731118","DOI":"10.1214\/aoms\/1177731118"},{"key":"9_CR81","doi-asserted-by":"crossref","unstructured":"Wang, W.: An iterative construction of confidence intervals for a proportion. Statistica Sinica 24(3), 1389\u20131410 (2014), http:\/\/www.jstor.org\/stable\/24310993","DOI":"10.5705\/ss.2012.257"},{"key":"9_CR82","doi-asserted-by":"publisher","unstructured":"Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Technol. Transf. 8(3), 216\u2013228 (2006). https:\/\/doi.org\/10.1007\/S10009-005-0187-8","DOI":"10.1007\/S10009-005-0187-8"},{"key":"9_CR83","doi-asserted-by":"publisher","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) 14th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol.\u00a02404, pp. 223\u2013235. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_17","DOI":"10.1007\/3-540-45657-0_17"},{"key":"9_CR84","doi-asserted-by":"publisher","unstructured":"Zuliani, P.: Statistical model checking for biological applications. Int. J. Softw. Tools Technol. Transf. 17(4), 527\u2013536 (2015). https:\/\/doi.org\/10.1007\/S10009-014-0343-0","DOI":"10.1007\/S10009-014-0343-0"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90643-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:22Z","timestamp":1745993302000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90643-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906428","9783031906435"],"references-count":84,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90643-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The models, tools, and scripts to reproduce our experimental evaluation are archived and available at DOI \u00a0[].","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data availability statement"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}