Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
Statistical model checking (SMC) randomly samples probabilistic models to approximate quantities of interest with statistical error
guarantees. It is traditionally used to estimate probabilities and expected rewards, i.e. means of different random variables on paths. In this paper, we develop methods using the Dvoretzky-Kiefer-Wolfowitz-Massart inequality (DKW) to extend SMC beyond means to compute quantities such as quantiles, conditional value-at-risk, and entropic risk. The DKW provides confidence bounds on the random variable’s entire cumulative distribution function, a much more versatile guarantee compared to the statistical methods prevalent in SMC today. We have implemented support for computing new quantities via the DKW in the modes simulator of the Modest Toolset. We highlight the implementation and its versatility on benchmarks from the quantitative verification literature.
guarantees. It is traditionally used to estimate probabilities and expected rewards, i.e. means of different random variables on paths. In this paper, we develop methods using the Dvoretzky-Kiefer-Wolfowitz-Massart inequality (DKW) to extend SMC beyond means to compute quantities such as quantiles, conditional value-at-risk, and entropic risk. The DKW provides confidence bounds on the random variable’s entire cumulative distribution function, a much more versatile guarantee compared to the statistical methods prevalent in SMC today. We have implemented support for computing new quantities via the DKW in the modes simulator of the Modest Toolset. We highlight the implementation and its versatility on benchmarks from the quantitative verification literature.
Details
| Original language | English |
|---|---|
| Title of host publication | Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems |
| Editors | Pavithra Prabhakar, Andrea Vandin |
| Publisher | Springer, Cham |
| Pages | 83-94 |
| Number of pages | 12 |
| ISBN (electronic) | 978-3-032-05792-1 |
| ISBN (print) | 978-3-032-05791-4 |
| Publication status | E-pub ahead of print - 2 Oct 2025 |
| Peer-reviewed | Yes |
Publication series
| Series | Lecture Notes in Computer Science |
|---|---|
| Volume | 16143 |
| ISSN | 0302-9743 |
Conference
| Title | 2nd International Joint Conference on Quantitative Evaluation of SysTems & Formal Modeling and Analysis of Timed Systems |
|---|---|
| Abbreviated title | QEST+FORMATS 2025 |
| Conference number | 2 |
| Description | part of CONFEST 2025 |
| Duration | 26 - 28 August 2025 |
| Website | |
| Degree of recognition | International event |
| Location | Aarhus University |
| City | Aarhus |
| Country | Denmark |
External IDs
| Scopus | 105020206991 |
|---|