GPU-Accelerated Synthesis of Probabilistic Programs

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F22%3APU144844" target="_blank" >RIV/00216305:26230/22:PU144844 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

GPU-Accelerated Synthesis of Probabilistic Programs

Popis výsledku v původním jazyce

We consider automated synthesis methods for finite-state probabilistic programs satisfying a given temporal specification. Our goal is to accelerate the synthesis process using massively parallel graphical processing units (GPUs). The involved analysis of families of candidate programs is the main computational bottleneck of the process. We thus propose a state-level GPU-parallelisation of the model-checking algorithms for Markov chains and Markov decision processes that leverages the related but distinct topology of the candidate programs. For structurally complex families, we achieve a speedup of the analysis over one order of magnitude. This already leads to a considerable acceleration of the overall synthesis process and paves the way for further improvements.

Název v anglickém jazyce

GPU-Accelerated Synthesis of Probabilistic Programs

Popis výsledku anglicky

We consider automated synthesis methods for finite-state probabilistic programs satisfying a given temporal specification. Our goal is to accelerate the synthesis process using massively parallel graphical processing units (GPUs). The involved analysis of families of candidate programs is the main computational bottleneck of the process. We thus propose a state-level GPU-parallelisation of the model-checking algorithms for Markov chains and Markov decision processes that leverages the related but distinct topology of the candidate programs. For structurally complex families, we achieve a speedup of the analysis over one order of magnitude. This already leads to a considerable acceleration of the overall synthesis process and paves the way for further improvements.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GJ20-02328Y" target="_blank" >GJ20-02328Y: CAQtuS: Počítačem podporovaná kvantitativní syntéza</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2022

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

International Conference on Computer Aided Systems Theory (EUROCAST'22)

ISBN

978-3-031-25312-6

ISSN

—

e-ISSN

—

Počet stran výsledku

11

Strana od-do

256-266

Název nakladatele

Springer Nature Switzerland AG

Místo vydání

Cham

Místo konání akce

Las Palmas de Gran Canaria, Canary Islands

Datum konání akce

20. 2. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—