Publication Type

Conference Proceeding Article

Version

acceptedVersion

Publication Date

9-2017

Abstract

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 be however 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 based on frequentist estimations. We propose outperforming and rigorous alternative schemes, based on Massart bounds and robust confidence intervals. Our theoretical and empirical analysis show that our proposal reduces the sample size while providing guarantees on error bounds.

Keywords

Error analysis, Estimation, Intelligent systems, Monte Carlo methods, Sampling

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Quantitative Evaluation of Systems: 14th International Conference, QEST 2017, Berlin, Germany, September 5-7: Proceedings

Volume

10503

First Page

333

Last Page

350

ISBN

9783319663340

Identifier

10.1007/978-3-319-66335-7_23

Publisher

Springer

City or Country

Cham

Copyright Owner and License

Authors

Additional URL

https://doi.org/10.1007/978-3-319-66335-7_23

Download

Share

COinS