PRISM - Symbolic Probabilistic Model Checking

Marta Kwiatkowska

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.

In the talk will give a brief overview of issues in probabilistic model checking, and finish with some examples(self-stabilisation, dynamic power management and FireWire root contention).