超越均值的数统计模型检验：分位数、CVaR 与 DKW 不等式（扩展版）
统计方法学
2025-09-16 v1 离散数学
计算机科学中的逻辑
摘要
统计模型检验 (SMC) 通过随机抽样概率模型来近似感兴趣的量，并提供统计误差保证。它通常用于估计概率和期望奖励，即不同路径上随机变量的均值。本文发展了使用 Dvoretzky-Kiefer-Wolfowitz-Massart 不等式 (DKW) 的方法，将 SMC 扩展到计算分位数、条件价值-at-risk 和熵敏感风险等量。DKW 对随机变量的整个累积分布函数提供置信区间，相较于当前 SMC 中流行的统计方法具有更大的灵活性。我们在 Modest Toolset 的 'modes' 模拟器中实现了通过 DKW 计算新量的支持。我们在来自定量验证文献中的基准测试中展示了该实现的灵活性。
引用
@article{arxiv.2509.11859,
title = {Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality (extended version)},
author = {Carlos E. Budde and Arnd Hartmanns and Tobias Meggendorfer and Maximilian Weininger and Patrick Wienhöft},
journal= {arXiv preprint arXiv:2509.11859},
year = {2025}
}
备注
Extended version of the article "Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality" presented/published at the 2nd International Joint Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems (QEST+FORMATS 2025), 26-28 August 2025, Aarhus, Denmark (https://www.qest.org/qest-formats-2025/)