PRISM is a probabilistic model checker, a tool for the modelling and analysis of systems which exhibit probabilistic behaviour. Probabilistic model checking is a formal verification technique. It is based on the construction of a precise mathematical model of a system which is to be analysed. Properties of this system are then expressed formally in temporal logic and automatically analysed against the constructed model.
PRISM has direct support for several types of probabilistic models:
It also supports probabilistic automata (PAs) [Seg95], but refers to them as MDPs. Models are supplied to the tool by writing descriptions in the PRISM language, a simple, high-level modelling language.
Properties of these models are written in the PRISM property specification language which is based on temporal logic. It incorporates several well-known probabilistic temporal logics:
PRISM performs probabilistic model checking, based on exhaustive search and numerical solution, to automatically analyse such properties. It also contains a discrete-event simulation engine for approximate model checking.