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. We solve the problem by formalizing its Bellman equation and give conditions under which an optimal policy exists. Based on these developments, we verify the value iteration and policy iteration algorithms which compute (close to) optimal policies. This formalization may serve as a basis for future work on reinforcement learning algorithms, planning under uncertainty, and partially observable MDPs.     «

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...     »

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 vergleichen, wird die existierende Formalisierung um eine Belohnungsfunktion ergänzt. Es stellt sich nun das Problem eine Strategie zu finden, welche die Belohnungen, die im Verlauf der Zeit gesammelt werden, maximiert. Zur Lösung wird die Bellman-Gleichung für dieses Problem formal hergeleitet und Bedingungen formuliert, unter denen eine optimale Strategie existiert. Basierend auf diesen Formalisierungen stellt die Arbeit verifizierte Versionen des Value-Iteration-Verfahren und des Policy-Iteration-Verfahren bereit, die (nahezu) optimale Strategien berechnen. Die hier entwickelte Formalisierung kann in Zukunft als Basis für Verifikationsprojekte im Zusammenhang mit bestärkendem Lernen und Planungsproblemen in der KI dienen.     «

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...     »