Statistical model checking estimates quantitative properties of stochastic systems, such as the probability that a given property holds and the expected rewards. Ideally, an estimation algorithm should be both sound (i.e. satisfying the given confidence bound) and efficient (i.e. using fewer simulations or producing narrower confidence intervals). However, many existing algorithms are either unsound (e.g. relying on asymptotic approximations like the central limit theorem) or inefficient (e.g. using conservative bounds like the Hoeffding bound). In this paper, we present sound and efficient algorithms for estimating probabilities and bounded expected rewards under three settings: point estimation with absolute error, point estimation with relative error, and interval estimation, yielding six problems in total. For estimating probabilities, we employ a hybrid strategy integrating two existing algorithms in the point estimation with absolute error setting. We adopt suitable existing algorithms in the other two settings. For estimating bounded expected rewards, the unknown distribution shape makes it challenging to design sound and efficient algorithms. To address this, we propose a lifting framework to lift the three algorithms for estimating probabilities to three new algorithms for estimating bounded expected rewards. We formally prove the soundness of the three lifted algorithms and demonstrate their efficiency through experiments.

@inproceedings{paperbot12332,
  title = {Sound and Efficient Statistical Model Checking for Probabilities and Bounded Rewards},
  author = {Hao Bu and Lin Huang and Tao Wei and Jingyi Wang},
  booktitle = {ASE},
  year = {2026},
  doi = {10.1145/3832783.3834371}
}