PRISM - Probabilistic Symbolic Model Checking 
Marta Kwiatkowska -- University of Birmingham
www.cs.bham.ac.uk/~mzk

December 7, 2006 
11:30-1:00
 

Probabilistic models, for example discrete- and continuous-time Markov
chains, are often used to model stochastic aspects of systems, ranging
from fault-tolerant protocols, power management strategies to
biological systems. In this talk, we give an overview of an automated
formal verification technique called probabilistic model checking.

Probabilistic model checking aims to establish if a desired property
holds in a probabilistic model, and with what probability. Properties
are typically expressed in a probabilistic variant of temporal logic,
and allow specifications such as "leader election is eventually
resolved with probability 1", and "what is the expected number of
rounds until consensus is reached?". In contrast to conventional model
checkers, which rely on reachability analysis of the underlying
transition system graph, probabilistic model checking additionally
involves numerical solutions of linear equations and linear
programming problems.

A brief introduction to probabilistic model checking with the tool
PRISM (www.cs.bham.ac.uk/~dxp/prism/) developed at the University of
Birmingham will be given. PRISM is a symbolic model checker - its
basic underlying data structures are Binary Decision Diagrams (BDDs)
and their generalisation, MTBDDs (multi-terminal BDDs), though for
numerical computations three engines (sparse, MTBDD and hybrid) are
supported. This talk will outline recently obtained results that yield
substantial reductions in model size (symmetry and games-based
abstraction). The techniques will be illustrated using exampels such
as the Zeroconf dynamic configuration protocol for IPv4 link-local
addresses.