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

TL;DR

This paper compares sequential and GPU-accelerated iterative methods, Jacobi and BiCGStab, for computing reachability probabilities in Markov chains, demonstrating GPU advantages and method performance variations based on matrix density.

Contribution

It introduces GPU implementations of Jacobi and BiCGStab methods for reachability probability calculations and compares their performance on different matrix types.

Findings

GPU implementations outperform sequential ones for large matrices.

BiCGStab is better for dense matrices, Jacobi for sparse matrices.

Jacobi method outperforms Krylov methods in probabilistic model checking contexts.

Abstract

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.