فهرست نشریات علمی دسترسی آزاد ایران

State explosion is a predominant challenge of model checking in all variants. Statistical model checking (SMC) is proposed to tackle this problem, which leads to promising results in most cases. Computing near-optimal policies for resolving non-deterministic choices is the main obstacle for applying SMC in the verification of Markov decision processes (MDPs). Although several solutions are available to cope with this problem they mainly suffer from memory limitation or non-accurate results with the given confidence level. In this paper, we define a criterion for the fitness of policies. We propose a novel method that provides an upper-bound for the number of policies needed to guarantee the precision of computed values with the desired level of confidence. The proposed criterion relies on statistical analysis on a set of randomly generated policies. It considers the mean and expected values of the computed reachability probabilities for the states of the model to determine an appropriate upper bound for the number of policies. We run a set of experiments for the proposed method.