Název:
Pokročilé metody pro syntézu pravděpodobnostních programů
Překlad názvu:
Advanced Methods for Synthesis of Probabilistic Programs
Autoři:
Stupinský, Šimon ; Holík, Lukáš (oponent) ; Češka, Milan (vedoucí práce) Typ dokumentu: Diplomové práce
Rok:
2021
Jazyk:
eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [eng][cze]
Pravdepodobnostné programy zohrávajú rozhodujúcu úlohu v rôznych technických doménach, ako napríklad počítačové siete, vstavané systémy, stratégie riadenia spotreby energie alebo softvérové produčkné linky. PAYNT je nástroj na automatizovanú syntézu pravdepodobnostných programov vyhovujúcich zadaným špecifikáciam. V tejto práci rozširujeme tento nástroj predovšetkým o podporu optimálnej syntézy a syntézy viacerých špecifikácií. Ďalej sme navrhli a implementovali novú metódu, ktorá dokáže efektívne syntetizovať parametre so spojitým definičným oborom ovplyvňujúce pravdepodobnostné prechody popri syntéze topológie programov, t.j., podporu pre syntézu topológie aj parametrov súčasne. Demonštrujeme užitočnosť a výkonnosť nástroja PAYNT na širokej škále prípadových štúdií z rôznych aplikačných domén ktoré majú uplatnenie v reálnom svete. Pri náročných problémoch syntézy môže PAYNT výrazne znížiť dobu behu až z dní na minúty a zároveň zaistiť úplnosť procesu syntézy.
Probabilistic programs play a crucial role in various engineering domains, including computer networks, embedded systems, power management policies, or software product lines. PAYNT is a tool for the automatic synthesis of probabilistic programs satisfying the given specifications. In this thesis, we extend this tool primarily to support optimal synthesis and synthesis for multi-property specifications. Further, we have proposed and implemented a new method that can efficiently synthesise continuous parameters affecting the transition probabilities alongside the synthesis of a program topology, i.e., support of both topology and parameter synthesis at the same time. We demonstrate the usefulness and performance of PAYNT on a wide range of real-world case studies from various application domains. For challenging synthesis problems, PAYNT can significantly decrease the run-time from days to minutes while ensuring the completeness of the synthesis process.
Klíčová slova:
automated synthesis; Markov models; model checking; probabilistic programs; automatizovaná syntéza; Markovské modely; model checking; pravdepododnostné programy
Instituce: Vysoké učení technické v Brně
(web)
Informace o dostupnosti dokumentu:
Plný text je dostupný v Digitální knihovně VUT. Původní záznam: http://hdl.handle.net/11012/200211