Original title: Optimalizace induktivní syntézy kontrolérů pro POMDP s časově omezenými cenami
Translated title: Optimizing Inductive Controller Synthesis Methods for POMDPs with Discounted Rewards Properties
Authors: Kříž, Ondřej ; Holík, Lukáš (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]
Pravděpodobnostní kontrola modelů je nezbytnou součástí verifikace systémů v různých prostředích. Klíčová limitace nástroje PAYNT, který syntetizuje pravděpodobnostní programy splňující danou specifikaci, leží v jeho zacházení s diskontními vlastnostmi. Tato práce rozšiřuje rámec nástroje STORM, na němž je postaven PAYNT, implementací diskontní iterace hodnot v rámci procesu induktivní syntézy. Diskontní iterace hodnot byla implementována v rámci STORMu, včetně identifikace vhodného prostředí pro řešitele, rozhodovacích segmentů v kódu a Gauss-Seidelovým násobením pro vylepšené výpočetní schopnosti. Nezbytnost použití vzorce v jazyce PRISM v rámci kontroly modelů v PAYNTu představuje problém pro vynechání diskontní transformace, která ztěžuje kontrolu modelu. Proto byla diskontní transformace ponechána s diskontním faktorem blízkým k jedné, a jsou porovnávány hodnoty potenciálních optim, které vrací diskontní a nediskontní iterace hodnot. Tato práce zlepšuje práci PAYNTu a STORMu s diskontními hodnotami a poskytuje základ pro další pokroky ve vývoji PAYNTu a STORMu. Probabilistic model checking is essential for verifying systems in diverse domains. A key limitation of the PAYNT tool, which synthesises probabilistic programs satisfying given specifications, lies in its handling of discounted properties. This thesis extends the STORM framework upon which PAYNT is built, incorporating the discounted value iteration method within inductive synthesis process to address this issue. The discounted value iteration function was developed within STORM, involving solver environment identification, decision-making segments in the code, and Gauss-Seidel multiplication for enhanced computational capabilities. The necessity for a PRISM formula in PAYNT's model checking process presented challenges for bypassing the discount factor transformation step. To overcome this, a discount factor transformation with a factor close to one was employed, comparing potential optima vectors between discounted and undiscounted iterations. This study improves discounted property handling in PAYNT and the STORM framework, providing a foundation for further advancements in the development of PAYNT.
Keywords: induktivní syntéza; Markovské rozhodovací procesy s částečným pozorováním; časově omezené ceny; discounted reward properties; inductive synthesis; Partially observable Markov decision processes

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

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


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