Efficient Probabilistic Model Checking on General Purpose Graphics Processors
Eindhoven University of Technology, The Netherlands
Model Checking Software In Proceedings of the 16th International SPIN Workshop on Model Checking Software (2009), pp. 32-49.
@article{bosnacki2009efficient,
title={Efficient Probabilistic Model Checking on General Purpose Graphics Processors},
author={Bo{v{s}}na{v{c}}ki, D. and Edelkamp, S. and Sulewski, D.},
journal={Model Checking Software},
pages={32–49},
year={2009},
publisher={Springer}
}
We present algorithms for parallel probabilistic model checking on general purpose graphic processing units (GPGPUs). For this purpose we exploit the fact that some of the basic algorithms for probabilistic model checking rely on matrix vector multiplication. Since this kind of linear algebraic operations are implemented very efficiently on GPGPUs, the new parallel algorithms can achieve considerable runtime improvements compared to their counterparts on standard architectures. We implemented our parallel algorithms on top of the probabilistic model checker PRISM. The prototype implementation was evaluated on several case studies in which we observed significant speedup over the standard CPU implementation of the tool.
November 23, 2010 by hgpu
