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 supports three types of probabilistic models:

discrete-time Markov chains (DTMCs),
Markov decision processes (MDPs),
continuous-time Markov chains (CTMCs).

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 the two probabilistic temporal logics

PCTL (probabilistic computation tree logic) for DTMCs and MDPs,
CSL (continuous stochastic logic) for CTMCs.

plus a number of custom features and extensions.

PRISM performs automatic analysis of such properties using either formal verification techniques based on numerical computation, or discrete-event simulation.

Introduction

PRISM Manual