Statistical Model Checking for Steady State Dependability Verification

We propose to apply the perfect simulation to perform statistical model checking of large Markov chains. Perfect simulation is an extension of Monte Carlo Markov Chain (MCMC) methods, it allows us to obtain exact steady-state samples of the underlying chain thus it avoids the burn-in time problem to detect the steady-state. The statistical model checking by MCMC methods has been already proposed in the last years. However the steady-state formulas can not be checked by this approach because of the problem of detecting steady-state. Thus we propose to do statistical model checking by combining perfect simulation and statistical hypothesis testing in order to verify steady state formulas. We apply our proposed method to verify the saturation and availability properties at long run for a multistage interconnection queueing network illustrating its efficiency when considering very large models.