PRISM: Probabilistic symbolic model checker. (English) Zbl 1047.68533

Field, Tony (ed.) et al., Computer performance evaluation. Modelling techniques and tools. 12th international conference, TOOLS 2002, London, GB, April 14–17, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43539-5). Lect. Notes Comput. Sci. 2324, 200-204 (2002).
Summary: 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, Markov decision processes and continuous-time Markov chains. 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, and quality of service properties for a range of systems, including randomized distributed algorithms, manufacturing systems and workstation clusters.
For the entire collection see [Zbl 0992.00046].


68M20 Performance evaluation, queueing, and scheduling in the context of computer systems
68Q60 Specification and verification (program logics, model checking, etc.)


Full Text: Link