Sound Statistical Model Checking for Probabilities and Expected Rewards

Carlos E. Budde; Arnd Hartmanns; Tobias Meggendorfer; Maximilian Weininger; Patrick Wienhöft

doi:10.1007/978-3-031-90643-5_9

Sound Statistical Model Checking for Probabilities and Expected Rewards

Carlos E. Budde
, Arnd Hartmanns
, Tobias Meggendorfer
, Maximilian Weininger
, Patrick Wienhöft^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

2 Downloads (Pure)

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.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings
Editors	Arie Gurfinkel, Marijn Heule
Place of Publication	Cham
Publisher	Springer
Pages	167-190
Number of pages	24
Volume	Part 1
Edition	1
ISBN (Electronic)	978-3-031-90643-5
ISBN (Print)	978-3-031-90642-8
DOIs	https://doi.org/10.1007/978-3-031-90643-5_9
Publication status	Published - 2025
Event	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 Duration: 3 May 2025 → 8 May 2025 Conference number: 31 https://etaps.org/2025/conferences/tacas/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	15696 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	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
Abbreviated title	TACAS 2025
Country/Territory	Canada
City	Hamilton
Period	3/05/25 → 8/05/25
Internet address	https://etaps.org/2025/conferences/tacas/

Keywords

This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.

Access to Document

10.1007/978-3-031-90643-5_9Licence: CC BY

Conference paperFinal published version, 695 KBLicence: CC BY

Cite this

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 (1 ed., Vol. Part 1, pp. 167-190). (Lecture Notes in Computer Science; Vol. 15696 LNCS). Springer. https://doi.org/10.1007/978-3-031-90643-5_9

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. Vol. Part 1 1. ed. Cham : Springer, 2025. pp. 167-190 (Lecture Notes in Computer Science).

@inproceedings{6bfd6e9fced64110a5d1ff7e414a550f,

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.",

keywords = "This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union{\textquoteright}s Horizon 2020 research and innovation programme under Marie Sk{\l}odowska-Curie Actions grant number 101008233.",

author = "Budde, \{Carlos E.\} and Arnd Hartmanns and Tobias Meggendorfer and Maximilian Weininger and Patrick Wienh{\"o}ft",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2025.; 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, TACAS 2025 ; Conference date: 03-05-2025 Through 08-05-2025",

year = "2025",

doi = "10.1007/978-3-031-90643-5\_9",

language = "English",

isbn = "978-3-031-90642-8",

volume = "Part 1",

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",

address = "Germany",

edition = "1",

url = "https://etaps.org/2025/conferences/tacas/",

}

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. 1 edn, vol. Part 1, 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, Ontario, Canada, 3/05/25. https://doi.org/10.1007/978-3-031-90643-5_9

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. Vol. Part 1 1. ed. Cham: Springer, 2025. p. 167-190 (Lecture Notes in Computer Science; Vol. 15696 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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

N1 - Conference code: 31

PY - 2025

Y1 - 2025

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.

KW - This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.

UR - https://www.scopus.com/pages/publications/105004792492

U2 - 10.1007/978-3-031-90643-5_9

DO - 10.1007/978-3-031-90643-5_9

M3 - Conference contribution

AN - SCOPUS:105004792492

SN - 978-3-031-90642-8

VL - Part 1

T3 - Lecture Notes in Computer Science

SP - 167

EP - 190

BT - Tools and Algorithms for the Construction and Analysis of Systems

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 -

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. 1 ed. Vol. Part 1. Cham: Springer. 2025. p. 167-190. (Lecture Notes in Computer Science). Epub 2025 May 1. doi: 10.1007/978-3-031-90643-5_9

Sound Statistical Model Checking for Probabilities and Expected Rewards

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version)

Cite this