Probabilistic symbolic model checking with PRISM: a hybrid approach.
In this paper we present efficient symbolic techniques for probabilistic model checking. These have been implemented in PRISM, a tool for the analysis of probabilistic models such as discrete-time Markov chains, continuous-time Markov chains and Markov decision processes using specifications in the probabilistic temporal logics PCTL and CSL. Motivated by the success of model checkers such as SMV which use BDDs (binary decision diagrams), we have developed an implementation of PCTL and CSL model checking based on MTBDDs (multi-terminal BDDs) and BDDs. Existing work in this direction has been hindered by the generally poor performance of MTBDD-based numerical computation, which is often substantially slower than explicit methods using sparse matrices. The focus of this paper is a novel hybrid technique which combines aspects of symbolic and explicit approaches to overcome these performance problems. For typical examples, we achieve a dramatic improvement over the purely symbolic approach. In addition, thanks to the compact model representation using MTBDDs, we can verify systems an order of magnitude larger than with sparse matrices, while almost matching or even beating them for speed.
Introduction
In the design and analysis of software and hardware systems it is often desirable
or even necessary to include probabilistic aspects of a system's behaviour. Examples
include representing unreliable or unpredictable behaviour in fault-tolerant
systems; deriving e-cient algorithms by using electronic coin
ipping in decision
making; and modelling the arrivals and departures of calls in a wireless cell.
Probabilistic model checking refers to a range of techniques for calculating
the likelihood of the occurrence of certain events during the execution of systems
which exhibit such behaviour. One rst constructs a probabilistic model of the
system. Properties such as \shutdown occurs with probability 0.01 or less" and
\the video frame will be delivered within 5ms with probability 0.97 or greater"
can be expressed in probabilistic temporal logics. Model checking algorithms
? Supported in part by EPSRC grant GR/M04617 and MathFIT studentship for David
Parker.
J.-P. Katoen and P. Stevens (Eds.), 8th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS'02), volume 2280 of LNCS, pages 52{66, 2002.
c
Springer-Verlag Berlin Heidelberg 2002
Marta Kwiatkowska, Gethin Norman, and David Parker
have been developed which then automatically verify whether the model satises
these properties.
Motivated by the success of symbolic model checkers, such as SMV [28] which
use BDDs (binary decision diagrams) [11], we have developed a symbolic probabilistic
model checker. In the non-probabilistic setting, model checking involves
analysing properties of state transition systems and the manipulation of sets
of states. Both these entities can be represented naturally as BDDs, often very
compactly [13]. In the probabilistic case, since probability transition matrices
and probability vectors are required, BDDs alone are not su-cient, and hence
we also use MTBDDs (multi-terminal binary decision diagrams) [17, 3], a natural
extension of BDDs for representing real-valued functions.
Symbolic probabilistic model checking has been considered by a number of
people [5, 21, 4, 26, 19, 23, 7, 25, 27] and it has been shown that it is feasible to
use MTBDDs to construct and compute the reachable state space of extremely
large, structured, probabilistic models. In these cases, it is often also possible to
verify qualitative properties, where model checking reduces to reachability-based
analysis. For example, in [19], systems with over 10 states have been veried.
Model checking quantitative properties, on the other hand, involves numerical
computation. In some cases, such as in [27], MTBDDs have been very successful,
being applied to systems with states. Often, however, it turns out that
such computation is slow or infeasible. By way of comparison, we have also implemented
the equivalent numerical computation routines explicitly, using sparse
matrices. In these cases, we nd that sparse matrices are orders of magnitude
faster. Here, we present a novel hybrid approach which uses extensions of the
MTBDD data structure and borrows ideas from the sparse matrix techniques
to overcome these performance problems. We include experimental data which
demonstrates that, using this hybrid approach, we can achieve speeds which are
orders of magnitude faster than MTBDDs, and in fact almost match the speed
of sparse matrices, whilst maintaining considerable space savings.
The outline of this paper is as follows. Section 2 gives an overview of probabilistic
model checking, introducing the probabilistic models and temporal logics
we consider. In Section 3, we describe our tool, PRISM, which implements this
model checking. We then move on to discuss the implementation. Section 4 introduces
the MTBDD data structure and explains how it is used to represent
and analyse probabilistic models. We identify a number of performance problems
in this implementation and, in Section 5, describe how we overcome these
limitations. In Section 6, we present experimental results and analyse the success
of our technique. Section 7 concludes the paper.
Model Checking
In this section we brie
y summarise the three probabilistic models and two
temporal logics that PRISM supports. The simplest probabilistic model is the
discrete-time Markov chain (DTMC), which species the probability P(s; s 0 )
of making a transition from state s to some target state s 0 , where the proba-
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach 3
bilities of reaching the target states from a given state must sum up to 1, i.e.
decision processes (MDPs) extend DTMCs by allowing
both probabilistic and non-deterministic behaviour. More formally, in any state
there is a non-deterministic choice between a number of discrete probability distributions
over states. Non-determinism enables the modelling of asynchronous
parallel composition of probabilistic systems, and permits the under-specication
of certain aspects of a system. A continuous-time Markov chain (CTMC), on the
other hand, species the rates R(s; s 0 ) of making a transition from state s to s 0 ,
with the interpretation that the probability of moving from s to s 0 within t time
units (for positive real valued t) is 1 e R(s;s 0 )t .
Probabilistic specication formalisms include PCTL [20, 10, 8], a probabilistic
extension of the temporal logic CTL applicable in the context of MDPs and
DTMCs, and the logic CSL [7], a specication language for CTMCs based on
CTL and PCTL.
allows us to express properties of the form \under any scheduling of
processes, the probability that event A occurs is at least p (at most p)". By
way of illustration, we consider the asynchronous randomized leader election
protocol of Itai and Rodeh [24] which gives rise to an MDP. In this algorithm,
the processors of an asynchronous ring make random choices based on coin tosses
in an attempt to elect a leader. We use the atomic proposition leader to label
states in which a leader has been elected. Examples of properties we would wish
to verify can be expressed in PCTL as follows:
{ P1 [ leader ] - \under any fair scheduling, a leader is eventually elected with
probability 1".
{ fair scheduling, the probability of electing a
leader within k discrete time steps is at most 0.5".
The specication language CSL includes the means to express both transient
and steady-state performance measures of CTMCs. Transient properties describe
the system at a xed real-valued time instant t, whereas steady-state properties
refer to the behaviour of a system in the \long run". For example, consider a
queueing system where the atomic proposition full labels states where the queue
is full. CSL then allows us to express properties such as:
{ probability that the queue becomes full within t time
units is at most 0:01"
{ \in the long run, the chance that the queue is not full is at
least 0:98".
Model checking algorithms for PCTL have been introduced in [20, 10] and
extended in [8, 4] to include fairness. An algorithm for CSL was rst proposed
in [7] and has since been improved in [6, 25]. The model checking algorithms for
both logics reduce to a combination of reachability-based computation (manip-
ulation of sets of states) and numerical computation. The former corresponds
to nding all those states that satisfy the formula under study with probability
exactly 0 or 1. The latter corresponds to calculating the probabilities for the remaining
states. For DTMCs, this entails solution of a linear equation system, for
4 Marta Kwiatkowska, Gethin Norman, and David Parker
Modules
Parser
Parser
Hybrid
Engine
Sparse
Engine Engine
Results
(States/Probabilities)
CUDD
MTBDD
Properties
System
Description
Prism Kernel
Fig. 1. PRISM System Architecture
MDPs, solving a linear optimisation problem, and for CTMCs, either solution
of a linear equation system or a standard technique known as uniformisation.
These numerical problems are typically too large for the application of direct
methods, and instead iterative techniques which approximate the solution up to
some specied accuracy are used.
3 The Tool
PRISM is a tool developed at the University of Birmingham which supports
the model checking described in the previous section. The tool takes as input
a description of a system written in PRISM's system description language, a
probabilistic variant of Reactive Modules [1]. It rst constructs the model from
this description and computes the set of reachable states. PRISM accepts specications
in either the logic PCTL or CSL depending on the model type. It then
performs model checking to determine which states of the system satisfy each
specication. All reachability-based computation is performed using BDDs. For
numerical analysis, however, there is a choice of three engines: one using pure
MTBDDs, one based on conventional sparse matrices, and a third using the hybrid
approach we present in this paper. Figure 1 shows the structure of the tool
and

Figure

2 shows a screen-shot of the graphical user interface.
PRISM is written in a combination of Java and C++ and uses CUDD [32], a
publicly available BDD/MTBDD library developed at the University of Colorado
at Boulder. The high-level parts of the tool, such as the user interface and parsers,
are written in Java. The engines and libraries are written in C++. The tool and
its source code, along with further information about the system description
language and case studies, is available from the PRISM web page [31].
4 An MTBDD Implementation
We now describe the implementation of the tool. The fundamental data structures
in PRISM are MTBDDs and BDDs. MTBDDs can be used to represent all
three of the supported models: DTMCs, MDPs and CTMCs. Furthermore, all
algorithms for the construction and analysis of these models can be implemented
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach 5
Fig. 2. The PRISM Graphical User Interface
using these data structures. In this section, we summarise how this is done and
discuss its performance.
Introduction to MTBDDs
xn be a set of distinct, totally ordered, Boolean variables. An
MTBDD M over directed acyclic graph with vertex
set Vn partitioned into non-terminal and terminal vertices. A non-terminal
vertex Vn is labelled by a variable var (v) 2 fx and has
two children labelled by a real
number val (v).
We impose the Boolean variable ordering < onto the graph by requiring that
a child w of a non-terminal vertex v is either terminal or is non-terminal and
satises var (v) < var(w). The MTBDD represents a function fM
IR. The value of fM determined by traversing M from the
root vertex, following the edge from vertex v to then(v) or else(v) if var(v) is 1
or 0 respectively. Note that a BDD is merely an MTBDD with the restriction
that the labels on terminal vertices can only be 1 or 0.
MTBDDs are e-cient because they are stored in reduced form. If vertices
v and w are identical (i.e.
else(w)), then only one is stored. Furthermore, if a vertex v satisifes
else(v), it is removed and any incoming edges are redirected to its unique child.
One of the most important factors about MTBDDs from a practical point of
view is that their size (number of vertices) is heavily dependent on the ordering
of the Boolean variables. Although, in the worst case, the size of an MTBDD representation
is exponential and the problem of deriving the optimal ordering for
a given MTBDD is an NP-complete problem, by applying heuristics to minimise
6 Marta Kwiatkowska, Gethin Norman, and David Parker
graph size, MTBDDs can provide extremely compact storage for real-valued
functions.
MTBDD Represention of Probabilistic Models
From their inception in [17, 3], MTBDDs have been used to encode real-valued
vectors and matrices. An MTBDD M over variables
that a real vector v of length 2 n is simply a
mapping from to the reals IR. Hence, if we decide upon an encoding of
in terms of fx (for example the standard binary encoding),
then an MTBDD M can represent v.
In a similar fashion, we can consider a square matrix M of size 2 n by 2 n
to be a mapping from to IR. Taking Boolean variables
to range over row indices and fy to range over column in-
dices, we can represent M by an MTBDD over fx g. DTMCs
and CTMCs are described by such matrices, and hence are also straightforward
to represent as MTBDDs. The case for MDPs is more complex since we
need to encode the non-deterministic choices. If the maximum number of non-deterministic
choices in any state is bounded by 2 k for some integer k, we can
view the MDP as a function from to IR.
By adding k extra Boolean variables to encode this third index, we can represent
the MDP as an MTBDD.

Figure

3 shows an example of a CTMC and its rate matrix. The CTMC
includes one state which is unreachable. This is explained in Section 5. Figure 4
gives the MTBDD which represents this CTMC and a table explaining its con-
struction. For clarity, in our notation for MTBDDs, we omit edges which lead
directly to the zero terminal vertex.
Fig. 3. A CTMC and its rate matrix
Transition x1 x2 y1 y2 x1 y1 x2 y2 R
Fig. 4. An MTBDD representing the CTMC in Figure 3
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach 7
Observe that, in Figure 4, row and column variables are ordered alternately.
This is one of the most common variable ordering heuristics to minimise MTBDD
size. To achieve compact MTBDD representations of probabilistic systems, how-
ever, we must also consider the actual encoding of row and column indices to
Boolean variables. A well known rule of thumb is to try and preserve structure
in the entity being represented [23]. In practice, this can be accomplished by
performing a direct translation from a high-level description of the model (in
our case the PRISM system description language) to MTBDDs. We presented
such a scheme in [19] which is not only fast but can lead to a very compact
encoding of probabilistic systems. The resulting variable ordering encodes unreachable
states, as well as reachable states, and hence reachability analysis (via
a simple BDD xpoint calculation) must be performed to identify them.
Our experimental data is presented in Section 6. For reasons of space we
only include statistics for two typical examples: rstly, an MDP model of the
coin protocol from Aspnes and Herlihy's randomized consensus algorithm [2],
parameterised by N (the number of processes) and an additional parameter K
xed at 4; secondly, a CTMC model of a Kanban manufacturing system [16]
parameterised by N (the number of pallets in the system). Figure 8 gives the
memory requirements for storing these models. Compare the 'MTBDD' and
'Sparse' columns: signicant savings in memory can be achieved using the symbolic
scheme described above over an explicit storage method. For other examples
which demonstrate this result, see the PRISM web page [31].
Probabilistic Model Checking with MTBDDs
We have implemented the entire model checking procedure for PCTL and CSL in
MTBDDs and BDDs. As we saw in Section 2, essentially this reduces to a combination
of reachability-based computation and numerical calculation. The former
can be performed with BDDs and forms the basis of non-probabilistic symbolic
model checking which has been proven to be very successful [13, 28]. The latter
involves iterative numerical methods, based on matrix-vector multiplication, an
operation for which e-cient MTBDD algorithms have been introduced [3, 17].
In fact, alternative, direct, methods such as Gaussian elimination and Simplex
could be applied to some of these problems, but have been shown to be unsuitable
for an MTBDD implementation [3, 26]. They rely on modifying the model
representation through operations on individual rows, columns or elements. This
is not only slow, but leads to a loss in regularity and a subsequent explosion in
MTBDD size.
The results of this implementation in MTBDDs can be summarised as fol-
lows. There is a clear distinction between the two dierent aspects of model
checking. Reachability-based computation, which is su-cient for model checking
qualitative properties, can be implemented e-ciently with BDDs, as is shown
in [19, 27]. Numerical computation, which is required for checking of quantitative
properties, is more unpredictable. This is the problem we focus on here.
We have found a number of case studies for which MTBBDs outperform
explicit techniques on numerical computation. One such example is the coin
8 Marta Kwiatkowska, Gethin Norman, and David Parker
protocol, introduced previously. We include results for this model in the top
half of Figure 9. Compare the columns for 'MTBDD' and `Sparse': it would be
impossible to even store the sparse matrix for the larger examples, assuming a
reasonable amount of memory. We have found this pattern to hold for several of
the other MDP case studies we have considered. Other examples which illustrate
this can be found on the PRISM web site [31], and include a Byzantine agreement
protocol and the IEEE 1394 FireWire root contention protocol.
For a second class of models, namely CTMCs, we nd that the symbolic
implementation of numerical iterative methods is far from e-cient. Despite a
compact MTBDD representation of the model, the process is generally very slow
or infeasible. This ine-ciency is caused by the MTBDD representation of the
iteration vectors becoming too large. For vectors to be represented compactly
by MTBDDs the main requirement is a limited number of distinct elements.
However, in general, when performing numerical analysis, the iteration vector
quickly acquires almost as many distinct values as there are states in the system
under study. Figure 9 shows the contrast in performance of MTBDDs between
the Kanban CTMC and the coin protocol MDP. The sparse matrix based implementation
is much faster.
5 A Hybrid Approach
We now present a method to overcome the ine-ciencies with MTBDDs outlined
in the previous section. Recall that sparse matrix techniques can yield extremely
fast numerical computation. Since the iteration vector is stored in a full array, it
remains a constant size. A single matrix-vector multiplication is carried out by
traversing the sparse matrix and extracting all the non-zero entries, each of which
is needed exactly once to compute the new iteration vector. Unfortunately, since
the probabilistic model is also stored explicitly, application to large examples is
often limited by memory constraints.
The approach taken here is to a use a hybrid of the two techniques: MTBDDs
and sparse matrices. We store the transition matrix in an MTBDD-like data
structure but use a full array for the iteration vector. We can then perform
matrix-vector multiplication, and hence iterative methods, using these two data
structures. The key dierence in this hybrid approach is that we need to extract
the non-zero matrix entries from an MTBDD rather than a sparse matrix. For
clarity, this presentation focuses on the case of CTMCs, where we solve a linear
equation system by iterative methods to compute the steady-state probabilities.
We have also applied these techniques to DTMC and MDP models.
If we restrict ourselves to certain iterative methods, namely Power, Jacobi
and JOR, then the matrix entries can be extracted in any order to perform
an iteration. This means that we can can proceed via a recursive traversal of
the MTBDD: it does not that matter that this will enumerate the entries in
an essentially random order, rather than row-by-row (or column-by-column) as
with a sparse matrix.
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach 9
Since the matrix indices are encoded with the standard binary representation
of integers, it is trivial to keep track of the row and column index during traversal
by noting whether a then or else edge is taken at each point and summing the
appropriate powers of 2. Unfortunately, there are a number of problems with
this naive approach. To resolve these, we make a number of modications to the
MTBDD data structure.
Modifying the MTBDD Data Structure
First, recall from Section 4, that to get an e-cient MTBDD representation of
our transition matrix, it must contain unreachable states. Performing matrix-vector
multiplication as just described on such an MTBDD would require the
vector array to store entries for all states, including those that are unreachable.
The number of unreachable states is potentially very large, in some cases orders
of magnitude larger than the reachable portion. This puts unacceptable limits
on the size of problem which we can handle.
The solution we adopt is to augment the MTBDD with vertex labels: integer
osets which can be used to compute the actual indices of the matrix elements (in
terms of reachable states only) during our recursive traversal. Figure 5 illustrates
this idea on the example from Section 4, which included an unreachable state.
On the left is the modied MTBDD representing the transition matrix R of the
CTMC. The table on the right explains how the traversal process works. Each
row corresponds to a single matrix entry (transition). The rst ve columns
describe the path taken through the MTBDD. The next four columns give the
vertex osets along this path. The last column gives the resulting matrix entry. In

Figure

6, we give the actual traversal algorithm. This would be called as follows:
TraverseRec(root , 0, 0), where root is the top-level vertex in the MTBDD.
Path Osets Transition
Fig. 5. The modied MTBDD representing the CTMC in Figure 5
The key idea is that indices are computed by summing osets. A vertex's
oset is only added when leaving the then edge of that vertex. Note that row
and column indices are computed independently, rows from osets on x i vertices,
and columns from osets on y i vertices. As an example, consider the last line of
the table. We take the path through the MTBDD which leads to the 7
terminal vertex. We only use the osets at levels x 1 , x 2 and y 2 where we exited
via then edges. The row index is 2, the column index is 1 and we obtain
Marta Kwiatkowska, Gethin Norman, and David Parker
TraverseRec(v, row , col)
if (v is a non-zero terminal vertex) then
found matrix element (row ;
elseif (v is a row vertex) then
TraverseRec(else(v), row , col)
elseif (v is a row vertex) then
TraverseRec(else(v), row , col)
TraverseRec(then(v), row , col
endif
Fig. 6. Hybrid Traversal Algorithm
the matrix entry (2; 7. Note that references to state 3 in Figure 4 have
changed to state 2 in Figure 5, since we only have three reachable states.
There are two further points to consider about the conversion of the MTBDD

Figure

to its new form (Figure 5). First, note that some vertices in an
MTBDD can be reached along several dierent paths. These shared vertices
correspond to repeated sub-matrices in the overall matrix. Consider the matrix
in

Figure

3 and its MTBDD representation in Figure 4. The bottom-left and
top-right quadrants of the matrix are identical (since rows and columns of unreachable
states are lled with zeros). This is re
ected by the fact that the x 2
vertex in the MTBDD has two incoming edges. The two identical sub-matrices
do not, however, share the same pattern of reachable states. This means that
there is a potential clash as to which oset should label the vertex.
We resolve this by adding extra copies of the vertex where necessary, labelled
with dierent osets. Note the additional two vertices on the right hand side in

Figure

5. Eectively, we have modied the condition under which two MTBDD
vertices are merged, requiring not only that are they are on the same level and
have identical children, but also that they have the same oset label. It should
be noted here that we transform the MTBBD once, use it for as many iterations
are required, and then discard it. Hence, we only need to be able to traverse the
data structure, not manipulate it in any way.
The second point to make about the conversion involves skipped levels. In an
MTBDD, if a vertex has identical children, it is omitted to save space. This causes
potential problems, because we must be careful to detect this during traversal. In
fact, the solution we adopt is to perform this check only once, during the initial
conversion, and replace skips with extra vertices. This allows us to ignore the
issue entirely during traversal and makes the process faster. There is an example
of this in Figure 5 { note the extra x 2 vertex on the left hand side. The exception
to this rule is that we do allow edges to skip from any vertex directly to the zero
terminal vertex, since we are only interested in the non-zero entries.
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach 11
Optimising the Approach
We can optimise our method considerably via a form of caching. MTBDDs exploit
structure in the model being analysed giving a signicant space saving.
This is achieved by identical vertices (representing identical sub-matrices) being
merged and stored only once. During traversal, however, each of these shared
vertices will be visited several times (as many times as the sub-matrix occurs
in the overall matrix) and the entries of the sub-matrix will be computed every
time. By storing and reusing the results of this computation, we can achieve a
signicant speed-up in traversal time.
Rather than store these results in a cache, which would need to be searched
through frequently, we simply attach the information directly to MTBDD ver-
tices. We select some subset of the vertices, build explicit (sparse matrix) representations
of their associated sub-matrices and attach them to the MTBDD.
There is an obvious trade-o here between the additional space required to store
the data and the resulting improvement in speed. The space required and time
improvement both depend on how many vertices (and which ones) we attach
matrices to. From our experiences, a good policy is to replace all the vertices in
one (fairly low) level of the MTBDD. In Figure 7, we demonstrate this technique
on the running example, replacing all vertices on the x 2 level with the matrices
they represent.
In practice, we nd that caching can improve traversal speed by an order
of magnitude. In the next section, we give experimental results from our implementation
which includes all the techniques described here.
(0
2Fig. 7. The modied MTBDD labelled with explicit sub-matrices
6 Results
In this section, we present our experimental results, obtained from the PRISM
tool. We compare the performance of the three implementations discussed in
this paper: pure MTBDDs, sparse matrices, and our hybrid approach, focusing
on the problem of iterative numerical computation.
In

Figure

8, we give storage requirements for the coin protocol and Kanban
models introduced earlier. We compare the size of the MTBDD, the sparse matrix
and the modied MTBDD used in the hybrid approach, with and without
optimisation. In Section 4, we observed the signicant advantage of MTBDDs
over sparse matrices. Note that, even when storing oset information, extra vertices
and explicit sub-matrices, the hybrid approach remains memory e-cient.
12 Marta Kwiatkowska, Gethin Norman, and David Parker
Model N States Memory (KB)
MTBDD Sparse Hybrid Hybrid Opt.
Coin 4 43,136 28.5 2,265 56.7 69.8
protocol 6 2,376,448 61.2 173,424 93.3 314
Kanban 4 454,475 95.7 48,414 171 231
system 5 2,546,432 123 296,588 219 337
6 11,261,376 154 1,399,955 272 486
Fig. 8. Storage requirements for the coin protocol and Kanban examples
Model N States Iter.s Time per iteration (sec.)
MTBDD Sparse Hybrid Hybrid Opt.
Coin 4 43,136 6,133 0.173 0.034 0.07 0.039
protocol 6 2,376,448 12,679 1.01 1.741 5.58 3.02
Kanban 4 454,475 466 - 0.436 6.09 0.502
system 5 2,546,432 663 - 2.76 33.4 3.150
Fig. 9. Model checking times for the coin protocol and Kanban examples
Furthermore, the time for adding this information to the MTBDD was in all
cases negligle compared to that for model checking.
In

Figure

9, we present model checking times for the same two case studies.
For the coin protocol, we verify a quantitative PCTL property which requires
solution of a linear optimisation problem. For the Kanban system, we model
check a quantitative CSL property which requires computation of the steady-state
probabilities via the solution of a linear equation system. We use the JOR
iterative method. All experiments were run on a 440 MHz Sun Ultra 10 workstation
with 1 GB memory. The iterative methods were terminated when the
relative error between subsequent iteration vectors was less than 10 6 .
As we remarked in Section 4, the coin protocol model, and many of our other
MDP models, are e-cient for MTBDDs. The problem we try to address with our
hybrid approach is typied by the Kanban example, where MTBDDs alone are
ine-cient. By using the techniques presented in this paper, we were able to consider
larger models than with sparse matrices. Furthermore, using the optimised
version, we can almost match the speed of sparse matrices. Other CTMC case
studies we have considered, such as queueing networks and workstation clusters,
conrm these results. Details can be found on the PRISM web page [31].
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach 13
Related Work: We are aware of three other probabilistic model checking tools.
ProbVerus [21] is an MTBDD-based model checker which only supports DTMCs
and a subset of PCTL. The tool E'MC 2 [22] supports model checking of CTMCs
against CSL specications using sparse matrices. The tool described in [18] uses
abstraction and renement to perform model checking for a subset of PCTL
over MDPs. There are a number of sparse-matrix based DTMC and CTMC
tools, such as MARCA [33], which do not allow logic specications but support
steady-state and transient analysis.
An area of research which has close links with our work is the Kronecker
approach [30], a technique for the analysis of very large, structured CTMCs and
DTMCs. The basic idea is that the matrix of the full system is dened as a
Kronecker algebraic expression of smaller matrices, which correspond to sub-components
of the overall system. It is only necessary to store these small matrices
and the structure of the Kronecker expression. Iterative solution methods
can be applied to the matrix while in this form. As with our approach, storage
requirements for the matrix are relatively small, but ingenious techniques must
be developed to minimise the time overhead required for numerical solution.
Tools which support Kronecker based methods include APNN [9] and SMART
[14].
In particular, SMART incorporates matrix diagrams [15], a data structure
developed as an e-cient implementation of the Kronecker techniques. The matrix
diagram approach has much in common with the hybrid method we present
in this paper. In particular, both methods use a decision-diagram like data structure
for storing matrices and full array to store vectors. The key dierence is that
matrix diagrams are tied to the Kronecker representation and as such require
more work to extract the transition matrix entries. In addition to traversing the
data structure, as we do, computation of matrix elements requires multiplication
of entries from the smaller matrices.
Another important dierence is that Kronecker and matrix diagram approaches
permit the use of more e-cient iterative methods, such as Gauss-Seidel.
Our approach does not presently support these. Hence, although we have less
work to do per iteration, we may require more iterations using our methods.
In addition, Gauss-Seidel can be implemented with a single iteration vector,
whereas methods such as Jacobi and JOR require two.
One issue that unites the Kronecker approach, matrix diagrams and our
method is that their limiting factor is the space required to store the iteration
vector. However compact the matrix representation is, memory proportional to
the number of states is required for numerical solution. Buchholz and Kemper
consider an interesting technique in [12] using PDGs (Probabilistic Decision
Graphs). This attempts to store the iteration vector in a structured way, as is
done with the matrix. More investigation is required to discover the potential of
this approach.
14 Marta Kwiatkowska, Gethin Norman, and David Parker
7 Conclusion
We have introduced PRISM, a tool to build and analyse probabilistic systems
which supports three types of models (DTMCs, MDPs and CTMCs) and two
probabilistic logics (PCTL and CSL). As well as MTBDD and sparse matrix
based model checking engines, PRISM includes a novel, hybrid engine which
combines symbolic and explicit approaches. We have shown that very large probabilistic
systems can be constructed and analysed using MTBDDs, but that,
often, numerical computation is very ine-cient. Our hybrid approach addresses
these performance problems, allowing verication, at an acceptable speed, of
much larger systems than would be feasible using sparse matrices. Further details
of this will be available in [29].
One problem with our current techniques is that they presently only support
the Power, Jacobi and JOR iterative methods. We plan to extend the work
to allow more rapidly converging alternatives such as Gauss-Seidel or Krylov
methods to be used.
The development of PRISM is an ongoing activity. In the near future we
intend to consider extensions of PCTL for expressing expected time and long
run average properties and of CSL to include rewards, expand the PRISM input
language to allow process algebra terms, and develop model checking engines for
PRISM which work in a parallel or distributed setting.



--R

Reactive modules.
Fast randomized consensus using shared memory.
Algebraic decision diagrams and their applications.
On algorithmic veri
Symbolic model checking for probabilistic processes.
Model checking continuous-time Markov chains by transient analysis
Approximative symbolic model checking of continuous-time Markov chains
Model checking for a probabilistic branching time logic with fairness.
A toolbox for functional and quantitative analysis of DEDS.
Model checking of probabilistic and nondeterministic systems.

Compact representations of probability distributions in the analysis of superposed GSPNs.
Symbolic model checking: 10 20 states and beyond.
SMART: Simulation and Markovian analyser for reliability and timing.
A data structure for the e-cient Kronecker solution of GSPNs
On the use of Kronecker operators for the solution of generalized stocastic Petri nets.

Reachability analysis of probabilistic systems by successive re
Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation.
A logic for reasoning about time and probability.
ProbVerus: Probabilistic symbolic model checking.
A Markov chain model checker.
Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains.
Symmetry breaking in distributed networks.
Faster and symbolic CTMC model checking.
Symbolic model checking of concurrent probabilistic systems using MTBDDs and Simplex.
Automated veri
Symbolic Model Checking.
Implementation of symbolic model checking for probabilistic systems.
On the stochastic structure of parallelism and synchronisation models for distributed algorithms.
PRISM web page.
CUDD: Colorado University decision diagram package.
MARCA: Markov chain analyser
--TR

--CTR
G. Ciardo , R. L. Jones, III , A. S. Miner , R. I. Siminiceanu, Logic and stochastic modeling with SMART, Performance Evaluation, v.63 n.6, p.578-608, June 2006
Annabelle McIver , Carroll Morgan, Abstraction and refinement in probabilistic systems, ACM SIGMETRICS Performance Evaluation Review, v.32 n.4, p.41-47, March 2005
Christel Baier , Frank Ciesinski , Marcus Grer, ProbMela and verification of Markov decision processes, ACM SIGMETRICS Performance Evaluation Review, v.32 n.4, p.22-27, March 2005
Christel Baier , Frank Ciesinski , Marcus Groesser, Quantitative analysis of distributed randomized protocols, Proceedings of the 10th international workshop on Formal methods for industrial critical systems, p.2-7, September 05-06, 2005, Lisbon, Portugal
Christel Baier , Boudewijn R. Haverkort , Holger Hermanns , Joost-Pieter Katoen, Model checking meets performance evaluation, ACM SIGMETRICS Performance Evaluation Review, v.32 n.4, p.10-15, March 2005
Gianfranco Ciardo , Andrew S. Miner, Implicit data structures for logic and stochastic systems analysis, ACM SIGMETRICS Performance Evaluation Review, v.32 n.4, p.4-9, March 2005
Marta Kwiatkowska , Gethin Norman , David Parker , Jeremy Sproston, Performance analysis of probabilistic timed automata using digital clocks, Formal Methods in System Design, v.29 n.1, p.33-78, July      2006
Hkan L. S. Younes , Reid G. Simmons, Statistical probabilistic model checking with a focus on time-bounded properties, Information and Computation, v.204 n.9, p.1368-1409, September 2006
probabilistic model checking;symbolic model checking;binary decision diagrams