Publication Details
PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems
Pilař Petr (FI MUNI)
Paoletti Nicola (UOx)
Brim Luboš, prof. RNDr., CSc. (FI MUNI)
Kwiatkowska Marta (UOx)
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{FITPUB11208,
author = "Milan \v{C}e\v{s}ka and Petr Pila\v{r} and Nicola Paoletti and Lubo\v{s} Brim and Marta Kwiatkowska",
title = "PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems",
pages = "367--384",
booktitle = "Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems",
series = "Lecture Notes in Computer Science",
journal = "Lecture Notes in Computer Science",
volume = 9636,
year = 2016,
location = "Berlin, DE",
publisher = "Springer International Publishing",
ISBN = "978-3-662-49673-2",
ISSN = "0302-9743",
doi = "10.1007/978-3-662-49674-9\_21",
language = "english",
url = "https://www.fit.vut.cz/research/publication/11208"
}