Nicht-Mehrdeutigkeit, Alternierung und Nichtstandardakzeptanz in automatenbasierter Modellprüfung probabilistischer Systeme
Zusammenfassung der Projektergebnisse
Das Projekt befasst sich mit der quantitativen Analyse von probabilistischen Systemen, modelliert durch Markovketten und Markov Entscheidungsprozesse (englische Abkürzung MDP für Markov decision process), gegen Linearzeiteigenschaften, dargestellt durch temporallogische Formeln. Der bekannteste Ansatz, der in mehreren Tools realisiert wurde, transformiert die Formel in einen deterministischen Rabin-Automaten (DRA) und analysiert das Produkt des Systemmodells und Automaten. Die Komplexität dieses Ansatzes ist doppelt exponentiell in der Formellänge und polynomiell in der Modellgröße. Aus komplexitätstheoretischer Sicht ist dies optimal für MDPs, nicht jedoch für Markovketten. Für diese sind effizientere Algorithmen mit einer einfach exponentiellen Zeitschranke bekannt. Hierzu zählt ein iteratives automatenloses Verfahren sowie automatenbasierte Ansätze mit separierten (stark nicht-mehrdeutigen) und alternierenden Automaten. Zum Projektstart 2016 waren keine Implementierungen der einfach exponentiellen Methoden bekannt. Zu den Hauptergebnissen des Projekts zählen Analysealgorithmen für Markovketten, die mit nichtmehrdeutigen (engl. unambiguous) Automaten zur Darstellung ω-regulärer Spezifikationen arbeiten. Damit wurde ein fehlerhafter Algorithmus der Literatur zum Einsatz von nicht-mehrdeutigen Büchi-Automaten (Abkürzung UBA für unambiguous Büchi automata) für die formale Analyse von Markovketten korrigiert. Neben der eigentlichen UBA-basierten Analyse wurden auch Algorithmen für die Erzeugung von UBA für Formeln der Logik LTL (linear temporal logic) sowie nicht-mehrdeutige Automaten mit anderen Akzeptanzbedingungen untersucht. In vergleichenden experimentellen Studien zeigte sich der UBA-basierte Ansatz kompetitiv mit dem sonst üblichen Verfahren mit deterministischen Automaten, in einigen Fällen auch überlegen. Weiteres Hauptziel des Projekts war es, deterministische Automaten mit symbolischen Darstellungsformen von Muller-Akzeptanz (anstelle von Rabin-Akzeptanz) und deren Nutzen für die quantitative Analyse sowohl von Markovketten und MDPs zu untersuchen, insbesondere in Hinblick auf eine Abwägung zwischen den Vorzügen, die flexiblere Akzeptanzbedingungen hinsichtlich der Automatengröße bieten können, und des gesteigerten Berechnungsaufwands der notwendigen Graphanalyse im Produkt des Systemmodells und des Automaten.
Projektbezogene Publikationen (Auswahl)
-
Markov Chains and Unambiguous Büchi Automata. Lecture Notes in Computer Science, 23-42. Springer International Publishing.
Baier, Christel; Kiefer, Stefan; Klein, Joachim; Klüppelholz, Sascha; Müller, David & Worrell, James
-
Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata. International Journal on Software Tools for Technology Transfer, 20(2), 179-194.
Klein, Joachim; Baier, Christel; Chrszon, Philipp; Daum, Marcus; Dubslaff, Clemens; Klüppelholz, Sascha; Märcker, Steffen & Müller, David
-
LTL to Deterministic Emerson-Lei Automata. Electronic Proceedings in Theoretical Computer Science, 256, 180-194.
Müller, David & Sickert, Salomon
-
Parametric Markov Chains: PCTL Complexity and Fraction-free Gaussian Elimination. Electronic Proceedings in Theoretical Computer Science, 256, 16-30.
Hutschenreiter, Lisa; Baier, Christel & Klein, Joachim
-
Alternative automata-based approaches to probabilistic model checking. Doktorarbeit, Technische Universität Dresden, Germany, 2019
David Müller
-
From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata. Lecture Notes in Computer Science, 262-279. Springer International Publishing.
Jantsch, Simon; Müller, David; Baier, Christel & Klein, Joachim
-
Generic Emptiness Check for Fun and Profit. Lecture Notes in Computer Science, 445-461. Springer International Publishing.
Baier, Christel; Blahoudek, František; Duret-Lutz, Alexandre; Klein, Joachim; Müller, David & Strejček, Jan
-
Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. Information and Computation, 272, 104504.
Baier, Christel; Hensel, Christian; Hutschenreiter, Lisa; Junges, Sebastian; Katoen, Joost-Pieter & Klein, Joachim
-
Determinization and Limit-Determinization of Emerson-Lei Automata. Lecture Notes in Computer Science, 15-31. Springer International Publishing.
John, Tobias; Jantsch, Simon; Baier, Christel & Klüppelholz, Sascha
-
From LTL to unambiguous Büchi automata via disambiguation of alternating automata. Formal Methods in System Design, 58(1-2), 42-82.
Jantsch, Simon; Müller, David; Baier, Christel & Klein, Joachim
-
Certificates and Witnesses for Probabilistic Model Checking. Doktorarbeit, Technische Universität Dresden, Germany, 2022
Simon Jantsch
-
From Emerson-Lei automata to deterministic, limit-deterministic or good-for-MDP automata. Innovations in Systems and Software Engineering, 18(3), 385-403.
John, Tobias; Jantsch, Simon; Baier, Christel & Klüppelholz, Sascha
-
Markov chains and unambiguous automata. Journal of Computer and System Sciences, 136, 113-134.
Baier, Christel; Kiefer, Stefan; Klein, Joachim; Müller, David & Worrell, James
