Sciweavers

Share
STTT
2011

Parallel probabilistic model checking on general purpose graphics processors

8 years 10 months ago
Parallel probabilistic model checking on general purpose graphics processors
We present algorithms for parallel probabilistic model checking on general purpose graphic processing units (GPGPUs). Our improvements target the numerical components of the traditional sequential algorithms. In particular, we capitalize on the fact that in most of them operations like matrix–vector multiplication and solving systems of linear equations are the main complexity bottlenecks. Since linear algebraic operations can be implemented very efficiently on GPGPUs,thenewparallelalgorithmsshowconsiderableruntime 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. Keywords Parallel model checking · General purpose graphics processing units
Dragan Bosnacki, Stefan Edelkamp, Damian Sulewski,
Added 15 May 2011
Updated 15 May 2011
Type Journal
Year 2011
Where STTT
Authors Dragan Bosnacki, Stefan Edelkamp, Damian Sulewski, Anton Wijs
Comments (0)
books