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

在这个项目中，我们将回顾由马尔科夫链和马尔可夫决策过程建模的概率系统的定量分析，这些系统符合某些时态逻辑中指定的omega-正则性质。已在多种工具中实现的最重要的方法是首先将公式转换为确定的拉宾自动机，并将计算给定模型中公式的概率的任务简化为计算给定马尔可夫模型与自动机的乘积中的可达性条件的概率的任务。该方法的时间复杂度是公式长度的双指数和系统模型大小的多项式。从复杂性理论的观点来看，这对于马尔可夫决策过程来说是最优的。然而，对于马尔可夫链，已知具有单指数时间复杂性的更有效的算法。其中一个方法依赖于无迭代自动机的方法，而另一些方法则通过使用分离的(即，一种强形式的明确的)Büchi自动机来避免时态逻辑公式的自动机的计算代价高昂的确定。弱交替Büchi自动机的非标准Powerset构造。就我们所知，目前还没有这些单一指数时间方法的实现。在该项目中，我们将研究对马尔可夫链及其参数变体的这些算法的改进和扩展，并与符号和非符号实现进行比较研究。更具体地说，我们将利用基于自动机的无二义性和交替性以及更详细的迭代自动机无迭代自动机的方法。虽然概率模型检测社区的先前工作主要集中在分支时间逻辑或标准线性时态逻辑(LTL)上，但我们将研究具有过去的模态的LTL以及属性描述语言(PSL)的核心片段。特别是，我们将设计新的算法来将具有和不具有过去的模态的LTL公式和PSL公式转换为明确的自动机。此外，我们将研究具有更灵活的非标准接受条件(而不是Rabin接受)的确定自动机及其在马尔可夫链和马尔可夫决策过程分析中的应用。这个方向的主要目标是利用在较小自动机尺寸方面增加的非标准接受条件的灵活性与在系统模型和自动机的产品中所需的图形分析的日益增加的计算难度之间的权衡。

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.