Home > Research > Publications & Outputs > Sound Statistical Model Checking for Probabilit...

Links

Text available via DOI:

View graph of relations

Sound Statistical Model Checking for Probabilities and Expected Rewards

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published
Close
Publication date1/05/2025
Host publicationTools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings
EditorsArie Gurfinkel, Marijn Heule
Place of PublicationCham
PublisherSpringer
Pages167-190
Number of pages24
ISBN (electronic)9783031906435
ISBN (print)9783031906428
<mark>Original language</mark>English
Event31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2025, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025 - Hamilton, Canada
Duration: 3/05/20258/05/2025

Conference

Conference31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2025, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025
Country/TerritoryCanada
CityHamilton
Period3/05/258/05/25

Publication series

NameLecture Notes in Computer Science
Volume15696 LNCS
ISSN (Print)0302-9743
ISSN (electronic)1611-3349

Conference

Conference31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2025, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025
Country/TerritoryCanada
CityHamilton
Period3/05/258/05/25

Abstract

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.