Error control for probabilistic model checking
Abstract
We introduce a framework for expressing correctness guarantees of
model-checking algorithms. The framework allows us to qualitatively
compare different solution techniques for probabilistic model
checking, both techniques based on statistical sampling and numerical
computation of probability estimates. We provide several new insights
into the relative merits of the different approaches. In addition, we
present a new statistical solution method that can bound the
probability of error under any circumstances by sometimes reporting
undecided results. Previous statistical solution methods could only
bound the probability of error outside of an “indifference
region.”
Sample citation
Håkan L. S. Younes. 2006.
Error control for probabilistic model checking. In
Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation, edited by E. Allen Emerson and Kedar S. Namjoshi, vol. 3855 of
Lecture Notes in Computer Science, 142–156, Charleston, South Carolina.Springer
Full paper (15 pages, 19 references)
© Springer-Verlag 2006
Presentation (21 slides)