交替树自动机的存储空性检验是通过符号可达性分析实现的

理论计算机科学电子笔记149（2006）33-49www.elsevier.com/locate/entcs基于符号可达性分析的交替树自动机的存储空性检验钱凯荣新南威尔士大学计算机科学工程学院澳大利亚悉尼摘要交替树自动机和AND/OR图提供了优雅的形式主义，使分支时间逻辑能够在线性时间内得到验证。Kupferman等人的开创性工作。[7]表明：1）分支时间模型检查可简化为表示模型和验证属性的两个交替自动机的乘积的语言非空性检查，以及2）非空性问题可以通过在表示该乘积的AND/OR图上执行搜索来解决。然而，他们的算法只能在显式状态模型检查器中实现，因为它需要堆栈来检测接受和拒绝运行。在本文中，我们提出了一个基于BDD的方法来检查的产品自动机的语言非空性。我们使用Schuppan和Biere [ 17 ]的一种称为“状态记录”的技术 这种技术使我们能够将乘积自动机转换为定义良好的AND/OR图。我们开发了一个基于BDD的可达性算法，以有效地确定是否存在AND/OR图的解图，从而解决了模型检查问题。虽然“状态记录”增加了状态空间的大小，我们的方法的优点在于节省内存的BDD可以oquerier和潜力，它开辟了优化的可达性分析。我们注意到，这种技术总是检测最短的反例。关键词：交替树自动机，语言空性检测，模型检测，与或图，可达性分析1 电子邮件地址：kairongq@cse.unsw.edu.au2电子邮件：anymeyer@cse.unsw.edu.au1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.07.02534K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 1491引言模型检查是一种自动验证技术，它可以穷举系统模型的所有状态[2，3，19]。该方法允许用户以完全自动化的方式检测财产违规，并从整体上验证在各种模型检测框架中，符号模型检测[9]和自动机理论[19]方法是突出的成功案例，并且已经基于这些方法构建了许多工具[1，6]。Vardi和Wolper [19]在线性时间时态逻辑（LTL）上使用了自动机理论方法。结合内存效率算法，该方法在流行的工具SPIN中实现[6]。最近，Kupferman等人[7]提出了一种用于分支时间时态逻辑的综合自动机理论在这篇论文中，还提出了一些分支时间时序逻辑，包括计算树逻辑（CTL）的内存效率模型检测算法。 从实现的角度来看，自动机理论算法可以很容易地纳入显式状态模型检查器，其中自动机的每个状态是represent- sented明确使用一块内存位。在符号模型检查中，一组状态可以用符号数据结构（如BDD）表示使用BDD的状态空间搜索通常计算给定状态集的所有后继者，称为图像因此，[7]中提出的算法不能直接使用BDD实现。我们在本文中的工作是设计一种方法，使用BDD验证分支时间逻辑在自动机理论框架。虽然分支时间模型检查可以通过使用时间逻辑公式的固定点特性有效地解决，但许多状态空间搜索优化技术仅适用于可达性分析[5，15，14]。近年来，将人工智能技术和模型检测相结合也做了很多工作。这项工作的大部分涉及启发式搜索算法，已被用来减少模型的状态空间的大小[20，4，13]。这些技术对于仅计算单个固定点的可达性分析最为有效对于一般的LTL或CTL模型检查，仍然不清楚如何应用这些技术。在最近的工作中，Schuppan和Biere [17]提出了一种称为“状态记录”的技术，将LTL模型检查转换为可达性分析。这样做，活性属性被转换为安全属性。原始模型中活性属性的满足性和转换后模型中的安全属性是等价的。我们的目标之一是推广这种技术，并提供一个框架，将分支时间模型检查转换为可达性分析。在下一节中，我们定义交替树自动机。第4节中K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 14935我们描述了自动机理论方法，特别是“状态记录”的概念。我们使用的AND/OR搜索图形式在第3节中简要介绍，以及搜索图的解图的定点计算我们基于BDD的自动机理论方法在第5节中解释。目前的实施仍处于初步阶段，但初步结果见第6节。最后，在第7节中，我们提出了我们的结论。我们工作的主要贡献是：• 使用交替树自动机和状态记录将分支时间模型检测问题简化为可达性分析。• 设计了一种基于BDD的AND/OR图搜索算法。• 通过处理任何类型的财产来概括Schuppan和Biere [17• 修改Kupferman et. [7]在一个象征性的环境中工作。2交替树自动机使用交替树自动机（ATA）的动机是它可以在分支时间逻辑的线性时间内构造。在这里，我们简要地描述形式概念。对于更全面的观点，读者应该参考[18，7]。一个有向图T=（VT，ET）是一棵树，如果每个节点x∈VT都有一条引入边，除了根x0没有引入边。设（x，y）∈ET为从x到y的有向边，称y为x的后继.一个节点x∈VT的度定义为x的后继节点的个数，记为d（x）。叶子节点是没有后继节点的节点。 树T的路π是一组节点π<$VT使得根x0∈π且对于每个节点x∈π，x要么是叶节点，要么存在唯一的节点y，其中（x，y）∈ET.请注意，我们允许无限树和无限路径。设是一个字母表，W：VT→是一个标签函数，它将树的每个节点映射到中的一个字母。对（T，W）称为一个带标号的树. 给定Kripke结构K=（S，R，s0），其中S是一组状态，R：S→S是一个转移关系，s0∈S是一个初始状态，我们可以从s0展开K，得到一个可能无限的（带标号的）树，其中所有的标号都来自S。这棵树被称为K的计算树。设A=（A，Q，δ，Q0，F）是一个自动机，其中A是一个字母表，Q是一个有限状态集，δ是一个转移关系，Q0<$Q是一个初始状态，F是接受条件.在一个词自动机中，给定一个状态q和输入字母σ，转移关系δ（q，σ）：Q×Σ→Q将对（q，σ）映射到一个集合{q0，q1，.，q k}Q。 自动机是确定性的，如果集合是单例，36K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 149否则是非确定性的（假设转换是完全的）。一个词自动机的运行对应于一个无限状态序列ρ = q0q1q2. ......这是什么？使得q0∈Q0和<$σ（qi+1∈δ（qi，σ））.在树自动机中，转换δ将每个状态和输入字母映射到集合{B0，B1，.，Bk}，其中Bi∈ P（Q）. 比如说，转换δ（q，σ）={{q0，q1，q2}，{q3，q4}}导致自动机的给定状态q同时且非确定地改变为两个集合之一。因此，与词自动机不同，树自动机的运行将生成一个（无限）计算树。一般来说，树的节点具有不同的分支度。如果任何节点的所有度都包含在一个集合D <$N中，那么我们称这个树为D-树。注意，如果D是一个单例，并且单例的元素是1，那么树自动机只是一个词自动机。2.0.1交替树自动机通过允许自动机状态转换的普遍和存在选择，推广了上面定义的非确定性树自动机[10，18]。再次考虑具有转移δ（q，σ）={{q0，q1，q2}，{q3，q4}}。如果我们把右边表示成布尔值-mula，例如，δ（q，σ）=q0<$q1<$q2<$q3<$q4，我们可以表示1）一个群内的迁移和2）群间的非确定性选择，相似性。实际上，这个布尔公式就是特征函数的两个集合。为了适应树的分支度，我们在变迁δ上增加一个额外的参数，并将上面的变迁重写为δ（q，σ，2）=（0，q0）<$（1，q1）<$（2，q2）<$（0，q3）<$（1，q4）。自动机理论模型检查允许使用一系列接受条件来表达不同的属性[19]。在本文中，我们将我们的研究限制在一个Bu？chiaceptancendition上。如果我们有一个无穷维自动机（Q，Q，δ，Q0，F），则F<$Q。如果我们有某个无穷次游程ρ，那么，因为Q是有限的，所以某个Qρ∈Q必然在ρ中无限次出现。A runρ是a（Bu¨chi）acceptruni <$Qρ$>F<$。因为我们一直在努力，一棵（计算）树，接受条件定义在运行中的路径上。ATA中的路径对应于字自动机中的运行。如果所有路径都是接受路径，则自动机的运行是接受运行。3符号与或图AND/OR图通常用于AI中对问题简化方案进行建模[11]。为了解决一个非平凡的问题，一个问题分解成许多（更小的）子问题。成功地解决子问题将根据分解条件产生原始问题的最终解K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 14937薄吴营德波西帕德公司简介我的天公共事业有一件外套p lay ten n是Fig. 1. 一个与或图表示打网球的问题图1显示了这种问题减少的一个简单示例。打网球必须具备两个条件：（1）好天气和（2）可用的场地。“好天气”这个问题被认为是一个原子子问题，这样我们就可以把它当作一个命题打网球的另一个条件是有一个可用的球场，在这种情况下，我们可能不得不在公共球场和私人球场之间做出选择。再次，公共法庭是原子的。私人法庭可以分解为预订和支付押金。这在本质上类似于自然演绎的过程。因此，我们可以说，为了解决形式上，AND/OR图是一个有向图G=（V，E），定义如下：• 一个指定的节点n0∈V称为根。• 存在一个函数，它将V中的每个节点映射到{，，T，}• 具有（n）=T或（n）=的节点被称为终端节点，并且除了它们自己之外没有到其他节点的出边。给定一个AND/OR图G=（V，E），一个解图Gs=（Vs，Es）是一个有向图，其中：• Vs<$V，Es<$E和n0∈Vs• 对于每个节点n∈Vs，如果n（n）=n，则n的只有一个后继在Vs中。• 对于每个节点n∈Vs，如果n（n）=n，则n的所有后继都在Vs中。• 所有的有限路径必须以一个T-节点结束，并且所有的无限路径必须有无限个T-节点作为子集。解图 Gs的高度H（ Gs）是T-节点前最长前缀的状态数。在图1中，AND/OR图具有两个解图，分别具有高度2和3，由虚线指示38K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 149和点划线多边形，它们对应于根节点所表示的问题的两个可能的解决方案。解图的存在性理想地捕获了模型中属性的可满足性。AND/OR图可以与启发式搜索算法相结合，以产生一种有效的机制来解决模型检查问题[16]。3.1求解图在AI [11，8]中已经研究了在AND/OR图中搜索解图的算法。一般来说，这些算法可以分为自上而下或自下而上。自顶向下算法从根构造部分解图，并使用自底向上传播来确认解图的存在性。自底向上算法从终端节点构造解图，并且可以通过检查根的可达性来确定解图的存在性。当然，这两种方法都是基于显式状态表示的。然而，我们的目标之一是确定一个解决方案图的AND/OR图表示的BDD。当转移关系由BDD表示时，通过计算给定节点的原像来计算其前驱节点是方便的。因此，我们的方法实际上是自下而上的，即它在单次运行中构造图并检查根的可达性设G=（S，s0，R，L）是一个导出AND/OR图的Kripke结构这里S是一组状态，s0是根，R<$S×S是一个转移关系，L<$S× {n，n，T，n}是一个标号函数。 我们要求L是全的，所以S中的所有状态都被标记。我们用S来表示具有标签的状态集。同样地，对于T，T和T。为了象征性地计算AND/OR图，我们需要计算G的所有可能解图的状态集SsolS ， 然 后 检 查 s0 是 否 ∈S sol 。 集 合 S sol 由 定 点 公 式 S sol= µZ 表 征 。（ST<$（EX（Z）<$S<$）<$（AX（Z）<$S<$））。定理3.1 S sol包含G诱导的所有解图的所有状态。证据证明遵循固定点的语义和解图的定义。固定点公式的右边从下往上计算任何可能解图的所有状态它很容易看出固定点的函数是单调的。计算开始于一组状态ST是真正的终端。组件（EX（Z）<$S）将所有的节点添加到Ssol中，并且（AX（Z）<$S）将所有的节点添加到Ssol中。 固定点的收敛保证了所有位置的所有节点，计算出可行解图Q我们的工作的一个特点是，模型检测问题被转化为K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 14939一个可达性问题。我们的方法也推广了[17]中的工作，可以处理任何类型的属性。由于上述公式表征了单个固定点，因此可以在计算中检查解的存在性：即，在计算的每次迭代中，我们检查是否s0∈Z在（EX（Z）<$S<$）和（AX（Z）<$S<$）之后两次。当然，检查状态意味着我们可以避免搜索整个状态空间，检测最小高度解决方案图。在实践中，如果这个最佳图是一个迹线，它通常对应于最短的反例，这当然是非常理想的诊断目的。4将自动机理论模型检测转换为可达性分析在这项工作中，我们使用自动机理论框架来验证CTL公式。 3模型检验问题涉及确定M，s0|其中M =（S，R，s0）是一个Kripke结构，而M是一个CTL性质。在[7]中提出的自动机理论框架中，这个问题被简化为语言空性检查问题。我们也使用这种方法，但需要将语言空性检查转换为AND/OR图可达性分析。设K=（S，R，s0，L，AP）是一个标号Kripke结构，其中S是一个状态集，R<$S×S是一个转移关系，s0∈S是一个初始状态（一般来说一个结构可以有一个初始状态集），L<$S×AP是一个标号函数.设（TK，WK）是K的计算树，其中WK用来自2AP的字母标记树的每个节点。设T是一个正范式的CTL公式，因此否定式被推到内部并放置在前面。德摩根定律的原子命题。为了方便起见，我们在公式的规范化过程中使用语义等价，以减少运算符的数量。给定一个公式φ，φ的闭包，记为cl（φ），由可以归纳定义的• ∈cl（• 如果<$1<$$>2∈cl（n）或<$1<$$>2∈cl（n），则<$1∈cl（n）和<$2∈cl（n）。• 若AX∈cl（n）或EX∈cl（n），则n∈cl（n）。• 若A（1U2）∈cl（），则1，2，1AX（A（1U2））∈cl（）。• 若E（1U2）∈cl（），则1，2，1EX（A（1U2））∈cl（）。• 若A（A1R2）∈cl（n），则n1，n2，n1<$AX（A（A1R2））∈cl（n）。• 若E（1R2）∈cl（），则1，2，1EX（A（1R2））∈cl（）。cl（n）中的公式构成交替自动机[3]我们的方法同样适用于其他分支时间逻辑，如CTL演算、无交替微演算和全微演算。40K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 149δp∈σ真Tp/∈σ假σ11AX{（0，），（1，），.，（k−1，n）} nEX{（0，），（1，），.， （k − 1，n）}nA（<$1U <$2）{δ<$（<$2，σ，k），δ<$（<$1<$AX（<$），σ，k）}<$E（1U2）{δ（2，σ，k），δ（1EX（），σ，k）}A（1R2）{δ（2，σ，k），δ（1AX（），σ，k）}CTL公式的一个表达式，初始状态为。按照惯例，我们将最外层的时态运算符表示为一个公式。例如，A（false R（E（true U（<$p）是一个R-公式，EXp是一个X-公式。cl（n）中的所有R-公式都是接受态.设A=（2AP，Q，q0，δ，L，F）是CTL公式的ATA.现在我们定义跃迁关系δθ。请注意，我们的构造与[7]中的构造不同，因为我们使用标签函数L来使用集合{，，T，}中的布尔连接符来标记ATA的每个状态。这使我们可以在转换的标签中省略连接词。我们还使用假设，如果p/∈σ，则<$p∈σ。转换关系δ及其对应的标记函数L定义如下：根据[7]，标记Kripke 结构K=（S，R，s0，L，AP ）和性质A=（2AP，Q，q0，δ，L，F）的乘积K×A被定义为一个单字母交替词自动机AK，=（{a}，S×Q，s0，q0，δ，L，S×F）。如果性质转移δ ∈（q，L（s），k）= θ和Kripke转移R（s）= t0，. ，tk，则对于每个c，自动化词的转移关系和标号函数为δ（εs，qε，a）= θ [（c，qJ）/εt c，qJε]，L（εs，qε）= Lε（q）.在定义了乘积自动机之后，我们现在引入状态记录机制。状态记录的思想是使用另一组状态变量来复制接受运行开始时的状态。 的存在可以通过检查当前状态是否已被记录来确定接受运行。 因为我们不知道一开始会是什么状态对于一个接受周期，我们使用一个三态自动机来猜测周期的开始。我们还使用一个2状态自动机来指示状态是否已被K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 14941记录。状态记录的本质是接受（拒绝）循环被简化，从而产生一个乘积自动机，它是一个定义良好的AND/OR图。这样，模型检验问题就转化为判定AND/OR图中解图的存在性问题。定理3.1的可达性算法可用于确定解图的存在性，从而解决模型检查问题。令Sr=S是一组状态，我们在必要时使用它来保存K两个小的Kripke结构K1和K2用于确定何时需要状态记录，如下所示：AK，K，K和Kχ在平移后的乘积是自动机A=（{a}，S，s0，s0，q0，T，0，R，L），其中S=S×Sr×Q×S×Sχ。转换关系R定义如下：• R（s，sr，q，sn，sx n，a）=Rn（sn） × s n，sr，q，sx n，如果sn=T，sx= 0并且q是接受状态（猜测循环的开始），或者• R（s，sr，q，L，0 r，a）= s，s，q，L，1 r（状态记录），或• R（s，s r，q，s n，s x n，a）= R（s）× s r n × δ（q，a）× R n（s n）× R x（s x）。相应的标签函数L定义为：• 如果q是接受状态，则L（s，sr，q，T，0）= k，或者• 如果q是接受状态，则L（s，s，q，L，1）= T，或者• L（s，s r，q，s n，s xn）= L n（q）.A中的状态标记遵循A中的状态标记K，k。引理4.1由A诱导的图GA是一个定义良好的AND/OR图。证据 从转移关系的定义可以直接得出，A是一个定义良好的AND/OR图。问题是，由于存在接受（和拒绝）运行，乘积AK，k将不能很好地定义当使用状态记录自动机Kχ和Kχ时，接受（拒绝）运行在本质被关注，从循环到有限的痕迹。A中接受循环的开始是一个T节点，另一个表示循环存在的副本是一个T节点。 因此，乘积A诱导一个定义良好的AND/ORK=（S，s0，R）ςKx=（Sx，s0，Rx）χS{T，L，R}{0， 1}s0不0RR（T）={L，R}，R（L）=L，R（R）=T Rx（0）= 1，Rx（1）= 142K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 149图二. 自动机理论方法graph.Q定理4.2GA有解图i ∈AK的语言，i ∈A非空，即K| = 0。证据 证明的关键是我们的状态记录自动机能够捕捉所有可能的接受（拒绝）周期。由于我们事先不知道哪个状态将处于周期的开始，因此我们在K中对每个接受（拒绝）状态使用非确定性转换R（T）={L，R}来猜测开始点。使用我们的构造规则，这个状态被标记为一个节点。这种考虑确保了每个可能的接受（拒绝）周期都将被捕获。因此，GA中解图的存在性证实了AK，k，因此K的语言的非空性。 |= 0。 Q5我们的方法从本质上讲，我们的方法，如图2所示，在自动机理论框架中使用基于BDD的算法来解决分支时间逻辑的语言非空问题该过程从模型开始，由Kripke结构表示，以及要验证的属性，表示为CTL公式。与传统的模型检测不同，我们还需要一个状态记录自动机作为输入。在第一步中，CTL公式被转换为（弱）交替树自动机。然后构造了三个输入的乘积自动机，并生成了一个AND/OR图以确定是否与或图有解图，我们使用特殊可达性分析算法如果这个算法找到了一个解图，这个性质就被验证了，而解图就是这个性质的证明。 否则，财产受到侵犯。为了确定反例，人们需要确定该属性的否定的智慧。 AND/OR中的可达性分析C o n s truc t p r o du c tau tom ato n将n个树更改为m到n（AT A）S o lu tio n g r ap h f on d，ie.P r o p e t y v针对AND/O R g ap的可恢复性分析我不知道你在说什么。p r o p er tyKr ip k e s tru ctur e of s y stem模型AN D/OR格拉普C T L福尔穆乌拉状态记录或记录在g au tomata（S R A）K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 14943经验证：A G EFp = A（falseR（E（tru eUp）图三. Kripke结构与CTL性质图使用BDD。我们将系统模型、属性自动机和状态记录自动机编码为BDD，将乘积自动机和与或图计算为BDD。5.0.1从ATA到使用BDD的AND/OR自动机理论分支时模型检验的关键是判定乘积交替自动机的语言非空性。Kupfer- man et. [7]将此问题简化为1个字母的自动机非空检查。虽然他们的算法使用AND/OR图作为底层数据结构，但1字母自动机的运行并不对应于AND/OR图如我们上面定义的。严重的问题涉及周期检测。当他们的算法第一次遇到接受（或拒绝）状态时，它可能会将状态标记为一个节点或一个节点。如果随后找到返回到接受（或拒绝）状态的循环，则相同的节点可以被标记为T或N。如果发生这种情况，则状态没有唯一标签。在显式状态模型检查器中，这个问题可以通过使用堆栈来存储接受周期来避免，如果周期确实存在，算法只需重新标记状态。这在基于BDD的模型检查器中不起作用，因为状态是隐式表示的，并且路径信息不能通过使用堆栈等结构来记录。5.0.2例如考虑图3中的Kripke结构和CTL属性。结构有4个状态，s3被唯一的原子命题p标记（假设p标记所有其他状态）。该性质在该模型中显然为真为了使用[7]中的算法来验证该性质，我们首先构造AG（EF p）的交替自动机如下：Qδ（q，{p}，k）δ（q，k，k）AG（EFp）k−1EFpc=0（c，AG（EFp））k−1EFpc=0（c，AG（EFp））EFP真k−1（c，EFp）c=0其中q是属性自动机的状态，状态AG（EF p）是s0S1pS3S244K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 149接受状态，另一个状态是拒绝状态。产品自动机的接受状态请注意，如果一个转换的值为true，这意味着通向该状态的路径在树自动机的运行中没有后继者。这对应于AND/OR图中的T节点。如果转换的值为false，则运行永远不会被接受，即 解图永远不会有一个节点。我们在这里省略了乘积自动机的形式化描述，而是在图4中描述了[7]中的算法用来检查语言的非空性的运行。图中的每个节点都是乘积自动机的一个状态。这个自动机的初始状态包含来自Kripke结构和属性自动机的初始状态。该算法从初始状态#1开始，该初始状态#1表明AG（EFp）在状态s0为真。这意味着EFp在s0处必须为真，这导致节点#2，并且AG（EFp）在s0的所有后继者（即s1）处必须为真，这导致节点#3。因此，节点#1是一个双节点。其他国家也以类似的方式扩大。转换为真导致节点#7，这是一个T节点。在这一点上，我们需要根据AND / OR图的解图的定义来反向传播标签。由于节点#4是一个T-节点，并且它的一个子节点是一个T-节点，因此节点#4也将被标记为T-节点。如果初始状态（#1）被标记为T节点，则语言是非空的。在这个例子中，有问题的状态是节点#6，因为它的一个后继节点循环回到一个曾经被扩张过的国家 在这种情况下，节点#1的标签将递归地依赖于其自身（因为节点#1、#3和#6的循环）。 当自动机运行接受或拒绝时，会发生此问题。事实上，很容易看出这里的循环是一个接受循环，因为#1是一个接受状态。为了避免这个问题，如果在标签的反向传播期间，节点的后继者导致接受循环，则我们认为该节点具有T节点作为后继者。因此，节点#6是T节点，因为节点#7是T节点，节点#1导致接受循环.或者，如果一个节点的后继导致一个拒绝循环，我们认为该节点有一个拒绝节点作为后继。很容易看出#1最终将被标记为T节点，并且乘积自动机的语言不是空的。在显式状态模型检查器中，上述非空算法通过维护两个堆栈来检测接受和拒绝循环。我们的目标是使用基于BDD的算法来检查语言的非空性，并使用BDD表示正在验证的模型和属性。通常，基于BDD的状态空间搜索不使用堆栈来记录哪些状态已经被访问，因此不能直接使用上述方法。相反，使用了状态记录。关键思想是使用另一组状态变量来记录可能存在于循环中的状态循环的存在K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 14945见图4。 自动机理论CTL模型检测可以通过检查原始状态变量的值是否等于记录的变量来确定因此，状态记录模拟堆栈，并且循环可以通过可达性算法来检测。我们使用这种方法来检测接受周期和拒绝周期。图5描述了使用这种技术的搜索图.在图4中，产品自动机的状态有两个组成部分，即Kripke结构的状态和属性自动机的状态。记录状态后，乘积自动机的状态有5个组成部分：即（s，t，n，save，saved），其中s是Kripke结构的状态，t是状态如 果 在 必 要 时 复 制 s ， 则 sender 仍 然 是 属 性 自 动 机 的 状 态 ， 而finallysave和saved是两个变量，用于确定何时记录状态以及该状态是否已经被记录。检测在接受周期中，在接受状态下记录状态是足够的。例如，在图5中，节点#1是接受状态，因此保存将非确定性地分成两个分支。保存的值在#2中变为L，在#3中变为R如果save=L，我们将在下一个转换中将s复制到t，并设置将该标记保存为1。请注意，非确定性分支将打开该状态是否是接受周期的开始的问题，因此该“split”节点的标签是“fixed”。虽然图4和图5中的图形相似，但后者包含更多的节点。特别地，阴影节点#11表明存在接受周期。11号节点是T型节点.通过应用状态记录，乘积自动机变成了一个AND/OR图，其中每个状态上的标签将只依赖于它自己的位置。使用我们的符号可达性算法，我们可以确定是否存在一个解决方案图，从而确定空的产品自动机的语言。46K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 149图五. 从自动机到定义良好的AND/OR图6执行我们已经在符号模型检查器NuSMV [1]中实现了这种方法。固定点公式的可达性算法已在单独的模块中实现，并使用NuSMV的弱前像和强前像例程用于时间算子EX和AX。我们采用的BDD为基础的模型检测，如输入变量排序和分区的过渡关系的功能。验证中的模型使用SMV输入语言表达。我们要求我们的算法的输入模型是一个翻译的自动机，诱导一个AND/OR图。这需要从原始模型和属性到新输入模型的源到源转换。为了产生下面的实验结果，我们需要手动进行翻译，但我们正在开发一种可以自动执行此操作的工具。我们实验的模型是一个gigamax缓存一致性协议。我们验证的属性是AG（EF p0.readable），它表明无论系统处于什么状态，都有一个未来状态，进程p0是可读的。该性质可以通过我们的基于自动机的方法和基于固定点特征的CTL模型检测算法来验证下表列出了一些初步结果。算法#BDD变量运行时间#BDD节点迭代我们的方法1881.3704257484标准880.2506594711由于我们需要使用一组变量来保存原始状态的副本，因此我们的方法使用的布尔变量数量是K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 14947标准算法。具体地说，我们使用另外88个变量来复制状态，12个变量来编码属性自动机和状态记录自动机。最终结果是运行时间更长，BDD节点（以及内存）更多。最后一列显示固定点计算的迭代次数。这是算法调用前图像（或图像）计算例程的次数的度量，这在符号模型检查中通常是昂贵的操作。在这个例子中，我们只调用了4个前图像操作，这大大低于标准算法调用的数量。7结论和今后的工作在这项工作中，我们已经在本质上转化为一个分支时间逻辑问题的可达性问题的AND/OR图，并把它放在一个符号设置。从我们的角度来看，这种转换的最大优点是，我们现在可以在可达性分析期间应用符号搜索算法来减少状态空间的大小。我们已经有了丰富的经验与启发式搜索[13，12]，并认为符号和启发式搜索技术的组合将带来更大的潜力。这项工作，连同工作的Kupferman等。[7]，强调了需要真正有效的（启发式）搜索算法来解决本质上是五分的AI问题表示，AND/OR图。在某种程度上，我们的方法会导致更差的性能，因为状态记录的额外负载。注意，这与Schup-pan和Biere在[ 17 ]中的结果是一致的 但从长远来看，在将分支时间模型检查转换为可达性分析之后，可以应用一系列优化技术来提高性能。虽然我们不探讨这些技术在本文中，我们将在不久的将来应用符号启发式搜索的可达性分析的分支时间属性。虽然我们专注于CTL模型检查，但本文中使用的方法适用于其他分支时间逻辑，如CTL逻辑和µ-Calculus。在我们的算法中，我们使用了一个新的概念。在事实上，由CTL构造的自动机满足在他们的自动机理论的方法，Kupferman等。al. [7]构建犹豫交替自动机（HAA）用于CTL演算和µ-演算。我们还应用HAA在我们的符号设置这些逻辑，并将报告这一点工作在稍后的日期。48K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 149引用[1] A. Cimatti，E.M.克拉克角，澳-地Giunchiglia和M.罗维里NuSMV：一个新的符号模型验证器。在Proc. of the 11th Int. Conf. on Computer Aided Verification，CAVSpringer-Verlag，1999.[2] E. M. Clarke，E. A. Emerson和A. P. Sistla.使用时态逻辑规范的有限状态并发系统的自动验证。ACM翻译计划。Lang.系统，8（2）：244[3] E. M. Clarke，O. Grumberg和D.A. Peled。模型检查。MIT Press，1999.[4] S. Edelkamp，A. Lluch-Lafuente和S. Leue用HSF- SPIN实现有向显式模型检验 在proc 模型检测软件，第八届国际 SPIN讲习班，加拿大多伦多，LNCS第2057卷，第57-79页。Springer-Verlag，2001.[5] 放大图片作者：Rana Fraer，Gila Kamhi，Barukh Ziv，Moshe Y.瓦迪和利莫·菲克斯优先遍历：验证和伪造的有效可达性分析。 在Proc. of 12th Int. Conf. on Computer Aided Verification，CAVSpringer-Verlag，2000.[6] 杰拉德·J·霍尔茨曼。 模型检查器SPIN。 软件工程，23（5）：279[7] 作者：J.瓦迪和皮埃尔·沃尔珀分支时间模型检测的自动机理论方法。J. ACM，47（2）：312[8] A. Mahanti和A.巴奇AND/OR图启发式搜索方法。Journal of the Association for ComputingMachinery，32（1）：28[9] K.L. 麦克米兰符号模型检查。Kluwer Academic Publishers，Boston，MA，1993.[10] David E. Muller和Paul E.不错无限树上的交替自动机。Theor. Comput. Sci. ，54：267[11] N. J·尼尔森 人工智能原理。 摩根·考夫曼出版公司，1980年[12] K. Qian和A.尼迈尔基于抽象的模型检查使用的是抽象细化。在proc 第二届国际Symp. 自动化技术验证和分析，ATVA'04，LNCS，第165-178页。Springer-Verlag，2004.[13] K. Qian和A.尼迈尔基于抽象和符号模式数据库的引导不变模型检验。 在proc 第十届国际Conf.关于系统构造和分析的工具和算法，TACAS '04，巴塞罗那，西班牙，LNCS的第2988卷，第497-511页。Springer-Verlag，2004.[14] K. Ravi和F.索门齐高密度可达性分析。在1995年IEEE/ACM计算机辅助设计国际会议论文集，ICCADIEEE计算机学会，1995年。[15] K. Ravi 和 F. 索 门 齐 加 速 符 号 遍 历 的 提 示 。 在 Proc. of Correct Hardware Design andVerification Methods，CHARMESpringer-Verlag，1999.[16] 安东内拉·桑托内启发式搜索+局部模型检查在选择μ演算。IEEE软件工程学报，29（6）：510[17] 维克多·舒潘和阿明·比尔。有限状态模型检验到可达性分析的有效简化。Int. Journal onSoftware Tools for Technology Transfer（STTT），5（2[18] 沃尔夫冈·托马斯。无限对象上的自动机。在理论计算机科学手册，B卷：形式模型和语义（B），第133麻省理工学院出版社，1990年。[19] 我的Vardi和P.沃尔珀自动程序验证的自动机理论方法在Symp的过程中。计算机科学中的逻辑，LICS'86，剑桥，马萨诸塞州，第332-344页。IEEE，1986年。K. Qian，中国山核桃A.Nymeyer/Electronic Notes in Theoretical Computer Science 14949[20] C. 韩阳和David L. 迪尔 状态空间的引导搜索验证。 第35届设计自动化会议论文集，DACACMPress，1998.