[Nim10] Vincent Nimal. Statistical Approaches for Probabilistic Model Checking. MSc Mini-project Dissertation, Oxford University Computing Laboratory. September 2010. [pdf] [bib] [Investigates approximate/statistical model checking techniques and implements them in PRISM.]
Downloads:  pdf pdf (3.36 MB)  bib bib
Abstract. In this dissertation, we survey the different techniques used to perform statistical probabilistic model checking, prove their respective validity and compare them in terms of (statistical) reliability. We then propose some extensions of these methods for computation of rewards, which to our knowledge has not been done before. All these strategies are added to the code of the probabilistic model checking tool PRISM, and we experiment them on several large biological model examples. We conclude by some recommendations for the practical use of these methods, based on the experiments observation and the methods comparisons.