Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-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.

Details

Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems
EditorsPavithra Prabhakar, Andrea Vandin
PublisherSpringer, Cham
Pages83-94
Number of pages12
ISBN (electronic)978-3-032-05792-1
ISBN (print)978-3-032-05791-4
Publication statusE-pub ahead of print - 2 Oct 2025
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science
Volume16143
ISSN0302-9743

Conference

Title2nd International Joint Conference on Quantitative Evaluation of SysTems & Formal Modeling and Analysis of Timed Systems
Abbreviated titleQEST+FORMATS 2025
Conference number2
Descriptionpart of CONFEST 2025
Duration26 - 28 August 2025
Website
Degree of recognitionInternational event
LocationAarhus University
CityAarhus
CountryDenmark

External IDs

Scopus 105020206991

Keywords