Conference paper

Č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. 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
Publication language:english
Original title:PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems
Title (cs):PRISM-PSY: Přesná syntéza parametrů pro stochastické systémy akcelerovaná na GPU
Pages:367-384
Proceedings:Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Conference:22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Series:LNCS 9636
Place:Berlin, DE
Year:2016
URL:http://dx.doi.org/10.1007/978-3-662-49674-9_21
ISBN:978-3-662-49673-2
Journal:Lecture Notes in Computer Science, Vol. 2016, No. 9636, DE
ISSN:0302-9743
DOI:10.1007/978-3-662-49674-9_21
Publisher:Springer International Publishing
Keywords
parameter synthesis, stochastic systems, data-parallel algorithms, GPU architectures 
Annotation
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.
BibTeX:
@INPROCEEDINGS{
   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 = {LNCS 9636},
   journal = {Lecture Notes in Computer Science},
   volume = {2016},
   number = {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 = {http://www.fit.vutbr.cz/research/view_pub.php?id=11208}
}

Your IPv4 address: 54.92.182.0
Switch to IPv6 connection

DNSSEC [dnssec]