Statistical probabilistic model checking with a focus on time-bounded properties

September 2006

Statistical probabilistic model checking with a focus on time-bounded properties

Authors:

Håkan L. S. Younes and Reid G. Simmons

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.

Notes:

@article{Younes-2006-122385,
author = {Håkan L. S. Younes And Reid G. Simmons},
title = {Statistical probabilistic model checking with a focus on time-bounded properties},
journal = {Proceedings of Information and Computation},
year = {2006},
month = {September},
volume = {204},
number = {9},
pages = {1368 - 1409},
}
Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.