Detail práce
GPU-Accelerated Synthesis of Probabilistic Programs
V tejto práci sa zoberáme problémom automatizovanej syntézy pravdepodobnostných programov: majme konečnú rodinu kandidátnych programov, v ktorej chceme efektívne identifikovať program spĺňajúci danú špecifikáciu. Aj riešenie tých najjednoduchších syntéznych problémov v praxi predstavuje NP-ťažký problém. Pokrok v tejto oblasti prináša nástroj Paynt, ktorý na riešenie tohto problému používa novú integrovanú metódu syntézy pravdepodobnostných programov. Aj keď sa tento prístup dokáže efektívne vysporiadať s exponenciálnym rastom rodín kandidátnych riešení, stále tu existuje problém spôsobený exponenciálnym rastom jednotlivých členov týchto rodín. S cieľom vysporiadať sa aj s týmto problémom, sme implementovali GPU orientované algoritmy slúžiace na overovanie kandidátnych programov (modelov), ktoré danú úlohu paralelizujú na stavovej úrovni pravdepodobnostých modelov. Celkové zrýchlenie doshiahnuté týmto prístupom za určitých podmienok potom prinieslo takmer teoretický limit možného zrýchlenia syntézneho procesu.
diskrétne Markovove reťazce, Markovove rozhodovacie procesy, overovanie modelov, syntéza pravdepodobnostných programov, CUDA, paralelizácia
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm A.
- V kapitole 6 je výkonnost jednotlivých metod pro Model Checking analyzována na několika modelech, pro každý model se v tabulkách nachází ještě několik variant různých velikostí, jak tyto varianty vznikly?
- Existuje možnost zahrnutí implementovaného rozšíření do stabilní verze nástroje STORM?
- Zvažujete publikování dosažených výsledků?
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT), člen
Drábek Vladimír, doc. Ing., CSc. (UPSY FIT VUT), člen
Peringer Petr, Dr. Ing. (UITS FIT VUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT), člen
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT), člen
@mastersthesis{FITMT24076,
author = "Vladim\'{i}r Marcin",
type = "Diplomov\'{a} pr\'{a}ce",
title = "GPU-Accelerated Synthesis of Probabilistic Programs",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2021,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/24076/"
}