|
|
Optimizing Inductive Controller Synthesis Methods for POMDPs with Discounted Rewards Properties
Kříž, Ondřej ; Holík, Lukáš (oponent) ; Češka, Milan (vedoucí práce)
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.
|
|
|
Model-Based Reinforcement Learning for POMDPs
Smíšková, Lucie ; Andriushchenko, Roman (oponent) ; Češka, Milan (vedoucí práce)
Partially observable Markov decision processes allow us to model systems containing state uncertainty. They are useful when we have only partial information about the states ( so called observations). The aim of this thesis was to develop a method combining inductive synthesis and reinforcement learning to develop the best possible finite-state controller. This method was then implemented as an extension to the tool PAYNT.
|
|
|
Controlling Autonomous Systems Based on Partially Observable Markov Decision Processes
Gyselová, Julie ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
Partially observable Markov decision processes offer a way to model systems with state uncertainty. An agent has limited information (observation) about its current location in the system. A finite-state controller that translates this information to actions that the agent can perform helps the agent interact with the model and achieve its goals. PAYNT is a tool that constructs a design space that contains all possible finite-state controllers of a given size for a POMDP and then tries to find the best FSC among those. In this thesis, I introduce a way to restrict the design space to encode only a subset of the controllers so that PAYNT can find the best controller in a much shorter time. If the used restriction is suitable, the controller quality is not affected. I also implement a method that can make the synthesis method implemented in PAYNT continuously find FSCs of increasing sizes and improving qualities by gradually applying restrictions from a predefined set.
|
|
|
Using Counter-Examples in Controller Synthesis for POMDPs
Frejlach, Jakub ; Síč, Juraj (oponent) ; Češka, Milan (vedoucí práce)
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.
|
|
|
Controlling Autonomous Systems Based on Partially Observable Markov Decision Processes
Gyselová, Julie ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
Partially observable Markov decision processes offer a way to model systems with state uncertainty. An agent has limited information (observation) about its current location in the system. A finite-state controller that translates this information to actions that the agent can perform helps the agent interact with the model and achieve its goals. PAYNT is a tool that constructs a design space that contains all possible finite-state controllers of a given size for a POMDP and then tries to find the best FSC among those. In this thesis, I introduce a way to restrict the design space to encode only a subset of the controllers so that PAYNT can find the best controller in a much shorter time. If the used restriction is suitable, the controller quality is not affected. I also implement a method that can make the synthesis method implemented in PAYNT continuously find FSCs of increasing sizes and improving qualities by gradually applying restrictions from a predefined set.
|
host ::
RSS.