Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality (extended version)
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911155375570944 |
|---|---|
| author | Budde, Carlos E. Hartmanns, Arnd Meggendorfer, Tobias Weininger, Maximilian Wienhöft, Patrick |
| author_facet | Budde, Carlos E. Hartmanns, Arnd Meggendorfer, Tobias Weininger, Maximilian Wienhöft, Patrick |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_11859 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality (extended version) Budde, Carlos E. Hartmanns, Arnd Meggendorfer, Tobias Weininger, Maximilian Wienhöft, Patrick Methodology Discrete Mathematics Logic in Computer Science 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. |
| title | Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality (extended version) |
| topic | Methodology Discrete Mathematics Logic in Computer Science |
| url | https://arxiv.org/abs/2509.11859 |