Unambiguity, alternation and non-standard acceptance in automata-based probabilistic model checking
Final Report Abstract
The project deals with the quantitative analysis of probabilistic systems, modeled by Markov chains and Markov decision processes (MDPs), with respect to linear-time properties represented by temporal logic formulas. The most well-known approach, which has been implemented in several tools, transforms the formula into a deterministic Rabin automaton (DRA) and analyzes the product of the system model and the automaton. The complexity of this approach is double-exponential in the length of the formula and polynomial in the model size. From a complexity-theoretic perspective, this is optimal for MDPs but not for Markov chains. For Markov chains, more efficient algorithms with a single-exponential time bound are known. These include an iterative automaton-free procedure as well as automaton-based approaches with separated (strongly unambiguous) and alternating automata. At the start of the project in 2016, no implementations of the single-exponential methods were known. The main results of the project include analysis algorithms for Markov chains that use unambiguous automata to represent ω-regular specifications. We hereby corrected a flawed algorithm of the literature regarding the use of unambiguous Büchi automata (UBA) for the formal analysis of Markov chains. In addition to the actual UBA-based analysis, algorithms for the generation of UBAs for formulas in LTL (linear temporal logic) and unambiguous automata with other acceptance conditions were also investigated. In comparative experimental studies, the UBA-based approach proved to be competitive with the commonly used approach based on deterministic automaton, and even superior in some cases. Another main goal of the project was to investigate deterministic automata with symbolic representations of Muller acceptance (instead of Rabin acceptance) and their usefulness for the quantitative analysis of both Markov chains and MDPs. A key focus is balancing the advantages that more flexible acceptance conditions can offer in terms of automaton size with the increased computational effort required for graph analysis in the product of the system model and the automaton.
Publications
-
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
