- Authors
- David Müller Technische Universität Dresden, Fakultät Informatik, Institut für Theoretische Informatik, Lehrstuhl für Algebraische und Logische Grundlagen der Informatik
- title
- Alternative Automata-based Approaches to Probabilistic Model Checking
- Please use the following URL when quoting:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-361005
- Date of submission
- 16.10.2018
- Date of defense
- 10.12.2018
- Abstract (EN)
- In this thesis we focus on new methods for probabilistic model checking (PMC) with linear temporal logic (LTL). The standard approach translates an LTL formula into a deterministic ω-automaton with a double-exponential blow up. There are approaches for Markov chain analysis against LTL with exponential runtime, which motivates the search for non-deterministic automata with restricted forms of non-determinism that make them suitable for PMC. For MDPs, the approach via deterministic automata matches the double-exponential lower bound, but a practical application might benefit from approaches via non-deterministic automata. We first investigate good-for-games (GFG) automata. In GFG automata one can resolve the non-determinism for a finite prefix without knowing the infinite suffix and still obtain an accepting run for an accepted word. We explain that GFG automata are well-suited for MDP analysis on a theoretic level, but our experiments show that GFG automata cannot compete with deterministic automata. We have also researched another form of pseudo-determinism, namely unambiguity, where for every accepted word there is exactly one accepting run. We present a polynomial-time approach for PMC of Markov chains against specifications given by an unambiguous Büchi automaton (UBA). Its two key elements are the identification whether the induced probability is positive, and if so, the identification of a state set inducing probability 1. Additionally, we examine the new symbolic Muller acceptance described in the Hanoi Omega Automata Format, which we call Emerson-Lei acceptance. It is a positive Boolean formula over unconditional fairness constraints. We present a construction of small deterministic automata using Emerson-Lei acceptance. Deciding, whether an MDP has a positive maximal probability to satisfy an Emerson-Lei acceptance, is NP-complete. This fact has triggered a DPLL-based algorithm for deciding positiveness.
- Keywords (DE)
- Modellprüfung probabilistischer Systeme, Markovkette, Markoventscheidungsprozess, Büchiautomat, Linear-temporale Logik
- Keywords (EN)
- Probabilistic Model Checking, Markov Chain, Markov Decision Process, Büchi Automaton, Linear-Temporal Logic
- Classification (DDC)
- 004
- Classification (RVK)
- ST 136
- Examiner
- Univ.-Prof. Dr. Dr. h.c. Javier Esparza
- supervisor
- Prof. Dr. rer. nat. Christel Baier
- Awarding institution
- Technische Universität Dresden, Dresden
- Project sponsoring
- Deutsche Forschungsgemeinschaft
Nicht-Mehrdeutigkeit, Alternierung und Nichtstandardakzeptanz in automatenbasierter Modellprüfung probabilistischer SystemeID: BA 1679/12-1 - version
- publizierte Version / Verlagsversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-361005
- Qucosa date of publication
- 13.11.2019
- Document type
- doctoral_thesis
- Document language
- English
- licence