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