  We consider the problem of computing reachability probabilities: given a
Markov chain, an initial state of the Markov chain, and a set of goal states of
the Markov chain, what is the probability of reaching any of the goal states
from the initial state? This problem can be reduced to solving a linear
equation Ax = b for x, where A is a matrix and b is a vector. We consider two
iterative methods to solve the linear equation: the Jacobi method and the
biconjugate gradient stabilized (BiCGStab) method. For both methods, a
sequential and a parallel version have been implemented. The parallel versions
have been implemented on the compute unified device architecture (CUDA) so that
they can be run on a NVIDIA graphics processing unit (GPU). From our
experiments we conclude that as the size of the matrix increases, the CUDA
implementations outperform the sequential implementations. Furthermore, the
BiCGStab method performs better than the Jacobi method for dense matrices,
whereas the Jacobi method does better for sparse ones. Since the reachability
probabilities problem plays a key role in probabilistic model checking, we also
compared the implementations for matrices obtained from a probabilistic model
checker. Our experiments support the conjecture by Bosnacki et al. that the
Jacobi method is superior to Krylov subspace methods, a class to which the
BiCGStab method belongs, for probabilistic model checking.
