On-the-fly Verification of Linear Temporal Logic中文翻译
需积分: 10 163 浏览量
2020-12-18
10:51:37
上传
评论
收藏 3.32MB DOCX 举报
线性时序逻辑的实时验证
摘要
本文提出了两种新的实用算法，用于解决线性时序逻辑的两个关键的动态模型检验问题:时
序逻辑公式的随需构造自动机;实时检查由程序的积(product)和属性产生的自动机是否为空。
1 介绍
自动检查有限状态程序是否满足其线性规范是一个在过去 15 年中引起了广泛关注的问题。
线性时序逻辑是一种强大的规范语言，用于表达安全性、活动性和公平性。然而，模型检
验问题是 PSPACE-complete。在实践中，模型检查方法面临与复杂性相关的限制:状态空间
程序的大小，表示公式的底层自动机的大小，以及应用模型检查算法的乘积自动机的大小
人们设计了许多技术来避免状态爆炸问题。通过使用二叉决策图，表示程序和公式自动机
可以检查非常大的并行系统[5]。另一种优化方法是动态验证，包括构造程序状态空间、属
性的否定和乘积自动机，同时检查乘积自动机是否为空。该方法的优点是算法能在完整的
程序状态空间和属性自动机建立之前给出答案。动态验证可以与[10]、[14]、[17]、[22]、
[23]方法结合使用，这些方法通过使用部分顺序语义执行缩减来避免对完整状态空间的探
索。这两种方法的成功案例清楚地证明了自动验证的有效性，即使对于相当大规模的工业
应用也是如此。
本文提出了新的实用算法，旨在解决线性时序逻辑的两个关键的动态模型检验问题:
——按需构造 时序逻辑公式的自动机;
——实时检查程序的乘积和属性产生的自动机是否为空。
这两个问题都已经被有效地解决了。[9]中的自动机构造算法似乎可以为时序逻辑公式生成
合理规模的自动机，并且它是动态运行的。[7]，[11]，[12]，[13]中的算法实时检查产品自
动机的空性。
我们的新自动机结构总是比在[9]中的好。它似乎能制造出更小的自动机。从实用的角度来
看，我们构建的是一个 B¨uchi 自动机的变体，即迁移 B¨uchi 自动机。与只有一组接受状态
[20]的简单 B¨uchi 自动机不同，transition B¨uchi 自动机有多组接受迁移。在[15]中已经证明，
具有迁移条件的 ω-自动机比具有节点条件的 ω 自动机简单。自动构造与[9]中提出的构造非
常相似。它也是基于 tableau 程序[25]，[26]。我们的方法的关键是使用符号计算，它允许
我们以一种自然的方式简化表达式，然后减少节点数量。此外，使用二元决策图[1]、[3]、
[4]可以高效、方便地实现。
新的检查算法是 Tarjan 算法的简单变体。
-算法设计为动态运行，即在遍历产品自动机的过程中，一旦遇到故障组件，就会检测到故
障。
-该算法直接工作于具有多个接受条件的迁移 B¨uchi 自动机，即不需要扩展迁移 B¨uchi 自
动机到一个简单的 B¨uchi 自动机。
-该算法可以用于检查公平性假设的时态性质的公式∧
i
GFpi，而没有不必要的开销。
以前存在的算法[7]、[11]、[13]没有任何上述有趣的特性。
本文的其余部分从定义有限状态程序、时序逻辑及其解释的一些预备知识开始。第 3 节介
绍迁移 B¨uchi 自动机和时序逻辑公式的自动机构造。第 4 节给出了模型检验算法。论文以
一些结束语结束。
2 预备知识
假 设 AP 是 一 组 原 子 命 题 。 我 们 写 2
AP
映 射 集 AP→{False,True} ， 2
2AP
映 射 集
剩余12页未读，继续阅读
评论0