15428
Milan Ceska, Petr Pilar, Nicola Paoletti, Lubos Brim, Marta Kwiatkowska
In this paper we present PRISM-PSY, a novel tool that performs precise GPU-accelerated parameter synthesis for continuous-time Markov chains and time-bounded temporal logic specifications. We redesign, in terms of matrix-vector operations, the recently formulated algorithms for precise parameter synthesis in order to enable effective dataparallel processing, which results in significant acceleration on many-core architectures. High […]
View View   Download Download (PDF)   
Elise Cormie-Bowins
We consider the problem of computing reachability probabilities: given a Markov chain, an initial state of the Markov chain, and a set of goal states of the Markov chain, what is the probability of reaching any of the goal states from the initial state? This problem can be reduced to solving a linear equation Ax=b […]
View View   Download Download (PDF)   
Anton J. Wijs, Dragan Bosnacki
We present several methods to improve the run times of probabilistic model checking on general-purpose graphics processing units (GPUs). The methods enhance sparse matrix-vector multiplications, which are in the core of the probabilistic model checking algorithms. The improvement is based on the analysis of the transition matrix structures corresponding to state spaces of a selection […]
Damian Sulewski
The evolution of science is a double-track process composed of theoretical insights on the one hand and practical inventions on the other one. While in most cases new theoretical insights motivate hardware developers to produce systems following the theory, in some cases the shown hardware solutions force theoretical research to forecast the results to expect. […]
View View   Download Download (PDF)   
Jiri Barnat, Petr Bauch, Lubos Brim, and Milan Ceska
Recent technological developments made various many-core hardware platforms widely accessible. These massively parallel architectures have been used to significantly accelerate many computation demanding tasks. In this paper, we show how the algorithms for LTL model checking can be redesigned in order to accelerate LTL model checking on many-core GPU platforms. Our detailed experimental evaluation demonstrates […]
View View   Download Download (PDF)   
Dragan Bosnacki, Stefan Edelkamp, Damian Sulewski, Anton Wijs
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 […]
View View   Download Download (PDF)   
Dragan Bosnacki, Stefan Edelkamp, Damian Sulewski, Anton Wijs
We present an extension of the model checker PRISM for (general purpose) graphics processing units (GPUs). The extension is based on parallel algorithms for probabilistic model checking which are tuned for GPUs. In particular, we parallelize the parts of the algorithms that boil down to linear algebraic operations, like solving systems of linear equations and […]
View View   Download Download (PDF)   
Dragan Bosnacki, Stefan Edelkamp, Damian Sulewski
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 […]
View View   Download Download (PDF)   

* * *

* * *

Follow us on Twitter

HGPU group

1752 peoples are following HGPU @twitter

Like us on Facebook

HGPU group

371 people like HGPU on Facebook

HGPU group © 2010-2016 hgpu.org

All rights belong to the respective authors

Contact us: