Bayesian Statistical Model-Checking for Complex Stochastic Systems

Probabilistic Model-Checking is a standard approach for automatically verifying stochastic systems. However, it becomes expensive or even intractable for classic approaches to verify complex systems. Statistical model-checking was proposed to overcome this limitation. In this paper, we propose a novel statistical model-checking approach which is based on Bayesian point estimation. Together with the Bayesian point estimation and a given conjugate prior distribution, we are able to predict the upper bound of sample size before sampling. We implement our techniques in a tool. Experiential results show that our approach is competitive, even better than other standard approaches in several cases.