Efficient Probabilistic Model Checking on General Purpose Graphics Processors

Dragan Bosnacki, Stefan Edelkamp, Damian Sulewski
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.


   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},





Download Download (PDF)   View View   Source Source   



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.
No votes yet.
Please wait...

* * *

* * *

* * *

HGPU group © 2010-2022 hgpu.org

All rights belong to the respective authors

Contact us: