Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality (extended version)

Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer +2

Statistical model checking (SMC) randomly samples probabilistic models to approximate quantities of interest with statistical error guarantees. It is traditionally used to estimate…