Sound Statistical Model Checking for Probabilities and Expected Rewards

Caros E. BuddeCaros E. Budde, Arnd HartmannsArnd Hartmanns, Tobias MeggendorferTobias Meggendorfer, Maximilian WeiningerMaximilian Weininger, Patrick WienhöftPatrick Wienhöft

ISSN: 1611-3349
DOI Link

Caros E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft
Sound Statistical Model Checking for Probabilities and Expected Rewards
In Arie Gurfinkel, Marijn Heule, eds., LNCS, volume 15696, 167-190, 2025. Springer Nature Switzerland

Details
Bibtex

KurzfassungAbstract
Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use unsound statistical methods that produce incorrect results more often than they claim. In this paper, we provide a comprehensive overview of tools and their correctness, as well as of sound methods available for estimating probabilities from the literature. For expected rewards, we investigate how to bound the path reward distribution to apply sound statistical methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz inequality that has not been used in SMC so far. We prove that even reachability rewards can be bounded in theory, and formalise the concept of limit-PAC procedures for a practical solution. The modes SMC tool implements our methods and recommendations, which we use to experimentally confirm our results.
Weitere Informationen unter:Further Information: Link
Projekt:Project: CPEC, CeTI
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{BHMWW2025,
  author    = {Caros E. Budde and Arnd Hartmanns and Tobias Meggendorfer and
               Maximilian Weininger and Patrick Wienh{\"{o}}ft},
  title     = {Sound Statistical Model Checking for Probabilities and Expected
               Rewards},
  editor    = {Arie Gurfinkel and Marijn Heule},
  booktitle = {LNCS},
  volume    = {15696},
  publisher = {Springer Nature Switzerland},
  year      = {2025},
  pages     = {167-190},
  doi       = {10.1007/978-3-031-90643-5_9}
}