Sequential Schemes for Frequentist Estimation of Properties in Statistical Model Checking
| Autor: | Cyrille Jegourel, Jun Sun, Jin Song Dong |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Accuracy and precision
Computer science Monte Carlo method Probabilistic logic 020207 software engineering 02 engineering and technology Robust confidence intervals Computer Science Applications Frequentist inference Sample size determination Approximation error Modeling and Simulation 0202 electrical engineering electronic engineering information engineering State space 020201 artificial intelligence & image processing Algorithm |
| Zdroj: | ACM Transactions on Modeling and Computer Simulation. 29:1-22 |
| ISSN: | 1558-1195 1049-3301 |
| DOI: | 10.1145/3310226 |
| Popis: | Statistical Model Checking (SMC) is an approximate verification method that overcomes the state space explosion problem for probabilistic systems by Monte Carlo simulations. Simulations might, however, be costly if many samples are required. It is thus necessary to implement efficient algorithms to reduce the sample size while preserving precision and accuracy. In the literature, some sequential schemes have been provided for the estimation of property occurrence based on predefined confidence and absolute or relative error. Nevertheless, these algorithms remain conservative and may result in huge sample sizes if the required precision standards are demanding. In this article, we compare some useful bounds and some sequential methods. We propose outperforming and rigorous alternative schemes based on Massart bounds and robust confidence intervals. Our theoretical and empirical analyses show that our proposal reduces the sample size while providing the required guarantees on error bounds. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|