Detail výsledku
PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems
Pilař Petr
Paoletti Nicola
Brim Luboš, doc. RNDr., CSc.
Kwiatkowska Marta
In this paper we present PRISM-PSY, a novel tool thatperforms 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 onmany-core architectures. High hardware utilisation, essential for performance and scalability, is achieved by state space and parameter spaceparallelisation: 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 casestudies demonstrate an overall speed-up of up to 31-fold on a single GPUcompared to the sequential implementation.
parameter synthesis, stochastic systems, data-parallel algorithms, GPU architectures
@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"
}