Main /

Introduction

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:

• discrete-time Markov chains (DTMCs),
• continuous-time Markov chains (CTMCs),
• Markov decision processes (MDPs),
• probabilistic timed automata (PTAs).

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:

• PCTL (probabilistic computation tree logic),
• CSL (continuous stochastic logic),
• LTL (linear time logic),
• PCTL* (which subsumes both PCTL and LTL).

plus support for costs/rewards, "quantitative" properties and several other custom features and extensions.

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.