Publication Details

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

ČEŠKA Milan, PILAŘ Petr, PAOLETTI Nicola, BRIM Luboš and KWIATKOWSKA Marta. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 9636. Berlin: Springer International Publishing, 2016, pp. 367-384. ISBN 978-3-662-49673-2. ISSN 0302-9743. Available from: http://dx.doi.org/10.1007/978-3-662-49674-9_21
Czech title
PRISM-PSY: Přesná syntéza parametrů pro stochastické systémy akcelerovaná na GPU
Type
conference paper
Language
english
Authors
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT)
Pilař Petr (FI MUNI)
Paoletti Nicola (UOx)
Brim Luboš, prof. RNDr., CSc. (FI MUNI)
Kwiatkowska Marta (UOx)
URL
Keywords

parameter synthesis, stochastic systems, data-parallel algorithms, GPU architectures 

Abstract

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.

Published
2016
Pages
367-384
Journal
Lecture Notes in Computer Science, vol. 9636, ISSN 0302-9743
Proceedings
Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Series
Lecture Notes in Computer Science
Conference
22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Eindhoven, The Netherlands, CZ
ISBN
978-3-662-49673-2
Publisher
Springer International Publishing
Place
Berlin, DE
DOI
UT WoS
000406428000021
EID Scopus
BibTeX
@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"
}
Back to top