Numerical vs. statistical probabilistic model checking
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, both theoretically and through empirical evaluation on a set of
case studies. Our 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. 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. 2006.
Numerical vs. statistical probabilistic model checking.
International Journal on Software Tools for Technology Transfer 8, no. 3: 216–228.
Full paper (13 pages, 37 references)
© Springer-Verlag 2006