Název: Syntéza pravděpodobnostních programů s optimální cenou
Překlad názvu: Synthesis of Probabilistic Programs with Rewards
Autoři: Hranička, Vojtěch ; Síč, Juraj (oponent) ; Češka, Milan (vedoucí práce)
Typ dokumentu: Bakalářské práce
Rok: 2021
Jazyk: cze
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [cze] [eng]
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ší. This thesis pursues the synthesis of probabilistic programs with rewards. Probabilistic synthesis leads to the automatic proposal of a system which fulfills required specifications. In this thesis, I work with a form of synthesis where we have a sketch of a given system. This sketch includes unknown variables and the objective is to find a combination of configuration of given variables in order to have the final program meeting the specified requirements. Recently, new approaches considering a set of solutions as a family of Markov chain have appeared. One of these approaches is the usage of a new method combining counterexample-guided abstraction refinement and counterexample-guided inductive synthesis. This method exceeds other methods for synthesis of probabilistic programs with its efficiency. In this thesis, I concretely focus on extending this tool's specification language by adding a possibility of application of rewards and until properties. Thanks to these extensions it is possible to specify searched solution more efficiently. Experiments demonstrate that even after the addition of these possibilities of specifications the speed of a given tool remains by a margin of order of magnitudes more effective than the standard method of synthesis.
Klíčová slova: Markovovy modely; Syntéza pravděpodobnostních modelů; Markov models; Synthesis of probabilistic models

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/199423

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-610674


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Bakalářské práce