Publication Details
PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems
Pilař Petr (FIT)
Paoletti Nicola (FIT)
Brim Luboš, doc. RNDr., CSc. (CM-SFE)
Kwiatkowska Marta (FIT)
parameter synthesis, stochastic systems, data-parallel algorithms, GPU architectures
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 data-parallel 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 leveraged 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 speed-up of up to 31-fold on a single GPU compared to the sequential implementation.
@inproceedings{BUT130997,
author="Milan {Češka} and Petr {Pilař} and Nicola {Paoletti} and Luboš {Brim} and Marta {Kwiatkowska}",
title="PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems",
booktitle="Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems",
year="2016",
series="Lecture Notes in Computer Science",
journal="Lecture Notes in Computer Science",
volume="9636",
pages="367--384",
publisher="Springer International Publishing",
address="Berlin",
doi="10.1007/978-3-662-49674-9\{_}21",
isbn="978-3-662-49673-2",
issn="0302-9743",
url="http://dx.doi.org/10.1007/978-3-662-49674-9_21"
}