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

D 2016

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

ČEŠKA, Milan, Petr PILAŘ, Nikola PAOLETTI, Luboš BRIM, Marta KWIATKOWSKA et. al.

Základní údaje

Originální název

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

Název česky

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

Autoři

ČEŠKA, Milan (203 Česká republika), Petr PILAŘ (203 Česká republika, domácí), Nikola PAOLETTI (826 Velká Británie a Severní Irsko), Luboš BRIM (203 Česká republika, garant, domácí) a Marta KWIATKOWSKA (826 Velká Británie a Severní Irsko)

Vydání

LNCS 9636. Berlin, 22nd International Conference, TACAS 2016, od s. 367-384, 18 s. 2016

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00088144

Organizační jednotka

Fakulta informatiky

ISBN

978-3-662-49673-2

ISSN

DOI

http://dx.doi.org/10.1007/978-3-662-49674-9_21

UT WoS

000406428000021

Klíčová slova anglicky

GPU; stochastic systems; model checking; parameter synthesis

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 16. 4. 2019 09:41, prof. RNDr. Luboš Brim, CSc.

Anotace

V originále

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 leverages 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 speedup of up to 31-fold on a single GPU compared to the sequential implementation.

Návaznosti

GA15-11089S, projekt VaV

Název: Získávání parametrů biologických modelů pomocí techniky ověřování modelů

Investor: Grantová agentura ČR, Získávání parametrů biologických modelů pomocí techniky ověřování modelů

Citovat

ČEŠKA, Milan, Petr PILAŘ, Nikola PAOLETTI, Luboš BRIM a Marta KWIATKOWSKA. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. In Marsha Chechik, Jean-François Raskin. 22nd International Conference, TACAS 2016. LNCS 9636. Berlin: Springer International Publishing, 2016, s. 367-384. ISBN 978-3-662-49673-2. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49674-9_21.

@inproceedings{1354080,
   author = {Češka, Milan and Pilař, Petr and Paoletti, Nikola and Brim, Luboš and Kwiatkowska, Marta},
   address = {Berlin},
   booktitle = {22nd International Conference, TACAS 2016},
   doi = {http://dx.doi.org/10.1007/978-3-662-49674-9_21},
   edition = {LNCS 9636},
   editor = {Marsha Chechik, Jean-François Raskin},
   keywords = {GPU; stochastic systems; model checking; parameter synthesis},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Berlin},
   isbn = {978-3-662-49673-2},
   pages = {367-384},
   publisher = {Springer International Publishing},
   title = {PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems},
   year = {2016}
}

TY  - JOUR
ID  - 1354080
AU  - Češka, Milan - Pilař, Petr - Paoletti, Nikola - Brim, Luboš - Kwiatkowska, Marta
PY  - 2016
TI  - PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems
PB  - Springer International Publishing
CY  - Berlin
SN  - 9783662496732
KW  - GPU
KW  - stochastic systems
KW  - model checking
KW  - parameter synthesis
N2  - 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 leverages 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 speedup of up to 31-fold on a single GPU compared to the sequential implementation.
ER  -

ČEŠKA, Milan, Petr PILAŘ, Nikola PAOLETTI, Luboš BRIM a Marta KWIATKOWSKA. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. In Marsha Chechik, Jean-Fran\c cois Raskin. \textit{22nd International Conference, TACAS 2016}. LNCS 9636. Berlin: Springer International Publishing, 2016, s.~367-384. ISBN~978-3-662-49673-2. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49674-9\_{}21.

Podrobný výpis o publikaci