Original title:
Syntéza pravděpodobnostních programů s optimální cenou
Translated title:
Synthesis of Probabilistic Programs with Rewards
Authors:
Hranička, Vojtěch ; Síč, Juraj (referee) ; Češka, Milan (advisor) Document type: Bachelor's theses
Year:
2021
Language:
cze Publisher:
Vysoké učení technické v Brně. Fakulta informačních technologií Abstract:
[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.
Keywords:
Markov models; Synthesis of probabilistic models; Markovovy modely; Syntéza pravděpodobnostních modelů
Institution: Brno University of Technology
(web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library. Original record: http://hdl.handle.net/11012/199423