Name
Abstract | ||
|---|---|---|
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, the new parallel algorithms show 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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/s10009-010-0176-4 | STTT |
Keywords | Field | DocType |
standard architecture,parallel algorithm,parallel model checking · general purpose graphics processing units,linear equation,general purpose graphics processor,prototype implementation,probabilistic model checker,linear algebraic operation,parallel probabilistic model checking,new parallel algorithm,case study,standard cpu implementation,probabilistic model,linear equations,linear algebra | Model checking,CUDA,Parallel algorithm,Computer science,Parallel computing,Probabilistic analysis of algorithms,Theoretical computer science,Multiplication,Matrix multiplication,Algebraic operation,Speedup | Journal |
Volume | Issue | ISSN |
13 | 1 | 1433-2787 |
Citations | PageRank | References |
16 | 0.69 | 32 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dragan Bošnački | 1 | 113 | 7.22 |
| Stefan Edelkamp | 2 | 1557 | 125.46 |
| Damian Sulewski | 3 | 87 | 6.45 |
| Anton Wijs | 4 | 203 | 22.84 |