Detail práce

Syntéza pravděpodobnostních programů s optimální cenou

Bakalářská práce Student: Hranička Vojtěch Akademický rok: 2020/2021 Vedoucí: Češka Milan, doc. RNDr., Ph.D.
Název anglicky
Synthesis of Probabilistic Programs with Rewards
Jazyk práce
český
Abstrakt

Tato práce se zabývá syntézou pravděpodobnostních modelů s optimální cenou. Pravděpodobnostní syntéza slouží k automatickému návrhu systému, který splňuje požadované specifikace. V této práci se věnuji způsobu syntézy kde máme šablonu pro daný systém, která obsahuje neznámé části a cílem je najít takovou kombinaci nastavení daných částí tak, aby výsledný systém splňoval specifikované požadavky. V poslední době se objevují nové přístupy uvažující o množině řešení jako o rodině Markovových řetězců. Jedním z těchto přístupů je použití nové metody kombinující metody protipříklady řízeného zjemňování abstrakce a induktivní syntézy. Tato metoda svou efektivitou převyšuje ostatní metody pro pravděpodobnostní syntézu. V této práci se konkrétně zaměřuji na rozšíření specifikačního jazyka tohoto nástroje o možnost použití takzvaných rewardů a until vlastností. Díky těmto rozšířením je možné lépe a jednodušeji specifikovat hledané řešení. Experimenty demonstrují, že i po rozšíření daného nástroje o tyto možnosti specifikace jeho rychlost v porovnání se standardní metodou syntézy zůstává až o několik řádů efektivnější.

Klíčová slova

Syntéza pravděpodobnostních modelů, Markovovy modely

Ústav
Studijní program
Informační technologie
Soubory
Stav
obhájeno, hodnocení A
Obhajoba
15. června 2021
Oponent
Průběh obhajoby

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.

Otázky u obhajoby

Čím si vysvetľujete rýchlejšiu optimálnu syntézu pri použití hybridnej metódy oproti feasibility syntéze pri experimentoch herman1 a linka?

Viete vysvetliť akým spôsobom je expanzovaná množina C v algoritme 4 a 5?

Dotaz na detaily implementace.
Dotaz na úlohu kostky v experimentální části práce.

Komise
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT), předseda
Kořenek Jan, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Peringer Petr, Dr. Ing. (UITS FIT VUT), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS FIT VUT), člen
Citace
HRANIČKA, Vojtěch. Syntéza pravděpodobnostních programů s optimální cenou. Brno, 2021. Bakalářská práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2021-06-15. Vedoucí práce Češka Milan. Dostupné z: https://www.fit.vut.cz/study/thesis/24078/
BibTeX
@bachelorsthesis{FITBT24078,
    author = "Vojt\v{e}ch Hrani\v{c}ka",
    type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
    title = "Synt\'{e}za pravd\v{e}podobnostn\'{i}ch program\r{u} s optim\'{a}ln\'{i} cenou",
    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 = "czech",
    url = "https://www.fit.vut.cz/study/thesis/24078/"
}
Nahoru