The algorithms, techniques and data structures that comprise PRISM come from a wide range of sources. Below is a short (and still rather incomplete) guide providing references to further information on each aspect of the tool. See also the Lectures section of this website for teaching material on many of these topics.
PRISM supports discrete-time Markov chains (DTMCs) and continuous-time Markov chains (CTMCs), good texts on which are [Ste94, Kul95]. It also supports Markov decision processes (MDPs); see for example [Bel57, Put94]. Strictly speaking, since the modelling language allows multiple probability distributions with the same action label, these are actually (simple) probabilistic automata [SL95, Seg95]. Finally, it also supports probabilistic timed automata (PTAs) [Jen96, KNSS02, Bea03].
PRISM also allows all types of model to be augmented with rewards (or costs). Such extensions of DTMCs and CTMCs are sometimes referred to as (discrete- or continuous-time) Markov reward models. Similarly, PTAs with rewards/costs are sometimes called priced PTAs.
PRISM's property specification language is based on temporal logic. It subsumes:
It also includes "quantitative" extensions of these logics, such as the use of the operator P=? for querying the value of a probability, rather than comparing it to a bound. Furthermore, PRISM allows such properties to be combined into more complex arithmetic expressions; see [KNP09a] for some examples. Other simple extensions to the above logics include, for example, allowing the CSL steady-state (S) operator of [BKH99] for DTMCs.
The property specification language also supports reward (or cost) based properties for DTMCs, CTMCs and MDPs through the R operator. Syntax and semantics (for the DTMC and CTMC case) can be found in [KNP07a]. Similar (and additional) reward operators can be found in [BHHK00b] for CTMCs, [AHK03] for DTMCs, and [dA98b, dA97a] for MDPs. Reward-bounded variants of the U operator, such as found in CSRL and CRL [BHHK00b, HCH+02] and in PRCTL [AHK03] are currently not supported in PRISM.
The model checking algorithm for PCTL on DTMCs is from [CY88, HJ94, CY95]. We use matrix-vector multiplication for the X and U<=k operators and solve linear equation systems for the U operator. The algorithms for U include a step which computes all states for which the probability is exactly 0 or 1; in PRISM these are referred to as the precomputation algorithms Prob0 and Prob1.
Model checking the S operator requires the steady-state probabilities of the DTMC to be computed. As described in, e.g. [Kul95], this requires: (1) identification of the bottom strongly connected components (BSCCs) of the DTMC; (2) solution of the steady-state probabilities for each BSCC; and (3) computation of the probabilities of reaching each BSCC from each state. (1) is covered below; (2) requires solution of a linear equation system, also covered below; (3) is the same as for the U operator, above. The transient probabilities of a DTMC are computed with a sequence of matrix-vector multiplications.
The basis for the model checking algorithm for PCTL on MDPs is from [BdA95]. The X and U<=k operators are straightforward extensions of the DTMC case, as described in [Bai98]. For the U operator, as with DTMCs, we first apply precomputation algorithms. In PRISM, these are called Prob0E and Prob1A (for minimum probabilities) and Prob0A and Prob1E (for maximum probabilities). Prob0E and Prob0A are given in [BdA95], Prob1E is from [dAKN+00] (which is a simple extension of the version in [dA97a, dA99]). For computation of other probabilities for the U operator, we use (approximate) iterative methods, rather than the linear optimisation problems proposed in [BdA95] (and in e.g. [CY90, CY98]). These iterative methods are expressed in terms of least fixed points in [Bai98] and are equivalent to the well-known value iteration method for MDPs (see e.g. [Put94]). PRISM also supports a notion of fairness when model checking MDPs. This is done using the techniques described in [BK98, Bai98]).
Linear equations systems are solved in PRISM using iterative numerical methods which approximate the solution up to a prescribed accuracy (direct methods such as Gaussian elimination do not scale well to large systems). Supported iterative methods include Power, Jacobi, (forwards and backwards) Gauss-Seidel, JOR (Jacobi over relaxation) and SOR (Successive over relaxation). [Ste94] gives good coverage of many of these methods.
Two of the most important data structures used in PRISM are binary decision diagrams (BDDs) [Bry86] and multi-terminal binary decision diagrams (MTBDDs) [CFM+97, BFG+97] (in the latter, MTBDDs are called ADDs: algebraic decision diagrams). The most complete description of how PRISM uses (MT)BDDs can be found in [Par02].