## A Comparison of Sequential and GPU Implementations of Iterative Methods to Compute Reachability Probabilities

DisCoVeri Group, Department of Computer Science and Engineering, York University, 4700 Keele Street, Toronto, ON, M3J 1P3, Canada

EPTCS 99, 2012, pp. 20-34; arXiv:1210.6412 [cs.DC] (24 Oct 2012)

@article{2012arXiv1210.6412C,

author={Cormie-Bowins}, E.},

title={"{A Comparison of Sequential and GPU Implementations of Iterative Methods to Compute Reachability Probabilities}"},

journal={ArXiv e-prints},

archivePrefix={"arXiv"},

eprint={1210.6412},

primaryClass={"cs.DC"},

keywords={Computer Science – Distributed, Parallel, and Cluster Computing, Computer Science – Logic in Computer Science},

year={2012},

month={oct},

adsurl={http://adsabs.harvard.edu/abs/2012arXiv1210.6412C},

adsnote={Provided by the SAO/NASA Astrophysics Data System}

}

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.

October 25, 2012 by hgpu