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.”
Full paper: PDF (15 pages, 19 references)
© Springer-Verlag Berlin Heidelberg 2006
Presentation: PPT, PDF (21 slides)
| Håkan L. S. Younes |
|
|
| Last modified: Mon Mar 13 12:37:54 EST 2006 |