Statistical probabilistic model checking with a focus on time-bounded properties
Abstract
Probabilistic verification of continuous-time stochastic processes
has received increasing attention in the model-checking community in the
past five years, with a clear focus on developing numerical solution
methods for model checking of continuous-time Markov chains. Numerical
techniques tend to scale poorly with an increase in the size of the
model (the “state space explosion problem”), however, and
are feasible only for restricted classes of stochastic discrete-event
systems. We present a statistical approach to probabilistic model
checking, employing hypothesis testing and discrete-event simulation.
Since we rely on statistical hypothesis testing, we cannot guarantee that
the verification result is correct, but we can at least bound the
probability of generating an incorrect answer to a verification problem.
Sample citation
Håkan L. S. Younes and
Reid G. Simmons. 2006.
Statistical probabilistic model checking with a focus on time-bounded properties.
Information and Computation 204, no. 9: 1368–1409.
Full paper