User: Guest  Login
Document type:
Masterarbeit 
Author(s):
Schäffeler, Maximilian 
Title:
Verified solution methods for Markov decision processes 
Translated title:
Verifizierte Lösungsverfahren für Markov-Entscheidungsprozesse 
Abstract:
Markov decision processes (MDPs) allow modeling decision-making in systems that exhibit both random and deterministic behavior. In our work, we extend an existing formalization of MDPs in the interactive theorem prover Isabelle/HOL. First, we introduce policies that formalize the strategy of the decision-maker. To assign a value to policies, we add reward functions to the MDP formalization. The problem arises of how to find an optimal policy, one that maximizes the rewards accumulated over time...    »
 
Translated abstract:
Markov-Entscheidungsprozesse (MDPs) erlauben es, Systeme zu modellieren, die sowohl stochastisches als auch deterministisches Verhalten aufweisen. Das Verhalten des Systems wird dabei durch von einem Agenten durchgeführte Aktionen beeinflusst. Diese Arbeit erweitert eine bereits existierende Formalisierung von MDPs für den interaktiven Theorembeweiser Isabelle/HOL. Zuerst werden Strategien, die das Verhalten des Agenten beschreiben, formal eingeführt. Um diese Strategien zu bewerten und zu vergl...    »
 
Keywords:
Markov Decision Processes, Algorithms, Interactive Theorem Proving, Isabelle/HOL, Value Iteration, Dynamic Programming 
Subject:
DAT Datenverarbeitung, Informatik 
DDC:
000 Informatik, Wissen, Systeme 
Advisor:
Abdulaziz, Mohammad (Dr.) 
Referee:
Nipkow, Tobias (Prof., Ph.D.) 
Year:
2021 
Pages:
X, 56 S. 
Language:
en 
Language from translation:
de 
University:
Technische Universität München 
Faculty:
Fakultät für Informatik