PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems

Milan Ceska, Petr Pilar, Nicola Paoletti, Lubos Brim, Marta Kwiatkowska
Department of Computer Science, University of Oxford, UK
22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016


   title={PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems},

   author={Ce{v{s}}ka, Milan and Pilar, Petr and Paoletti, Nicola and Brim, Lubo{v{s}} and Kwiatkowska, Marta},



Download Download (PDF)   View View   Source Source   



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 hardware utilisation, essential for performance and scalability, is achieved by state space and parameter space parallelisation: the former leverages a compact sparse-matrix representation, and the latter is based on an iterative decomposition of the parameter space. Our experiments on several biological and engineering case studies demonstrate an overall speedup of up to 31-fold on a single GPU compared to the sequential implementation.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2024 hgpu.org

All rights belong to the respective authors

Contact us: