Název: Využití protipříkladů v syntéze kontrolerů pro POMDP
Překlad názvu: Using Counter-Examples in Controller Synthesis for POMDPs
Autoři: Frejlach, Jakub ; Síč, Juraj (oponent) ; Češka, Milan (vedoucí práce)
Typ dokumentu: Diplomové práce
Rok: 2023
Jazyk: eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [eng] [cze]
Tato práce se zabývá částečně pozorovatelnými Markovskými rozhodovacími procesy \linebreak (POMDP), významnými stochastickými modely pro rozhodování za nejistoty a částečné pozorovatelnosti. POMDP lze aplikovat od navigace robotů až po samořídící vozidla. Nerozhodnutelný problém řízení POMDP vedl k různým přístupům, včetně konečných stavových kontrolerů (FSC) založených na pozorování a udržování histore v paměti. Identifikaci malých a ověřitelných FSC lze redukovat na syntézu Markovských řetězců. Tato práce se zaměřuje na induktivní syntézu řízenou protipříklady (CEGIS) implementovanou v rámci programu PAYNT a zkoumá využití Markovských rozhodovacích procesů jako protipříkladů. Je nastíněna nová hladová metoda pro konstrukci protipříkladů, která je implementována v programu PAYNT, která v některých případech vykazuje zlepšení oproti stávající metodě. This thesis examines partially observable Markov decision processes (POMDPs), a prominent stochastic model for decision-making under uncertainty and partial observability. POMDPs have diverse applications, from robot navigation to self-driving vehicles. The undecidable control problem of POMDPs has led to various approaches, including finite-state controllers (FSCs) based on observations and history. Identifying small and verifiable FSCs reduces the synthesis of Markov chains. This thesis focuses on counterexample-guided inductive synthesis (CEGIS) within the PAYNT program, exploring the use of Markov decision processes as counterexamples. A new greedy method for constructing counterexamples is outlined and implemented in PAYNT, showing improvements in some cases compared to the existing method.
Klíčová slova: counterexample guided inductive synthesis; finite-state controler synthesis; Markov models; partially observable Markov decision processes; probabilistic model checking; Markovské modely; pravděpodobnostní model checking; protipříklady řízená induktivní syntéza; syntéza konečně-stavových kontrolerů; částečné pozorovatelné Markovské rozhodovací procesy

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

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


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 > Diplomové práce