Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study

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. 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.

Full paper: PDF (15 pages, 26 references)
© Springer-Verlag Berlin Heidelberg 2004

Presentation: PPT, PDF (39 slides)


  1. Usa Sammapun, Insup Lee, and Oleg Sokolsky. 2005. RT-MaC: Runtime monitoring and checking of quantitative and probabilistic properties. In Proceedings of the 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, 147–153. IEEE Computer Society.

  2. Koushik Sen, Mahesh Viswanathan, and Gul Agha. 2004. Learning continuous time Markov chains from sample executions. In Proceedings of the First International Conference on the Quantitative Evaluation of Systems, 146–155. IEEE Computer Society.

  3. Koushik Sen, Mahesh Viswanathan, and Gul Agha. 2004. Statistical model checking of black-box probabilistic systems. In Proceedings of the 16th International Conference on Computer Aided Verification, 202–215. Springer.

Håkan L. S. Younes Valid CSS! Valid XHTML 1.0!
Last modified: Thu May 11 14:56:58 EDT 2006