Unambiguity, alternation and non-standard acceptance in automata-based probabilistic model checking

点击翻译按钮获取中文摘要

In the project, we will revisit the quantitative analysis of probabilistic systems modeled by Markov chains and Markov decision processes against omega-regular properties specified in some temporal logic. The most prominent approach that has been realized in several tools first transforms the formula into a deterministic Rabin automaton and reduces the task to compute the probability for the formula in the given model to the task to compute the probability for a reachability condition in the product of the given Markovian model and the automaton. The time complexity of this approach is double exponential in the length of the formula and polynomial in the size of the system model. From a complexity-theoretic point of view, this is optimal for Markov decision processes. However, more efficient algorithms with single exponential time complexity for Markov chains are known. One of these methods relies on an iterative automata-less approach, while others avoid the computationally expensive determinization of automata for temporal logic formulas by using separated (i.e., a strong form of unambiguous) Büchi automata resp. a non-standard powerset construction for weak alternating Büchi automata. To the best of our knowledge, no implementations of these single exponential-time methods are available. Within the project, we will study refinements and extensions of these algorithms for Markov chains and parametric variants thereof, and carry out comparative studies with symbolic and non-symbolic implementations. More specifically, we will exploit unambiguity and alternation for automata-based probabilistic model-checking purposes as well as the iterative automata-less approach in more detail.While prior work of the probabilistic model-checking community has mainly concentrated on branching-time logics or standard linear temporal logic (LTL), we will study LTL with past modalities as well as a core fragment of the property specification language (PSL). In particular we will design new algorithms for translating LTL formulas with and without past modalities and PSL formulas into unambiguous automata.Furthermore, we will investigate deterministic automata with more flexible non-standard acceptance conditions (rather than Rabin acceptance) and their use for the analysis of Markov chains and Markov decision processes. The major goal in this direction is to exploit the trade-off between the increased flexibility of non-standard acceptance conditions in terms of smaller automata sizes and the increasing computational hardness of the required graph analysis in the product of the system model and the automaton.