Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version)
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911150710456320 |
|---|---|
| author | Budde, Carlos E. Hartmanns, Arnd Meggendorfer, Tobias Weininger, Maximilian Wienhöft, Patrick |
| author_facet | Budde, Carlos E. Hartmanns, Arnd Meggendorfer, Tobias Weininger, Maximilian Wienhöft, Patrick |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_00559 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version) Budde, Carlos E. Hartmanns, Arnd Meggendorfer, Tobias Weininger, Maximilian Wienhöft, Patrick Logic in Computer Science 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. |
| title | Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2411.00559 |