Benutzer: Gast  Login
Dokumenttyp:
Masterarbeit 
Autor(en):
Schäffeler, Maximilian 
Titel:
Verified solution methods for Markov decision processes 
Übersetzter Titel:
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...    »
 
übersetzter 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...    »
 
Stichworte:
Markov Decision Processes, Algorithms, Interactive Theorem Proving, Isabelle/HOL, Value Iteration, Dynamic Programming 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
DDC:
000 Informatik, Wissen, Systeme 
Betreuer:
Abdulaziz, Mohammad (Dr.) 
Gutachter:
Nipkow, Tobias (Prof., Ph.D.) 
Jahr:
2021 
Seiten/Umfang:
X, 56 S. 
Sprache:
en 
Sprache der Übersetzung:
de 
Hochschule / Universität:
Technische Universität München 
Fakultät:
Fakultät für Informatik