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自动机。弱交替Büchi自动机的非标准幂集构造据我们所知，没有这些单一指数时间方法的实现。在该项目中，我们将研究马尔可夫链及其参数变体的这些算法的改进和扩展，并进行符号和非符号实现的比较研究。更具体地说，我们将利用明确性和交替自动机为基础的概率模型检查的目的，以及迭代自动机少的方法更detailed.While以前的工作的概率模型检查社区主要集中在分支时间逻辑或标准的线性时序逻辑（LTL），我们将研究LTL与过去的模态以及属性规范语言（PSL）的核心片段。特别是，我们将设计新的算法，翻译LTL公式和没有过去的模态和PSL公式到明确的automata.Further，我们将研究确定性自动机更灵活的非标准的接受条件（而不是拉宾接受）和它们的使用马尔可夫链和马尔可夫决策过程的分析。在这个方向上的主要目标是利用之间的权衡增加灵活性的非标准的验收条件，在较小的自动机的大小和所需的图形分析的产品的系统模型和自动机的计算难度增加。