Verifikation von Markov Entscheidungsprozessen in diskreter Zeit

Abstract

Diese Arbeit beschäftigt sich mit der Verifikation von probabilistischen Systemen in diskreter Zeit, insbesondere Markov Entscheidungsprozessen (MDP). Sie beinhaltet sowohl theoretische als auch praktische Fortschritte, aufgeteilt in vier Bereiche. Zuerst wird eine jahrzehntealte offene Frage bezüglich mean payoff Problemen gelöst und, basierend auf der Antwort, neue Algorithmen präsentiert, die als erste solche Probleme effizient berechnen. Dann wird eine effiziente und flexible Implementierung von LTL-zu-Automaten Übersetzungsalgorithmen gezeigt, die unter Anderem im Kontext der probabilistischen Verifikation von LTL Formeln eine zentrale Rolle spielt. Als Drittes wird das fundamental neue Konzept des Kerns eines MDP präsentiert, eine flexible Grundlage um approximative Berechnungen auf MDP zu beschleunigen. Zuletzt wird ein wichtiger Schritt in Richtung risikobewusster Analyse von probabilistischen Systemen diskutiert.