high performance computing on graphics processing units: hgpu.org

We provide an efficient implementation of existing parameter synthesis techniques for stochastic systems modelled as continuous-time Markov chains (CTMCs). These techniques iteratively decompose the parameter space into its subspaces and approximate the satisfaction function that for any parameter values from the parameter space returns the probability of the formula being satisfied in the CTMC given by those parameter values. Based on a sparse matrix representation we developed an efficient CPU oriented algorithm and GPU oriented algorithm; the latter takes advantage of the GPU architecture and parallelizes the task at the state level of the stochastic model. We also devised a technique for further parallelization on the parameter subspace level to better utilize the hardware and thus further speed up the computation. The overall speed up is more than 20 on multiple systems compared to the optimized sequential implementation which itself is several times faster than the original one.