Thesis Details
GPU-Accelerated Synthesis of Probabilistic Programs
This paper examines the problem of automatic synthesis of probabilistic programs: having a finite family of candidate programs, how can one efficiently identify a program that satisfies a given specification. Even the most straightforward synthesis problems prove to be NP-hard. An improvement to this state of practice is brought by the PAYNT tool, which tackles this problem with a novel integrated technique for synthesising probabilistic programs. Even though it efficiently deals with the exponential growth of the family size, there is still a problem with the underlying state-space explosion. To solve this problem, we have implemented GPU-oriented model-checking algorithms that takes advantage of the GPU architecture and parallelise the task at a state level of a probabilistic model. The overall acceleration that we were able to achieve with this approach was, under certain conditions, close to the theoretically possible limit of the acceleration of the whole synthesis process.
Discrete-Time Markov Chains, Markov Decision Processes, Model-Checking, Synthesis of Probabilistic Programs, CUDA, Parallelisation
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT), člen
Drábek Vladimír, doc. Ing., CSc. (DCSY FIT BUT), člen
Peringer Petr, Dr. Ing. (DITS FIT BUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT), člen
Smrčka Aleš, Ing., Ph.D. (DITS FIT BUT), člen
@mastersthesis{FITMT24076,
author = "Vladim\'{i}r Marcin",
type = "Master's thesis",
title = "GPU-Accelerated Synthesis of Probabilistic Programs",
school = "Brno University of Technology, Faculty of Information Technology",
year = 2021,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/24076/"
}