Numerical vs. statistical probabilistic model checking: An empirical study
Abstract
Numerical analysis based on uniformisation and statistical techniques
based on sampling and simulation are two distinct approaches for
transient analysis of stochastic systems. We compare the two solution
techniques when applied to the verification of time-bounded until
formulae in the temporal stochastic logic CSL. This study differs
from most previous comparisons of numerical and statistical approaches
in that CSL model checking is a hypothesis testing problem rather than
a parameter estimation problem. We can therefore rely on highly
efficient sequential acceptance sampling tests, which enables
statistical solution techniques to quickly return a result with some
uncertainty. This suggests that statistical techniques can be useful
as a first resort during system prototyping, rather than as a last
resort as often suggested. We also propose a novel combination of the
two solution techniques for verifying CSL queries with nested
probabilistic operators.
Sample citation
Håkan L. S. Younes,
Marta Kwiatkowska,
Gethin Norman, and
David Parker. 2004.
Numerical vs. statistical probabilistic model checking: An empirical study. In
Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, edited by Kurt Jensen and Andreas Podelski, vol. 2988 of
Lecture Notes in Computer Science, 46–60, Barcelona, Spain. Springer.
Full paper (15 pages, 26 references)
© Springer-Verlag 2004
Presentation (39 slides)