Numerical vs. Statistical Probabilistic Model Checking

Håkan L. S. Younes Marta Kwiatkowska Gethin Norman David Parker


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:

pdf (13 pages, 37 references)
© Springer-Verlag 2006


[ Google Scholar ]
  1. David N. Jansen, Joost-Pieter Katoen, Marcel Oldenkamp, Mariëlle Stoelinga, and Ivan S. Zapreev. 2008. How fast and fat is your probabilistic model checker? An experimental performance comparison. In Proceedings of the 3rd International Haifa Verification Conference, 69–85. Springer.
  2. Rena Bakhshi, Francois Bonnet, Wan Fokkink, and Boudewijn Haverkort. 2007. Formal analysis techniques for gossiping protocols. ACM SIGOPS Operating Systems Review 41(5):28–36.
  3. Joost-Pieter Katoen and Ivan S. Zapreev. 2006. Safe on-the-fly steady-state detection for time-bounded reachability. In Proceedings of the Third International Conference on Quantitative Evaluation of Systems, 301–310. IEEE Computer Society.