Název:
Computer-Aided Synthesis of Probabilistic Models
Překlad názvu:
Computer-Aided Synthesis of Probabilistic Models
Autoři:
Andriushchenko, Roman ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce) Typ dokumentu: Diplomové práce
Rok:
2020
Jazyk:
eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [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.
Klíčová slova:
Markov models; probabilistic model checking; synthesis of probabilistic models; Markovovy modely; probabilistický model checking; syntéza pravděpodobnostních modelů
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/192498