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

基于自动机的概率模型检查中的明确性、交替性和非标准接受

• 批准号: 313089026
• 负责人: Professorin Dr. Christel Baier
• 金额: --
• 依托单位: Professur für Algebraische und logische Grundlagen der Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2016
• 资助国家: 德国
• 起止时间: 2015-12-31 至 2023-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/313089026?language=en
• 关键词: Unambiguity; alternation; non; standard; acceptance

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.

在该项目中，我们将重新审视由马尔可夫链建模的概率系统和马尔可夫决策过程针对某些时间逻辑中指定的定量规则属性的分析。在几种工具中实现的最突出的方法首先将公式转换为确定性拉宾。自动机将计算给定模型中公式的概率的任务减少到计算给定马尔可夫模型和自动机的乘积中可达条件的概率的任务。这种方法的时间复杂度是双倍的。从复杂性理论的角度来看，这对于马尔可夫决策过程来说是最优的，并且对于马尔可夫链来说，具有单指数时间复杂度的更有效的算法是已知的。其中一种方法依赖于无迭代自动机方法，而其他方法则通过使用（即，明确的强形式）Büchi 自动机来避免为时间逻辑公式分离的自动机的计算昂贵的确定。据我们所知，在该项目中，这些单指数时间方法尚不可用，我们将研究这些算法对马尔可夫链和参数变体的改进和扩展。更具体地说，我们将利用明确性和交替性来进行基于自动机的概率模型检查以及迭代。更详细地介绍无自动机方法。虽然概率模型检查社区之前的工作主要集中在分支时间逻辑或标准线性时序逻辑 (LTL) 上，但我们将使用过去的模态以及核心片段来研究 LTL。特别是，我们将设计新的算法，将带有或不带有过去模态的 LTL 公式和 PSL 公式转换为明确的自动机。此外，我们将研究确定性自动机。具有更灵活的非标准接受条件（而不是拉宾接受）及其用于马尔可夫链和马尔可夫决策过程分析的主要目标是利用非标准接受的灵活性增加之间的权衡。更小的自动机尺寸以及系统模型和自动机的乘积中所需图形分析的计算难度不断增加的条件。