Original title: Využití protipříkladů v syntéze kontrolerů pro POMDP
Translated title: Using Counter-Examples in Controller Synthesis for POMDPs
Authors: Frejlach, Jakub ; Síč, Juraj (referee) ; Češka, Milan (advisor)
Document type: Master’s theses
Year: 2023
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [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.
Keywords: 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; counterexample guided inductive synthesis; finite-state controler synthesis; Markov models; partially observable Markov decision processes; probabilistic model checking

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

Permalink: http://www.nusl.cz/ntk/nusl-531437


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Master’s theses