Original title:
Computer-Aided Synthesis of Probabilistic Models
Translated title:
Computer-Aided Synthesis of Probabilistic Models
Authors:
Andriushchenko, Roman ; Lengál, Ondřej (referee) ; Češka, Milan (advisor) Document type: Master’s theses
Year:
2020
Language:
eng Publisher:
Vysoké učení technické v Brně. Fakulta informačních technologií Abstract:
[eng][cze]
Předkládaná práce se zabývá problémem automatizované syntézy pravděpodobnostních systémů: máme-li rodinu Markovských řetězců, jak lze efektivně identifikovat ten který odpovídá zadané specifikaci? Takové rodiny často vznikají v nejrůznějších oblastech inženýrství při modelování systémů s neurčitostí a rozhodování i těch nejjednodušších syntézních otázek představuje NP-těžký problém. V dané práci my zkoumáme existující techniky založené na protipříklady řízené induktivní syntéze (counterexample-guided inductive synthesis, CEGIS) a na zjemňování abstrakce (counterexample-guided abstraction refinement, CEGAR) a navrhujeme novou integrovanou metodu pro pravděpodobnostní syntézu. Experimenty nad relevantními modely demonstrují, že navržená technika je nejenom srovnatelná s moderními metodami, ale ve většině případů dokáže výrazně překonat, někdy i o několik řádů, existující přístupy.
This thesis considers the problem of automated synthesis of probabilistic systems: having a family of Markov chains, how can one efficiently identify a chain satisfying a given specification? Such families often arise in various domains of engineering when modeling systems under uncertainty, and deciding even the simplest problems shows to be NP-hard. To tackle this problem, we adopt the principles of counterexample-guided inductive synthesis (CEGIS) and abstraction refinement (CEGAR) and develop a novel integrated technique for probabilistic synthesis. Experiments on practically relevant case studies demonstrate that the designed technique is not only comparable to state-of-the-art synthesis approaches, in most cases it manages to significantly outperform existing methods, sometimes by a margin of orders of magnitude.
Keywords:
Markovovy modely; probabilistický model checking; syntéza pravděpodobnostních modelů; Markov models; probabilistic model checking; synthesis of probabilistic models
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/192498