conference paper published yes Carlos E. Budde author Arnd Hartmanns author Tobias Meggendorfer author b21b0c15-30a2-11eb-80dc-f13ca25802e10000-0002-1712-2165 Maximilian Weininger author 02ab0197-cc70-11ed-ab61-918e71f56881 Patrick Wienhöft author KrCh department TACAS: Tools and Algorithms for the Construction and Analysis of Systems IST-BRIDGE: International postdoctoral program project 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 unsound 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 modes SMC tool implements our methods and recommendations, which we use to experimentally confirm our results. https://research-explorer.ista.ac.at/download/19742/19770/2025_TACAS_Budde.pdf application/pdfno Springer Nature2025Hamilton, ON, Canada eng 0302-9743 1611-3349 9783031906428 2411.0055910.1007/978-3-031-90643-5_9 15696167-190 https://research-explorer.ista.ac.at/record/19769 Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. Sound statistical model checking for probabilities and expected rewards. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15696. Springer Nature; 2025:167-190. doi:<a href="https://doi.org/10.1007/978-3-031-90643-5_9">10.1007/978-3-031-90643-5_9</a> Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound statistical model checking for probabilities and expected rewards. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15696, 167–190. Budde, Carlos E., et al. “Sound Statistical Model Checking for Probabilities and Expected Rewards.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15696, Springer Nature, 2025, pp. 167–90, doi:<a href="https://doi.org/10.1007/978-3-031-90643-5_9">10.1007/978-3-031-90643-5_9</a>. C. E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, and P. Wienhöft, “Sound statistical model checking for probabilities and expected rewards,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15696, pp. 167–190. Budde, C. E., Hartmanns, A., Meggendorfer, T., Weininger, M., &#38; Wienhöft, P. (2025). Sound statistical model checking for probabilities and expected rewards. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15696, pp. 167–190). Hamilton, ON, Canada: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-90643-5_9">https://doi.org/10.1007/978-3-031-90643-5_9</a> C.E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 167–190. Budde, Carlos E., Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and Expected Rewards.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15696:167–90. Springer Nature, 2025. <a href="https://doi.org/10.1007/978-3-031-90643-5_9">https://doi.org/10.1007/978-3-031-90643-5_9</a>. 197422025-05-25T22:17:08Z2025-06-02T09:45:41Z