ABSTRACT
PRISM: Probabilistic Symbolic Model Checker
Prof. Marta Kwiatkowska
School of Computer Science, University of Birmingham
Probability is widely used in the design and analysis of software and
hardware systems: as a means to derive efficient algorithms (e.g. the
use of coin flipping and randomness in decision making); as a model for
unreliable or unpredictable behavior (e.g. fault-tolerant systems,
computer networks); and as a tool to analyse system performance (e.g.
the use of steady-state probabilities in the calculation of throughput
and mean waiting time). Probabilistic verification (or probabilistic
model checking) refers to a range of techniques for calculating the
likelihood of the occurrence of certain events during the execution of
the system, and can be useful to establish properties such as
``shutdown occurs with probability at most 0.01'' and ``video frame
will be delivered within 5ms with probability at least 0.97''.
This talk introduces the probabilistic model checker PRISM being
developed at the University of Birmingham. PRISM can be used to build a
variety of probabilistic models (discrete- and continuous-time Markov
chains and Markov decision processes). Models are specified using a
simple state-based language, an extension of Reactive Modules. Two
property specification languages are supported, PCTL (probabilistic
computation tree logic) and CSL (continuous stochastic logic). PRISM
is a symbolic model checker - its basic underlying data structures are
BDDs and MTBDDs (multi-terminal BDDs), though for numerical
computations three engines (sparse, MTBDD and hybrid) are supported.
The talk will give a brief overview of issues in probabilistic model
checking, outline the symbolic model construction together with
selected algorithms, and finish with some examples.
More information about the subject can be found on
http://www.cs.bham.ac.uk/~dxp/prism/.
Maintained by rbennett@cs.ucl.ac.uk