Efficient probabilistic model checking on general purpose graphic processors

D. Bosnacki, S. Edelkamp, D. Sulewski

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

18 Citations (Scopus)
1 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationModel Checking Software (16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. Proceedings)
EditorsC.S. Pasareanu
Place of PublicationBerlin
ISBN (Print)978-3-642-02651-5
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Efficient probabilistic model checking on general purpose graphic processors'. Together they form a unique fingerprint.

Cite this