Original title: Induktivní syntéza kontrolérů pro POMDP vůči vlastnostem ve stabilním stavu
Translated title: Inductive Controller Synthesis for POMDPs with Respect to Steady-State Properties
Authors: Jarolím, Antonín ; Kozák, David (referee) ; Češka, Milan (advisor)
Document type: Bachelor'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á syntézou konečných automatů pro částečně pozorovatelné Markovovské rozhodovací procesy s ohledem na vlastnosti v ustáleném stavu. Množina přípustných kontrolérů je prozkoumávána pomocí state-of-the-art syntézních metod. Metoda Abstraction-Refinement (AR) prozkoumává tuto množinu tím, že bere v úvahu rodiny kontrolérů najednou. Byl navržen nový algoritmus generující proti-příklady vzhledem ke vlastnostem v ustáleném stavu, pomocí principů metody counterexample-guided inductive synthesis. V experimentální části se porovnává metoda AR se základní one-by-one metodou. Ukáže se, že metoda AR je rychlejší o několik řádů ve většině případů, s výjimkou jednoho, kde nízké hodnoty přechodů snížily její rychlost. Není k dispozici žádný jiný nástroj, který umí provádět takovou syntézu, takže porovnání s jinými přístupy nebylo možné. This thesis considers the problem of synthesizing finite-state controllers (FSC) for partially observable Markov decision processes wrt. steady-state properties. The set of candidate FSCs (design-space) is explored using state-of-the-art synthesis methods. The Abstraction-Refinement (AR) method prunes the design-space by considering families of FSCs at once. The novel algorithm generating counter-examples regarding steady-state properties using principles of the counterexample-guided inductive synthesis method is proposed. The experimental evaluation compares the AR method with a one-by-one exploration. It shows that the AR method is faster by orders of magnitude in all but one example, where the low transition rates reduced the speed of the AR method. No other tool is capable of performing such synthesis, so a comparison with other approaches is not available.
Keywords: abstrakce rodin Markovských řetězců; protipříklady; rodina konečných automatů; syntéza konečných automatů; vlastnosti ve stabilním stavu; částečně pozorovatelný Markovův rozhodovací proces; abstraction of Markov chains; counter-examples; family of finite state controllers; finite state controller synthesis; partially observable Markov decision process; steady-state properties

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

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


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