Konferenzbeitrag
Verifikation von Markov Entscheidungsprozessen in diskreter Zeit
Lade...
Volltext URI
Dokumententyp
Text/Conference Paper
Zusatzinformation
Datum
2022
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Quelle
Verlag
Köllen Druck + Verlag GmbH
Zusammenfassung
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.