Standard
Sound Statistical Model Checking for Probabilities and Expected Rewards. / Budde, Carlos E.; Hartmanns, Arnd
; Meggendorfer, Tobias et al.
Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings. ed. / Arie Gurfinkel; Marijn Heule. Cham: Springer, 2025. p. 167-190 (Lecture Notes in Computer Science; Vol. 15696 LNCS).
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Harvard
Budde, CE, Hartmanns, A
, Meggendorfer, T, Weininger, M & Wienhöft, P 2025,
Sound Statistical Model Checking for Probabilities and Expected Rewards. in A Gurfinkel & M Heule (eds),
Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings. Lecture Notes in Computer Science, vol. 15696 LNCS, Springer, Cham, pp. 167-190, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2025, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, Canada,
3/05/25.
https://doi.org/10.1007/978-3-031-90643-5_9APA
Budde, C. E., Hartmanns, A.
, Meggendorfer, T., Weininger, M., & Wienhöft, P. (2025).
Sound Statistical Model Checking for Probabilities and Expected Rewards. In A. Gurfinkel, & M. Heule (Eds.),
Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings (pp. 167-190). (Lecture Notes in Computer Science; Vol. 15696 LNCS). Springer.
https://doi.org/10.1007/978-3-031-90643-5_9Vancouver
Budde CE, Hartmanns A
, Meggendorfer T, Weininger M, Wienhöft P.
Sound Statistical Model Checking for Probabilities and Expected Rewards. In Gurfinkel A, Heule M, editors, Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings. Cham: Springer. 2025. p. 167-190. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-90643-5_9
Author
Budde, Carlos E. ; Hartmanns, Arnd
; Meggendorfer, Tobias et al. /
Sound Statistical Model Checking for Probabilities and Expected Rewards. Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings. editor / Arie Gurfinkel ; Marijn Heule. Cham : Springer, 2025. pp. 167-190 (Lecture Notes in Computer Science).
Bibtex
@inproceedings{bc759de1b5b443c8b3ac88954ee24f1b,
title = "Sound Statistical Model Checking for Probabilities and Expected Rewards",
abstract = "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.",
author = "Budde, {Carlos E.} and Arnd Hartmanns and Tobias Meggendorfer and Maximilian Weininger and Patrick Wienh{\"o}ft",
year = "2025",
month = may,
day = "1",
doi = "10.1007/978-3-031-90643-5_9",
language = "English",
isbn = "9783031906428",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "167--190",
editor = "Arie Gurfinkel and Marijn Heule",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings",
note = "31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2025, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025 ; Conference date: 03-05-2025 Through 08-05-2025",
}
RIS
TY - GEN
T1 - Sound Statistical Model Checking for Probabilities and Expected Rewards
AU - Budde, Carlos E.
AU - Hartmanns, Arnd
AU - Meggendorfer, Tobias
AU - Weininger, Maximilian
AU - Wienhöft, Patrick
PY - 2025/5/1
Y1 - 2025/5/1
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-031-90643-5_9
DO - 10.1007/978-3-031-90643-5_9
M3 - Conference contribution/Paper
AN - SCOPUS:105004792492
SN - 9783031906428
T3 - Lecture Notes in Computer Science
SP - 167
EP - 190
BT - Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings
A2 - Gurfinkel, Arie
A2 - Heule, Marijn
PB - Springer
CY - Cham
T2 - 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2025, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025
Y2 - 3 May 2025 through 8 May 2025
ER -
