upper bound of policies for statistical model checking of markov decision processes

State explosion remains a fundamental challenge in model checking. statistical model checking (smc) offers a promising approach to mitigate this issue. still, its application to markov decision processes (mdps) is hindered by the computational difficulty of resolving nondeterminism with near-optimal policies. existing methods for policy selection within smc often suffer from limited memory efficiency or fail to guarantee the specified confidence level for result accuracy. to address this, we introduce a novel statistical criterion for policy evaluation and propose an efficient method for determining an upper bound on the number of policies required to achieve a desired confidence level in the computed reachability probabilities. our method leverages the mean and standard deviation of reachability probabilities obtained from a set of randomly sampled policies to derive this bound. experimental results validate the effectiveness of our approach and demonstrate that it provides more reliable results in most cases.