Original title: Vylepšení syntézy kontrolerů pro POMDP s využitím abstrakce a podobnosti.
Translated title: Using inheritance dependencies to accelerate abstraction-based synthesis of finite-state controllers for POMDPs.
Authors: Shevchenko, Aleksandr ; Macák, Filip (referee) ; Češka, Milan (advisor)
Document type: Bachelor's theses
Year: 2024
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
Částečně pozorovatelný Markovský rozhodovací proces (POMDP) je důležitým modelem pro autonomní plánování, který se používá v mnoha oblastech, jako je robotika a biologie. Tato práce se zaměřuje na metodu Abstraction-Refinement pro induktivní syntézu konečně stavových kontrolérů (FSC) pro POMDP. Klasická verze AR vyžaduje model checking quotient MDP pro celou množinu kompatibilních akcí podrodiny v každé iteraci. My navrhujeme algoritmus, který využívá dědičné závislosti ke snížení velikosti masky pro quotient MDP a ke zrychlení model checkingu pro podrodiny FSC. Také představujeme chytrou verzi tohoto algoritmu, která zachovává všechny jeho výhody a snižuje jeho slabiny. Během experimentů se ukázalo, že náš přístup také ovlivňuje činnost jiných částí syntézy, jako je např. model building. V závislosti na modelu POMDP, pozorujeme jak zrychlení, tak zpomalení ve srovnání s AR. V průměru naše metoda zrychluje celkovou dobu syntézy 1.2 krát a v některých případech až desetkrát. Partially observable Markov decision process is an important model for autonomous planning used in many areas, such as robotics and biology. This work focuses on the Abstraction-Refinement framework for the inductive synthesis of finite-state controllers (FSCs) for POMDPs. The classic version of AR requires model checking of a quotient MDP for an entire set of compatible choices of the subfamily in each iteration. We propose an algorithm that uses inheritance dependencies to reduce the size of the quotient MDP’s mask and accelerate model checking for subfamilies of FSCs. We also introduce a smart version of this algorithm, which preserves all its advantages and reduces its weaknesses. During the experiments, it turned out that our approach also affects the operation of other parts of the synthesis, e.g. model building. Depending on the POMDP model, we observe both speedups and slowdowns in comparison to AR. On average, our approach speeds up the overall synthesis time by 1.2 times, and in some cases up to the factor 10.
Keywords: dědičné závislosti pro Markovské modely; model checking; syntéza konečně stavových kontrolérů; Částečně pozorovatelný Markovský rozhodovací proces; finite-state controller synthesis; inheritance dependencies for Markov models; model checking; Partially observable Markov decision process

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: https://hdl.handle.net/11012/246617

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


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