David Parker
Reader, Computer Science, University of Birmingham
[KNP01] Marta Kwiatkowska, Gethin Norman and David Parker. PRISM: Probabilistic Symbolic Model Checker. In Proc. PAPM/PROBMIV'01 Tools Session, pages 7-12. Available as Technical Report 760/2001, University of Dortmund. September 2001. [ps.gz] [pdf] [bib] [Tool paper describing PRISM.]
Downloads:  ps.gz ps.gz (71 KB)  pdf pdf (228 KB)  bib bib
Notes: For more information about PRISM, see the website.
Abstract. In this paper we describe PRISM, a tool being developed at the University of Birmingham for the analysis of probabilistic systems. PRISM supports three probabilistic models: discrete-time Markov chains, continuous-time Markov chains and Markov decision processes. Analysis is performed through model checking such systems against specifications written in the probabilistic temporal logics PCTL and CSL. The tool features three model checking engines: one symbolic, using BDDs (binary decision diagrams) and MTBDDs (multi-terminal BDDs); one based on sparse matrices; and one which combines both symbolic and sparse matrix methods. PRISM has been successfully used to analyse probabilistic termination, performance, dependability and quality of service properties for a range of systems, including randomized distributed algorithms [2], polling systems [22], workstation clusters [18] and wireless cell communication [17].