分布式符号有界属性检查算法及实现在SymC验证工具中的应用

理论计算机科学电子笔记135（2006）47-63www.elsevier.com/locate/entcs分布式符号有界属性检查1普拉迪普湾Nalla，Roland J. Weiss，PrakashPeranandam，JürgenRuf，ThomasKropf，WolfgangRosensti elWilhelm-Schickard-InstitutfurInforrmatikUniversitüatTuübingenSand13，72076Tu？bingen，Germany摘要在本文中，我们描述了一种分布式的，基于BDD的有界属性检查算法及其在验证工具SymC中的实现。分布式算法验证更大的模型，并比顺序版本更快地返回结果核心算法在达到阈值大小后将状态集的分区分发到计算节点。节点异步地在节点上进行图像计算。 该方案的主要可扩展性问题是状态集分区的重叠。我们提出了静态和动态的重叠减少技术。关键词：验证，有界模型检查，属性检查，二元决策图，并行化。1引言虽然基于二元决策图（BDD）[7]和有界模型检查（BMC）[3]的状态空间的符号表示[ 8 ]极大地增加了验证工具可以处理的设计大小，但模型检查技术的研究仍然集中在更快地验证更大的模型。大型设计会在状态空间探索期间导致内存溢出，即可怕的状态空间爆炸。有1这项工作部分由德国研究理事会在GRASP和KOMFORT项目内提供资金，并由联邦医疗保险基金和教育中心在FEST项目1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.01848P.K. Nalla等人/理论计算机科学电子笔记135（2006）47提出了几种解决方案来处理BDD的巨大内存需求。一种建议是将BDD [30]划分为两个或更多个部分，并在进一步遍历期间单独处理它们。分区的遍历可以顺序[10]或并行[14]完成。在[28]中，提出了一种基于模型[12]和有界模型检查的组合，该组合在工具SymC中实现。检查算法遍历模型和属性的乘积自动机，直到它检测到属性的验证或违反，或者达到显式或隐式的时间界限只有边界集保存在内存中，即。不执行定点这种方法对于某些类别的模型和属性表现良好，但顺序版本也面临大型模型的内存耗尽，例如。一些ISCAS89的例子。这一事实促使并行化的证明算法，我们在这里提出。本文的结构如下。下一节讨论相关的工作和我们的贡献。第3节总结了符号有界属性检查，然后描述了分布式算法。然后，我们提出了我们的静态和动态的重叠减少的方法第6节给出了实验结果。最后，我们总结并提到未来的工作。2相关工作2.1分区在文献中存在许多分解表示为BDD的布尔函数的方法对于分布式验证[16，14]，分裂算法旨在创建平衡的分区。然而，在顺序验证方法中存在类似的方法[11，10]。这些算法的主要特点成本函数通常考虑所实现的余因子减少、余因子之间的共享量以及余因子的存储器平衡。此外，CUDD包[31]包含各种分解算法，产生平衡和不平衡分区.此外，分解技术允许用多个BDD表示相同的函数，但需要更少的内存[20，19]。必须针对这些技术更新图像计算算法更复杂的操作由BDD [30]的降低的峰值存储器要求来设置如[4]中所示，减少甚至可以是指数的。最后，密集下近似[26，25]试图减少BDD的内存需求，但仍然捕获了很大比例的状态空间。这些算法是次要的利益状态集分布，因为它们会导致不平衡的子集。P.K. Nalla等人/理论计算机科学电子笔记135（2006）4749没有一个建议的算法考虑后续的状态重叠。然而，对于具有显式状态图表示的模型检查器进行了类似的工作[21，5]。他们应用图形算法，尝试找到具有很少交叉转换的分区，以减少进程之间的通信延迟。在[15]中，作者在模型检查Petri网的上下文中研究了状态空间分布，也采用了显式表示。这些方法不能直接应用于符号表示。2.2分布式模型检验近年来，模型检测中的状态空间爆炸问题引起了人们对如何通过调整算法以适应分布式这包括显式[32，5，17，6]和符号[14，16，2，13，18]模型检查方法。海法的团队还致力于基于BDD的验证算法的并行化在核心，它们创建当前状态集的k个切片，并将这些切片分发到k个集群机器。他们使用[20]中的切片技术，但使用增强的成本函数来选择切片变量[16]。国家分为国有和非国有。在每个图像计算步骤之后，非拥有状态被分发到拥有节点。在[16]中，如果初始平衡丢失，则通过调整切片来实现负载平衡在[14]中，他们试图通过按需拆分和加入BDD来每一步后交换无主状态，使得它们的算法主要是同步的。在[14，16]中，可达性是用定点迭代来计算的，在[2]中，正则表达式用于指示非法行为，在[ 13 ]中检查了µ -演算公式。我们的方法检查PSL（属性规范语言）[1]或FTL（有限线性时间时序逻辑）[27]中指定的时间有界属性，无需定点迭代。2.3贡献用于并行化基于BDD的验证算法的同步方案降低了潜在的加速比，因为进程一直在等待其他进程完成。到目前为止，还没有成功的基于异步BDD的验证出租被提出。我们的方法的主要贡献是这样一个异步分布式算法。该算法只有在减少了交叉转换导致的共享状态以避免重复工作时才是可行的我们提出了静态和动态重叠减少算法。50P.K. Nalla等人/理论计算机科学电子笔记135（2006）47系统描述SYMC接受/拒绝性能财产描述机智/反例翻译成AR-自动机翻译成形式表示符号执行引擎Fig. 1. SymC操作概述。3顺序符号有界属性检查[28，22]中的形式验证算法结合了有界属性检查和符号遍历。时序逻辑公式被转换为称为接受-自动机（AR-自动机）的特殊有限状态机[27]。AR-自动机允许在有限序列上发现违反或验证属性，因此它们非常适合有界属性检查。检查算法操纵系统描述和表示为BDD的为了避免构造完全转移关系，构造了一组合取划分的转移关系，用于早期量化[9]。该算法已在工具SymC中实现，其一般操作如图所示1.一、顺序验证算法的迭代分两步进行。首先，计算AR自动机的后继状态，并检查其终止条件。如果不满足终止条件，则在第二步中在系统上执行图像计算在图像计算过程中，所有分区的合取都是建立在连续性上的，以获得后继状态集。像有界模型检查[3]一样，这种属性检查算法不会彻底遍历状态空间，而是检查给定时间范围内的所有可达状态该算法的核心优化技术是状态集分裂。每当达到表示当前状态集合的BDD的大小的阈值时，该集合被分成不相交的部分，并且算法以分而治之的方式继续对这些子集进行处理。顺序验证算法继续使用其中一个子集，并将其他子集堆叠起来。这可以递归地发生事务处理在当前子集上继续，直到达到时间界限或满足终止条件。终止通过发现有效性或违反属性来停止验证。否则，对所有堆叠的子集重复该过程。如果检查所有路径上的属性，则终止条件不同，即。普遍量化，或在一个路径，即。存在性量化非正式地，顺序终止条件定义如下：如果在当前状态集中检测到一个拒绝状态，P.K. Nalla等人/理论计算机科学电子笔记135（2006）4751如果当前状态集中的所有状态都是接受状态，则找到属性的验证否则，该财产仍处于如果在当前状态集中检测到一个接受状态，则发现属性的有效性。如果当前状态集中的所有状态都是拒绝状态，则发现属性的违规。否则，属性仍然挂起。4有界属性检查该分布式检测算法由初始的顺序检测阶段和后续的并行检测阶段组成首先，在所有k个计算节点上创建转换关系，并且在一个节点上顺序地进行状态空间遍历，分裂成k个子集已经并行执行，每个节点负责获得整个状态集的自己的不相交部分节点独立于这些子集开始状态空间遍历。终止条件保持不变，但是节点必须传递其本地结果，以便允许测试依赖于所有状态的终止条件。由于交叉转换，这种简单的方案无法在许多模型上提供显著的加速这些转换开始于当前子集的状态，但导致已经存在于其他状态子集之一中的状态我们称这种现象状态集重叠，或只是重叠。当然，冗余地执行用于重叠状态的图像计算。由于图像计算是形式验证工具的关键组件之一，因此该组件的冗余严重影响了整个验证过程的时间和内存需求。因此，优化分布式算法集中在减少重叠（见第5节）。4.1状态集分布将状态集拆分为k个部分以供后续并行遍历是代价高昂的操作。因此，我们已经并行执行了为简单起见，我们假设k= 2n，n∈N。基本上，一旦第一个节点将其状态集转储到磁盘，所有其他节点都会在通知后拾取转储的集合。然后，每个节点将集合分成两部分，并根据其等级，识别每一个节点，它丢弃一部分，并继续递归地在另一部分上分裂，直到只剩下它自己的子集该算法如图所示。二、52P.K. Nalla等人/理论计算机科学电子笔记135（2006）47SK//从状态集S中获取k个切片的子集igetSubset（in：S，k，i; out：Si）Si：= S对于j：= 1 .. log2（k）分裂（Si; g，h）//奇数位跳过h，偶数位跳过g如果i % 2 = 1则Si：= g else Si：=h i：= i / 2//获取下一位//将状态集S分割为两个切片g和hsplit（in：S; out：g，h）跳过GGS秩= gGS秩= gSHS秩= h跳过h跳过h图二.状态集分布算法。 左侧给出了分布算法，右侧显示了一个示例应用。4.2状态集重叠在所有节点选择了它们的状态子集之后，节点继续进行符号状态空间遍历。一个非常重要的观察结果是，经过几步遍历后，网络节点之间可能会出现状态重叠。定义1设S是一个用BDD表示的集合。则S的最大最小项的个数表示S中的状态数。定义2设S是一个非空集，S1，...，S k<$S，其中k≥ 2。 然后，我们将这些分区的状态重叠ok∈[0，1]定义为：k− 1ǁS ∩S ǁo=i=1j=i+1ij.（一）i=1因此，重叠是子集排列的成对交叉部分中的状态的归一化平均分母中的和的范围从1到k−1，因为这产生了具有i j的对Si，Sj的数量。ok= 0的重叠对应于不相交的分区，并且ok= 1的重叠对应于包含相同状态的分区。5重叠减少布尔函数表示符号遍历中的所有状态集和转移关系。如果要表示的集合很大，这种表示可以变大，直接对应于更多的内存需求。的布尔函数使用BDD表示和操作 理论要求|F|一个布尔函数f的节点数定义为它的节点数。为了减少内存需求，可以将布尔函数划分为更小的部分，其并集是整个集合。P.K. Nalla等人/理论计算机科学电子笔记135（2006）4753SvvS1S2n遍历步骤图像n（S1）图像n（S2）SvvS1S2n遍历步骤图像n（S 1）=图像 nSvvS1S2n遍历步骤图像n（S 1）图像n（S2）（a）Tv仅取决于v（b）Tv取决于ei （c）Tv取决于ei图三. n步后子集的可能重叠，依赖于分裂变量。定义3给定布尔函数f：Bn→B，f被划分为两个函数f1和f2，其中v是f的支撑集，f=f1<$f2，其中f1=v<$fv，f2=v<$fv<$。（二）分割变量v定义了f分割为f1和f2。这种拆分可以通过BDD操作轻松实现。BDD是一种压缩的决策树，其中连接了公共子树。这导致函数表示中节点的显著共享。因此，将函数f分割成两个函数f1和f2，其中v的选择不佳，可能不一定减少分割函数的存储器需求，并且可能导致|f1| ≈ |F2| ≈ |F|.在下面的论述中，我们确定了一个状态集，其特征函数表示为BDD。5.1静态重叠减少重叠起源于不同集合中的状态具有到相同的下一状态的转换为了最小化分裂的重叠，所选择的分裂变量v不应允许具有共同的下一状态的状态处于不同的分裂中。换句话说，v应该划分状态，使得它们没有共同的下一个状态。然而，在现实中，这样的划分是不可能的，但是可以在选择分裂变量v时进行一些调整以最小化重叠。为了找到一个好的分裂变量，我们静态分析的设计表示为有限状态机（FSM）。A FSM A是4元组A =（S，T，I），其中S ={s1，.，Sn}是由状态变量e1，. .. ，T m个分区，并且Im是初始状态的集合。选择一个好的分裂变量v的想法依赖于合取分割的转移关系T[9]。对于每个i∈ 1，.，m是54P.K. Nalla等人/理论计算机科学电子笔记135（2006）47我我转换关系对应于下一个状态变量J，则T=Mi=1 Ti.我们从状态变量集合E={e1，.，e m}。 图3（a）示出了没有重叠的最佳情况。这只有当v在所有进一步的情况下都坚持它的真值时，步骤，即划分Tv（Ti，其中 v=ei）仅取决于v。虽然这是理想的情况，但在实际设计中几乎没有这种情况这意味着v可能会在未来的步骤中改变其真值，因为它对转移关系的划分取决于更多的因素。最坏的情况下，几乎完全重叠可能会发生，如果Tv取决于输入变量析取只，如图3（b）所示。常见的情况介于这两个极端之间，发生在v依赖于输入与状态变量的其他组合时，如图3（c）所示。MinOverlap算法是利用划分的转移关系T的静态信息来找到好的分裂变量v。在预处理步骤中，每个状态变量都被分配一个单位，并且变量按其单位递减排序输入表将状态变量映射到它们的输入。随后，分裂变量选择算法利用该信息。定义5设l1，l2∈N是连续的lookaheads.对于给定的有限状态机A，状态变量e∈ E的单位元eΦl1，l2（e）∈[−1，1]，其中h|E|=m，定义为Φl1，l2（e）=|−| D ↓（e，l 2）|D↓ (e, l2)|.（三）M集合D↑（e，l1）包含所有在l1步中被e约束的状态变量，集合D↓（e，l2）包含所有在l2步中被e约束的状态变量这些集合从l1= 1和l2= 1开始迭代地确定每个Ti直接对应于下一个状态变量eJ的真值，因此我们通过遍历所有Ti和ei来计算这些集合。对于D↑（e，1），我们计算包含e的划分Ti，而对于D↓（e，1），我们计算支持Ti的状态变量。MinOverlap算法的基本假设是，在具有高分辨率的变量v上进行分割将导致结果分割之间的较少交叉转换，因为Φ11，12（v）n的值在v上的每个可变分割结束。当然，还有其他因素决定这些下一个值状态变量削弱了我们的假设我们的算法工作得很好，如果分区的转移关系Ti只依赖于合取连接的变量。 它降级，如果T i依赖于析取连接的变量，其中至少一个析取只包含输入变量。然而，分析每个T i的子句的所有布尔连接词在计算上是昂贵的。eP.K. Nalla等人/理论计算机科学电子笔记135（2006）4755实际的MinOverlap算法选择一个可行的状态变量进行分割。状态变量根据它们的重要性进行分类，并放入不同的集合中。我们从包含具有高重复性的变量的集合开始，并根据平衡条件检查它们。此外，我们使用[16]中的成本函数计算这些变量的成本，该成本函数由冗余和缩减因子组成。如果没有一个被检查的变量满足平衡条件，则选择具有最小成本的变量。图4给出了MinOverlap的伪代码。//S是当前状态集1//S1和 S2是生成的分区2//Φ是表3中的单位//δ是内存平衡因子4//α是成本函数5的权重split（in：S，Φ，δ，α; out：S1，S2）6bestCost：=Φ.top（）7minCost：= cost（S，bestCost，δ，α）8while C = getDataSet（Φ）C/=9对所有w∈C10如果max（|Sw|、|Sw'|）≤δ|S|当时11v：= w; goto do split12其他13thisCost：= cost（S，v，α）14如果thisCost minCost则15 0 then tillEnd：= false else tillEnd：= true7当迭代t8时0是属性的显式时间界限G[b]！（s1512.start s1512.video. 第1512.I1733条）（4）F[b] OutBuffer.s consume（5）6.1静态重叠减少在这一部分中，我们专注于将静态重叠减少算法MinOverlap与来自[16]的切片启发式的更改版本（标记为MinDist）以及来自CUDD包[31]的变量析取分解算法（标记为VarDisj）进行比较。MinOverlap算法是通过使用数据来记录统计变量而定义的。我在这里在实验中，我们使用了一个平衡条件max（|f1|、|F2|）≤2|F|为MinOverlap算法。 结果示于图六、3 http://kepler.sfb382-zdv.uni-tuebingen.de58P.K. Nalla等人/理论计算机科学电子笔记135（2006）47设计分裂alg.递归级别：拆分变量。步骤：ok·100StvtS1269Φ1，1一点三十二分一分三十一点五0.11214.13（0.55）#2Φ1，0一点三十二分一分三十一点五0.11217.5（0.51）37电子邮件1：0的比例1：58.60.36236.7（0.28）5000瓦尔迪斯一点十四分1：57.40.15371.2（0.25）S1512Φ5，1一分九十六秒5：64.8/ 10：89.30.153204.85（4.52）#2Φ1，01分10秒5：89.3/ 10：91.80.113330.31（4.4）57电子邮件1分10秒5：89.3/ 10：91.80.873324.89（3.72）10000瓦尔迪斯1分10秒5：89.3/ 10：91.80.383312.75（3.75）S1269Φ1，11：32/2：34/3：361：9.10.6869.9（0.55）#8Φ1，01：32/ 2：34/ 3：40，361：9.10.6869.43（0.52）37电子邮件1：0/ 2：42，6/ 3：12，8，401：12.70.5558.8（0.29）5000瓦尔迪斯1：14/ 2：12/ 3：10，26NA0.2658.4（0.27）S1512Φ5，11：96/ 2：98/ 3：100，1010：54.6/ 15：68.30.232891.7（4.6）#8Φ1，01：10/2：12/3：1410：76.4/ 15：94.20.152993.0（4.4）57电子邮件1：10/ 2：96，12/ 3：12，14，9410：76.6/ 15：94.21.52988.9（3.7）10000瓦尔迪斯1：10/ 2：12，94，96/ 3：12，96，1410：76.4/ 15：94.20.713029.2（3.7）NH2Φ1，11：14/ 2：48，16/ 3：10，18，5260：11.7 /100：25.40.65#481（7.12）#8Φ1，01：14/ 2：54，16/ 3：48，18，1060：12.2 /100：26.60.51第272名（7.0）118电子邮件1：4/ 2：58，176/ 3：24，134，54，4060：22.1 /100：40.813.4第151期（6.04）50000瓦尔迪斯1：4/ 2：58，40/ 3：44，54，18，17660：20.9 /100：41.013.3145号（6.07）图六、MinOverlap与其他算法的比较第一列列出了设计，其次是使用的处理器数量，状态变量的数量和分裂阈值。第二列指示拆分算法。第三列给出了每个拆分递归级别上所选拆分变量的索引。CUDD包通过索引识别变量。然后第四列显示不同迭代步骤的重叠。第五列和第六列分别列出了平均拆分时间st和总验证时间vt（或者用#表示存储器超过1000，后跟最大步数）。拆分时间对应于如图4所述的算法拆分所花费的时间。讨论：MinOverlap算法的预处理步骤不需要大量时间，在所有实验中，其消耗的验证时间不到1%。 对于两个处理器，设计s1269显示可以观察到，通过选择高效率的变量，重叠现象显著减少，从而总体核查时间有所增加。MinOverlap和MinDist都选择了较高的重叠变量，但只有MinOverlap显著减 少 了 重 叠 。 这 是 由 于 第 5.1 节 中 解 释 的 不 一 致 性 前 瞻 条 件 。 对 于MinOverlap，Influence保持正值，对于Φ1，1，Influence变为负值。对于八个处理器，设计s1269具有低重叠与所有分裂al-租女士。但是另外两个设计清楚地显示了应用MinOverlap的好处，无论是对于具有巨大重叠还是适度重叠的设计。设计s1512属于几步后有巨大重叠的P.K. Nalla等人/理论计算机科学电子笔记135（2006）4759类别。 然而，民-60P.K. Nalla等人/理论计算机科学电子笔记135（2006）47具有l1= 5的前视的重叠能够显著延迟重叠的发生并减少验证时间。然而，这表明，高重复变量只能帮助减少几个步骤的重叠，但不能避免它超过一个限制，使动态删除技术是必须的。的设计NH2中的重叠比其它设计中的重叠增加得慢得多，但其大小导致存储器超过100W。同样，MinOverlap能够减少重叠，即使在100步之后。这允许节点在没有内存的情况下比现在走得更远。6.2动态重叠缩减首先，我们在顺序SymC中运行了一些较大的设计，并打开了所有相关的优化。顺序算法在达到阈值时重复拆分状态集，而并行版本仅在状态集分布时进行拆分结果见图7。对于大多数设计，顺序算法不能完成遍历，由于内存溢出或超时问题4。设计阈值Φl1，l2时限的峰值节点数vtS486320000Φ1，154.48#2S151250000Φ2，11003.80*80人S1423第1页50000Φ1，0-13.55#11S1423第3页50000Φ1，01214.27*11NH250000Φ1，110002.30663图7.第一次会议。完全优化的顺序SymC的结果。第一列列出设计名称。第二列给出了分裂阈值。第三列显示用于MinOverlap分割的单位。第四列和第五列分别列出属性中指定的时间范围和最大峰值节点计数（以百万为单位最后一列显示了总体验证时间。#n或 *n 表示存储器超时或步骤n超时。图8示出了使用专用于检查算法的32个处理器和充当协调器的一个处理器的具有动态重叠去除在这些实验中，在整个验证过程中每p步重复应用动态重叠去除。讨论：首先，并行算法能够完成顺序方法由于空间或时间而无法处理的所有问题。时间限制。设计s4863和s1512清楚地显示了并行化和动态重叠消除的优势，即减小p减少了验证时间。此外，与顺序版本相比，设计nh2的遍历以2.8的加速比完成。4 实验在一小时后停止。P.K. Nalla等人/理论计算机科学电子笔记135（2006）4761设计p（Φl1，l2）时限的Seq.时间（步长）峰值节点数vtS4863200001（Φ1，1）51.67（1）8.39587.732（Φ2，1）51.69（1）10.52613.32S1512100002（Φ2，1）100108.75（33）2.41508.213（Φ3，1）100108.95（33）2.55522.255（Φ5，1）100106.53（33）2.83643.61S1423第1页500001（Φ1，1）-75.70（8）13.20748.52（Φ2，1）-75.54（8）13.77806.995（Φ5，1）-76.13（8）11.23567.41s1423p2500001（Φ1，1）-76.62（8）1.87114.25S1423第3页500001（Φ1，1）12152.04（9）14.511322.222（Φ2，1）12151.84（9）13.181171.183（Φ3，1）12153.18（9）7.68791NH250000100（Φ1，1）100086.22（132）1.658230.08见图8。具有动态重叠消除的分布式算法的结果。第一列表示设计和拆分阈值。第二列示出了执行重叠减少的时间段p和MinOverlap中使用的单位。第三列列出属性中指定的时间范围。第四列列出了顺序部分所用的时间和并行阶段开始的时间步长。第五列显示了所有节点的最大峰值节点数，单位为百万。最后一列列出了总体核查时间。对于设计s1423，我们考虑了三个性质p1，p2和p3。p1和p2都来自[2]和纯LTL性质，因此在该性质中没有指定时间界限。 与[2]相比，SymC在设计中发现错误的速度要快得多，即使考虑到不同的硬件配置。然而，设计s1423的表现出乎意料，因为验证时间随着较短的动态重叠减少周期而增加。这种效应是由表示状态集的BDD的行为引起的从集合中删除状态实际上增加了它们的BDD表示。这将打开一个新的线程，以了解何时以及如何应用动态删除。我们还调查，如果动态变量重新排序照顾这个问题。图9描绘了具有缩减周期2的电路s1512为了使图形清晰可见，仅显示了四个节点当节点0和24在执行期间交换它们的到达顺序时，可以很好地看到负载平衡效果。最后，测量结果表明，从磁盘读取和写入BDD不会显著因此，网络I/O62P.K. Nalla等人/理论计算机科学电子笔记135（2006）47不是分布式算法的瓶颈P.K. Nalla等人/理论计算机科学电子笔记135（2006）47633025201510501234567 8910还原时间点见图9。 节点在减少点的到达顺序，显示节点之间的负载平衡。7结论和今后的工作提出了一种基于BDD的有界性检验算法的并行化方法。两个主要贡献是一个新的分裂算法考虑到重叠减少和一个分布式的异步状态空间遍历算法与动态重叠减少导致自然的负载平衡。MinOverlap分裂启发式算法通过预处理转移关系并使用此信息对潜在分裂变量的列表进行排序来增强当前分解算法实验表明，该预处理步骤能够实际减少重叠和分裂时间。此外，MinOverlap几乎不会显著降低拆分运行时间或由此产生的重叠。动态重叠减少是一种重要的技术，可以验证更大的设计，并显著提高分布式算法的适用性。重新分配空闲节点避免了计算能力的浪费。然而，对于某些设计，重叠减少实际上可以增加具有较少状态的集合的BDD表示。这似乎与固定的BDD变量顺序在顺序阶段之后保持的特性有关我们在计算节点上使用不同的变量排序来处理这些情况。此外，我们正在扩展我们的实验，从VIS套件和最近的IBM的例子设计8确认我们要感谢审稿人的详细评论，这有助于提高本文的质量。引用[1] Accellera，http://www.eda.org/vfv网站。节点到达顺序节点0节点8节点16节点2464P.K. Nalla等人/理论计算机科学电子笔记135（2006）47[2] 本-大卫，S.，T. Heyman，O. Grumberg和A. Schuster，Scalable distributed on-the-the-spatialsymbolic model checking ， International Journal on Software Tools for Technology Transfer（STTT）4（4）（2003），pp. 496-504[3] Biere，A.，A. Cimatti，E.M. Clarke，O.Strichman和Y.Zhu，Bounded Model Checking，in：M. Zelkowitz，编辑，Highly Dependency Software，Advances in Computers58，AcademicPress，2003。[4] 博利格湾和I. Wegener，Partitioned BDD vs. other BDD models，in：ACM/IEEE InternationalWorkshop on Logic Synthesis（IWLS），1997.[5] Braberman，V.，A. Olivero和F. Schapachnik，Issues in Distributed Timed Model Checking：Building Zeus，International Journal on Software Tools for Technology Transfer（STTT）7（1）（2005），pp.四[6] 布林湖，I. Cern'a，P. Moravecand d J. Simsa，Distributedpartialordereductionoffstatespaces，in：Proceedings of PDMC 2004 [24].[7] 布赖恩特河E、Symbolic boolean manipulation with ordered binary-decision diagrams，ACMComputing Surveys24（3）（1992），pp. 293-318[8] Burch，J.，E. Clarke，K.L. McMillan，D.迪尔和L.Hwang，符号模型检验：1020State and Beyond，Information and Computing98（1992），pp. 142-170.[9] Burch，J.R.，E. M. Clarke和D. E. Long，Representing circuits more efficiently in symbolicmodel checking，第28届设计自动化会议（1991年），pp. 403-407.[10] Cabodi，G.，卡穆拉蒂湖Lavagno和S. Quer，Disjunctive Partitioning and Partial IterativeSquaring ： An Effective Approach for Symbolic Traversal of Large Circuits ， in ： 34thConference on Design Automation（1997），pp. 728-733。[11] Cabodi，G.，Camurati和S. Quer，大型有限状态机的改进可达性分析，在：ICCAD 1996会议记录[23]，pp. 354-360[12] Clarke，E.M.，O. Grumberg和D.E. Peled，[13] Grumberg，O.，T. Heyman和A. Schuster，分布式符号模型检验的μ-演算，在：G。贝里，H。Comon和A. Finkel，editors，Computer Aided Verification，13th International Conference，Lecture Notes in Computer Science2102（2001），pp. 350-362.[14] Grumberg，O.，T. Heyman和A. Schuster，一种有效的分布式算法用于可达性分析，在：W。A.小亨特和F. Somenzi，editors，Computer Aided Verification，15th International Conference，Lecture Notes in Computer Science2725（2003），pp. 54比66[15] Haverkort，B.，A. Bell和H. Bohnenkamp，从随机Petri网有效的顺序和分布式生成非常大的马尔可夫链，在：第八届国际Petri网和性能模型研讨会（1999年）。[16] Heyman，T.，D.盖斯特岛Grumberg和A.李国忠，大规模电路并行可达性分析中的可扩展性问题 。 A. Emerson 和 A. P. Sistla ， editors ， Computer Aided Verification ， 12th InternationalConference，Lecture Notes in Computer Science1855（2000），pp. 20-35[17] 英格斯角P.和H. Barringer，CTL* 共享内存架构上的模型检查，在：PDMC