理论计算机科学电子笔记135（2006）3-18www.elsevier.com/locate/entcs基于接受前件的分布式LTL模型检测顶点排序L. Brim 1，I. Cern'a2，P. Moravec，J. 圣门沙捷克共和国布尔诺马萨里克大学信息学院摘要基于分布式自动机的LTL模型检查依赖于在Buuchiatom m atonn中查找接受循环的算法。在[9]中，基于最大接受前导的优先级排序是一种基于循环的优先级排序。 接受状态的排序（因此是最大值）是影响模型检查整体复杂性的主要因素之一，因为不完美的排序可以强制对自动机进行多次重新探索。本文讨论了在分布式环境中寻找最优排序的问题，证明了它的困难性，并给出了在分布式环境中寻找最优排序的几种算法。我们从理论上和实验上比较了这两种方法，以找出哪种方法效果更好。关键词：LTL-modedelchecking，Bu？chiaauto omata，optimalorderi n g1介绍在过去的十年中，已经开发了许多使用分布式和/或并行处理的技术来对抗验证问题的计算复杂性它们涵盖了可达性分析[3，14，17，21]，分支时间逻辑的验证[4，5，7，8，12，15]，线性时间逻辑[1，2，10]，等价性检查[6，18]以及其他验证问题。1 捷克共和国资助机构第201/03/05092捷克共和国科学院资助的研究，资助号：1ET 4080505031571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.0154L. Brim等人/理论计算机科学电子笔记135（2006）3本文主要研究文献[9]中提出的LTL模型检验的最大接受预处理器技术我们将展示如何扩展和优化这种技术，以加快在分布式环境中的LTL模型检查。最大接受前趋算法（MAP）是从自动机方法出发，将LTL模型检测问题归结为Buéchi自动机的最优解问题。 当且仅当在Buechi自动机G中存在可达接受圈时，Buechi自动机A A A t o m a t o n a cept是一个非空语言.可达性是一种可以有效地进行局部化的图形探索技术。MAP算法利用可达性在分布式环境中进行循环检测。该算法是来自观察，所有的顶点上的一个周期有相同的一组前辈。为了避免计算所有前驱的集合，该算法为每个顶点分配单个代表性前驱。该算法的另一个核心思想是利用顶点排序来确定合适的代表。也就是说，假设图的顶点是有序的，代表是顶点的最大接受前驱（或空值，如果没有）。一个图包含一个接受圈的充分不幸的是，这不是一个必要条件，因为可能存在一个接受循环，而MAP算法的总体复杂度主要来自计算代表和迭代次数，其中顶点被重新分类并重新计算代表。结果表明，顶点排序对提高算法的性能至关重要在文献[9]中，只考虑了几种基本的顶点排序，而对顶点排序及其对算法效率的影响的系统阐述却没有得到解决。在本文中，我们详细研究了顶点排序的影响首先，我们引入最优排序的概念，作为MAP算法在第一次迭代中终止的排序，即不对代表重新分类。最优排序可以例如通过图的深度优先搜索遍历然而，正如我们所证明的，这个问题本身是P-完全的，它的有效分布解并不在手边（第3节）。因此，我们制定了几个算法来解决分布式环境中的排序问题，并研究它们的理论性质（第4节）。所有的专家都经过了详细的L. Brim等人/理论计算机科学电子笔记135（2006）35实验评估（第5节）更深入地了解它们在分布式验证中的实际可用性。2最大可接受前置器在本节中，我们概括了[9]中提出的MAP算法的主要思想，集中讨论了顶点排序对算法复杂度的影响MAP算法遵循基于自动机的LTL模型检查方法[22]。将验证问题归结为布尔希自动机的空性问题，并将其表示为可积问题. 设A=（A，S，δ，s，Acc）是一 个Bu？hi自动机，其中A是一个输入αbet，S是一个有限状态集，δ：S×A→2S是一个转移关系，s是一个初始状态，Acc？S是一个接受状态集自动机A可以是用有向图GA=（V，E，s，A）标识，称为自动机图，其中V∈S是对应于所有可达状态的顶点集。自动机A，E ={（u，v）|u，v ∈V，v ∈ δ（u，a），对a ∈ N}，s ∈ V是A的初始状态对应的可区别初始顶点，A是A的可达接受状态对应的可区别接受顶点集.定义2.1设G=（V，E，s，A）是一个自动机图。可达关系~+v×V定义为u~+vi ≥有向路u0，u1，.，uk ∈ G，其中u0= u，uk= v且k > 0。有向路径u0，u1，.，ukn构成一个圈，如果u0= uk，并且该路径至少包含一条边。如果路径上至少有一个顶点u0，u1，.，ukn属于接受顶点A的集合。一个Buchiautomatonrecognises是一个非线性映射语言，它表示一个含有接受环的自动MAP算法通过最大接收前导来检测接收周期。 它假定向量集上的线性序。通过对所有v∈V设置零零值v，将该排序扩展到 设 置 V_n{null}（null∈/V）.定义2.2设G=（V，E，s，A）是一个自动机图。图G的最大接受前驱函数，映射G：V→（V{null}），是定义为.max {u∈A|u ~+v}如果{u∈A|u ~+v}mapG（v）=否则为空如果存在一个顶点v∈V，且映射G（v）=v，则算法报告一个接受循环。然而，可能发生的是，该图包含接受6L. Brim等人/理论计算机科学电子笔记135（2006）3循环，且对所有v∈V，不等式映射G（v）/=v成立。由于一个循环上的所有顶点必须有相同的最大接受前驱，这只能在此前驱位于循环之外这样的顶点可以从接受顶点的集合中移除，而不违反图中接受环的存在这个想法是形式化的概念删除转换。当删除变换被应用于具有映射G（v）/=v的自动机图G时，对于所有v∈V，它通过删除显然不位于任何圈上的顶点来定义2.3设G =（V，E，s，A）是一个自动机图，并将G映射到其最大接受前驱函数。定义删除变换为del（G）=（V，E，s，A），其中A = A\{u ∈ A|mapG（u）<$u}）。请注意，删除转换的应用程序可能会导致不同的map函数，但它保留了“图包含接受循环”的属性MAP算法交替地计算映射函数并应用删除变换，直到发现接受循环或接受状态集为空。A/=0时的MAP算法计算地图G;如果（n∈A：mapG（u）=u）然后返回CYCLEintn=nums（n）;fiodreturnNO CYCLE在我们的原始算法[9]中，删除变换已经使用集合{u∈A|V.mapG（v）= u}的接受顶点。这里使用的删除变换的新公式在优化顶点排序的上下文中更合适，因为它通常会删除更多的顶点。例如考虑图2上的具有两个接受顶点2和4以及由它们的编号给出的顶点排序的图该算法在原始定义下的两次迭代中终止（在第一次迭代中删除顶点4，在第二次迭代中删除顶点2），而在新定义下只需一次迭代即可终止（两个接受顶点都被删除，因为映射G（2）=null 2和映射G（4）=null4）。修改后的算法的正确性可以很容易地证明以下类似的参数[9]。L. Brim等人/理论计算机科学电子笔记135（2006）372134Fig. 1.删除转换3MAP算法的最优顶点排序分布式MAP算法的时间复杂度为O（a2·m），其中a为自动机图的接受顶点数，m为自动机图的边数.这里，因子a·m来自映射函数的计算，因子a与迭代次数有关，即，del函数的计算为了优化的复杂性，旨在通过选择适当的顶点排序减少迭代次数如何对顶点进行排序的一种自然方法是使用枚举顺序，因为它是在枚举式的on-the-mothery模型检查中计算的。 在[9]中，每个顶点都用一个由三个数字组成的向量来标识-工作站标识符，哈希表中的行号和行中的列号。顶点的排序由这些三元组的字典序给出在本节中，我们定义了最优排序的概念，并证明了最优排序问题是P-完全的。设k是MAP算法使用的顶点上的线性排序，并且iterk是直到MAP算法终止的主循环的迭代次数。定义3.1当矩阵元素= 1时，排序是最优的排序的最优性与接受顶点集上的可达关系密切相关。定义3.2一个序对所有u，v∈A都尊重可达性i，当-ever（u~+v<$v+u）则u<$v。引理3.3如果一个序矩阵考虑可达性，那么它是最优的。证据 我们证明了非最优排序不尊重可达性。假设图G的排序不是最优的，且存在一个接受圈。如果对于所有接受顶点u，值映射G（u）/=u，则该算法在第一次迭代中不会检测到接受循环。设v是圈上的最大接受顶点则v∈映射G（v），映射G（v）~+v，v+mapG（v）.因此，Google不尊重可达性。如果图中没有接受圈，则存在接受顶点8L. Brim等人/理论计算机科学电子笔记135（2006）3v，在MAP算法的第一次迭代之后不被重新分类为不接受这意味着v∈G（v）和G（v）~+v.从非周期性我们有V+mapG（v），这意味着它不考虑可达性。引理3.4对于每一个自动机图，都有一个最优排序。 而且，最优排序的时间复杂度为O（a·m）.证据我们给出了一个计算最优排序的算法。作为第一步，该算法计算可达性关系R ={（u，v）|u，v∈A，u~+v}.这个计算可以通过例如从所有接受顶点分别运行一个可达性过程来完成，这需要时间O（a·m）。现在，如果图不包含任何接受圈，则对于u，v∈A，我们将u∈v当且仅当（u，v）∈R。其他的顶点对是任意排序的。如果图包含一个接受圈，则存在一个顶点u，使得（u，u）∈R。令v∈u，对于每个接受顶点v，vi=u。其他的顶点对也是任意排序的。请注意，一个图可以有几个最优排序，因为相互不可达的非接受顶点和接受顶点的排序并不重要。问题是在分布式环境中是否可以更有效地计算最优排序我们提供了一个强有力的证据表明，最优排序的计算不能通过使用任何合理数量的并行处理器来显著加速也就是说，我们证明了最优排序问题是P-完全的，因此内在的顺序。一个问题是P-完全的，如果它属于P，并且每个语言L ∈ P都是这个问题的对数空间可约的（关于P-完全性的细节见[ 13 ]）。最优排序问题是对一个给定的自动机图和两个接受顶点u，v，决定在图顶点的每一个最优排序中u是否在v引理3.4表明，最优排序问题是在P. 从与非电路值问题出发，通过约化证明了P-硬度NAND布尔电路是序列B=（B0，.，Bn），其中B0=1anddBi=<$（Bi1<$Bi2），i1，i2i.Letvalue（B0）=truee，value（Bi）=（ value （ Bi1 ） =value （ Bi2 ） ） ， 并 且 value （ B ） =value （ Bn ） 。NANDCV问题是针对给定的NAND布尔电路B判定值（B）是否为真。Ladner [16]证明了NANDCV问题是P-完全的。定理3.5最优排序问题是P-困难的。证据通过将NANDCV问题在对数空间中约化为最优排序问题。令B =（B0，.，Bn）是NAND布尔电路。我们L. Brim等人/理论计算机科学电子笔记135（2006）39I0的t0F0FiTi2II1我我Fi2Gi2我不是Gi1Fi1Ti1II2构造一个自动机图G，并以这样的方式标识它的两个顶点u，v，使得在图顶点的每个最优排序中u先于v当且仅当value（B）=true。首先，对于每个Bi，我们归纳地构造一个图Gi图G0=（{T0，I0，F0}，{（T0，I0），（I0，F0），（F0，I0）}）在图2a）中描绘设Bi=<$（Bi1<$Bi2）. 如图2b）所示，Gi包含其子图Gi1和Gi2，新的向量Ti、Ii、Fi和新的边a) 图G0b）图Gi图二. 自动机图我们证明了对于所有i = 0，...，n，则图Gi具有特定的可达性。也就是说，如果value（Bi）=true，则Ti~+Ii~+Fi，Fi~+Ii，Ii/~+Ti，Fi+Ti，如果value（Bi）=false则Fi~+Ii~+Ti，Ti~+Ii，Ii+Fi和Ti+Fi.这个断言可以通过对i的归纳来证明。对于i= 0，value（B0）=true，断言可以很容易地按照图2a）检查。对于感应步骤，使用向上pose值（Bi）=true。值（Bi1）=值（Bi2）=假，并且通过归纳推理，存在从Ii1到Ti1和从Ii2到Ti2的路径。由边（Ti，Ii），（Ii，Ii1），（Ti1，Ii2）和（Ti2，Fi）组成的路构成了Gi中从Ti到Fi的路. 另一方面，由于在Gi1中没有从Ii1到Fi1的路径，也没有在Gi2中从Ii2到Fi2的路径，所以在Gi中没有从Ii和Fi到Ti的路径。情况值（Bi）=假根据值（Bi1）和值（Bi2）的值分为三个子情况，所有子情况都与前一情况类似地处理。为了完成最优排序问题的P-困难性的证明，让我们将NAND布尔电路B简化为自动机图G，该自动机图G包含作为其子图Gn的一个新的初始顶点S和从S到Gn中所有顶点的边。点Tn和Fn是可接受的。根据Gn的性质，我们有：10L. Brim等人/理论计算机科学电子笔记135（2006）342351如果value（B）=true则Tn~+Fn<$Fn+Tn，如果value（B）=false则Fn~+Tn<$Tn/~+Fn。我们主张在每个最优序Tn中value（B）=truei ∈Fn.显然，如果value（B）=true并且Fn在Tn之前，则map（Tn）=null，map（Fn）=Tn，并且MAP算法将需要两次迭代来完成循环检测。对于相反的含义，如果value（B）=false，则Fn在Tn之前的顺序是最优的，因为map（Fn）=null和map（Tn）=Fn。为了总结证明，我们观察到，图G的构造可以在相对于电路大小的空间对数中完成4顶点排序由于最优排序问题是P-完全的，我们不能期望在分布式环境中计算最优排序比在顺序设置中更有效因此，我们的目标是非最优排序。在本节中，我们将介绍几种计算顶点排序的算法除了一个之外，所有的都很容易在分布式环境中计算。对于所有的排序，我们指出如何我们阐述了一个定量的措施，表征的距离。定义4.1设k是一个序，γ = ku1，.，un= G中的一条路。n（u，i，. . ，uik）是序列（u1， . . . ，un）ifui1， . . ，uikareaceptinggveticesandduik 你. . . . 你好，我是2号，我是1号。 路径γ的逆序子序列的最大长度是路径γ的索引，索引（γ）。顶点u的索引被定义为索引（u）= max {索引（γ）|γ是一条路径从G中的初始顶点到顶点u}。一个自动机图G的指数定义为指数（G）= max {指数（u）|u是G中的一个顶点。为了说明这个定义，让γ= 104，2， 3， 5， 1是图3中所示的路径，12<$3<$4<$5是图3中所示的路径。 则（4， 2），（4， 3），（4， 3， 1）和（3， 1）是序列（4， 2， 3， 5， 1）的反向序列。另一方面序列（4，2，3，1）和（5，1）不是γ的逆序列。路径的指数γ是3。图三. 具有反向子序列的路径（4，3，1）定理4.2对图G和顶点序为n的图，itern= index n（G）。L. Brim等人/理论计算机科学电子笔记135（2006）311证据为了证明不等式指标<$（G）≤iter<$让我们假设有一个顶点u的指标<$（u）> iter<$。 令σ =（u1，. u，k）是从s到u的路径的反向子序列，|σ|= index（u）。那么在相同的删除变换期间，必须从A中删除至少两个顶点ui，uj（i j但是ui~+uj，uj<$ui，因此uj<$map（uj）。这与删除变换的定义相矛盾。对于相反的不等式指标<$（G）≥iter<$，设u是顶点， γ = μs，. u∈ G是一条路，使得下标k（γ）=下标k（u）=下标k（G）= k。令σ =（u1，u2，.uk）是最大长度的反向子序列，路径γ。通过对索引i的归纳，证明了MAP算法在第i次迭代时，顶点ui从接受顶点集中被移除.对于i= 1，这个断言是由γ的极大性得出的。对于归纳步骤，假设顶点ui−1在第（i−1）次迭代中被移除。如果ui在第i次迭代中没有从接受顶点集合中移除，则存在一个顶点vi∈A，且s~+vi~+ui和ui∈vi（即在第i次迭代中ui∈v映射（ui））.顶点vi在第i次迭代之前被重新分类为不可接受，我们可以对顶点vi重复类似的论点。 因此，我们有顶点ui<$vi<$vi−1<$.. v1，带s ~+v1~+. vi~+ui. 因此（v1，v2，. vi，ui，... uk）是反向子序列从s到u的路径的k+ 1个顶点。这违背了γ和σ。现在我们定义几个顶点排序，它们基于图遍历的不同方式。除第一项外，所有其他预期均适用于分派。定义4.3设G是一个自动机图。·DFS：假设图G被深度优先搜索（DFS）遍历。我们定义u∈DFSv i，顶点u比顶点v晚被DFS回溯（即，DFS是DFS后序的逆）。BFS：假设图G被广度优先搜索（BFS）遍历。我们定义u<$BFSvi <$BFS在顶点v之前访问顶点u。BFS：假设图G被BFS遍历。设GJ为广度优先搜索树。设visit（u）=（accpreds，BFSnr），其中acc preds是GJ中顶点u的接受前驱的数目，BFSnr是BFS访问顶点u我们定义u=BFSpredsvi =visit（u）在字典上小于visit（v）。图4中显示了CIBFSpreds和CIBFS之间的差异。在这两个图中，初始顶点的后继者都是从左到右进行为12L. Brim等人/理论计算机科学电子笔记135（2006）3一BCD左、侧边测量器BFS记录 = 2个计数器BFS = 1（sinceaBFSb，但bBFS prdsa），而对于高、中、高和侧边集，bB F S p rds= 1和n个DiterBFS =2（sincedBFSpredsc，但tcBFSd）。见图4。 BFSSpreads和BFSSpreads的比较对于下一个排序，假设图G被分成子图G1，G2，.，Gn.进一步假设G被一个改进的深度优先搜索（cDFS）遍历，它在遍历交叉边（顶点来自不同子图的边）时与DFS不同对于每个子图，cDFS维护一个顶点队列，从该队列开始局部DFS。局部DFS仅遍历相应的子图。当遇到交叉边时，其端点被排队到相应的队列中，并且搜索回溯。cDFS从初始顶点用本地DFS启动，并且当没有本地DFS正在运行并且所有队列为空时终止分布cDFS的计算的一种直接方法是将子图G1，G2，.，在不同的计算机上运行，并并行运行本地DFS。cDFS：假设图G被cDFS遍历。对于u∈Gi，v∈Gj，我们定义u∈cDFSvi ∈i j或（i=j且u回溯晚于v）。Lemma4. 4D FS是一个可选的排序，即， 索引DFS（G）=1。证据根据引理3.3，证明了BLDFS尊重可达关系。设u，v∈A，u~+v和v/~+u.如果DFS在v之前访问u，则u在其所有后继者之后被回溯，因此u是DFSv。如果u的访问晚于v，那么v一定是在到达u之前就已经被回溯了，因为没有从v到u的路径。因此，uDFSv.最优DFS的最优性对应于DFS问题的P-完全性[20]。引理4.5对于每个f ∈ {fBFS，fBFSpreds，fcDFS}，存在自动机图G，使得索引f（G）=|一|.证据图5 a）中描述了证明BFS和BFSSpreds上限的图（初始顶点的后继顶点从左到右遍历，0BFSa1BFS.一个m和一个0千分之一的BF扩散一个1千分之一的BF扩散...（m）和图5b）中的DFS（初始顶点的后继顶点自底向上遍历，dcDFS b）。L. Brim等人/理论计算机科学电子笔记135（2006）313a0a1amBC2 1a) BFS和BFSSpreds的上限b）BFS Spreds的上限图五. 上界5次实验我们已经实现了MAP算法的变体，使用前一节中描述的顶点这些实验是在一个由10个Intel Pentium 4 2.6 GHz工作站组成的网络上进行的，每个工作站具有1 GB RAM，每个工作站与100 Mbps快速以太网互连，并使用我们自己的分布式验证环境Divine提供的工具[11]。为了检查算法的性能，我们使用代表各种验证问题的图形进行了广泛的实验评估。这些图及其最重要的特征名称顶点Acc. 顶点误差电梯10 1891372307692没有LookUpProc8 219545691458848没有公共订阅12051215204612没有Rether 10 4113250035649118没有Rether 08 22898644850689是的PLCshedule600 150962873827319是的电梯4 1998570331596没有Phils14L 371931162410147没有TrainGate 8 21757237211668232是的彼得森3Err 11135804796734是的表1图表摘要14L. Brim等人/理论计算机科学电子笔记135（2006）3彼得森3Err 1246810公司简介时间81 127 527065Iter。11111公司简介时间 167 387 246 216 165Iter。11111联系我们 时间 116 213 114 9872Iter。11111Rether 08 2246810公司简介时间8670324031Iter。11111公司简介时间 465 285 146 158 93Iter。11111联系我们 时间 342 136 88131 95Iter。11111TrainGate 8 2246810公司简介时间8969452410Iter。11111公司简介时间 116 67342316Iter。11111联系我们 时间7765262014Iter。11111PLCshedule600 1 246810公司简介时间9 109 456213Iter。 11111公司简介时间7931418Iter。 11111联系我们时间33233Iter。 11111DVDFS时间– 820 588 450 242Iter。–1111表2实验结果：包含接受循环的可到达的接受顶点。错误列指示图形中是否存在接受循环。大多数图表无法存储在一台计算机上。我们比较了顶点排序，BFS，BFS，和BFS。此外，有几个自然的顶点排序来自用于存储状态的随机哈希函数（更多细节请参见[9我们使用[9]中最好的一个，表示为RND，作为与新提出的排序进行比较的所有实验的详细结果报告于表2和表3中。对于每一个图和每一个排序，我们在不同数量的工作站上进行了实验。对于每个设置，我们给出了算法执行的迭代次数和以秒为单位的运行时间。运行时间表示从几次运行中取得的平均值。符号在具有接受循环的图的情况下，所有计算仅执行一次迭代。换句话说，一个最优的排序是立即找到的L. Brim等人/理论计算机科学电子笔记135（2006）315电梯4 1246810公司简介时间 225 112 766760Iter。12108810公司简介时间 227 121 917360Iter。34443联系我们 时间 299 242 190 121 105Iter。44554Lup8 2246810公司简介时间714678266 245 196Iter。1212121212公司简介时间 1640 866547 508 365Iter。57989联系我们 时间427293185 167 129Iter。33333Phils14L 3246810公司简介时间 2718 1983 2220 3269 2709Iter。1111111111公司简介时间 3444 2606 4812 1935 2813Iter。44968联系我们 时间 3430 1735 2597 1427 1226Iter。33333Rether 10 42 4 6810公司简介时间––– 1130722Iter。–––2020公司简介时间––– 1390945Iter。–––1011联系我们 时间–––594406Iter。–––45电梯10 1246810公司简介时间 295 193 167 153 119Iter。1414141414公司简介时间 296 265 346 382 208Iter。578108联系我们 时间 159 130 119 117 90Iter。34444公共订阅1246810公司简介时间152 92676650Iter。88888公司简介时间159 97725652Iter。46666联系我们时间152 91676452Iter。33333DVDFS时间336 195 285 195 142Iter。78888表3实验结果：没有接受循环的虽然从理论的角度来看，这似乎很奇怪，但有一些实验证据证明这一点。迭代次数由商图高度限制。G=（V，E）的商图是一个图（W，H），使得W是G的强连通分支集，且（C1，C2）∈H当且仅当C1C2且存在r∈C1，s∈C2使得（r，s）∈E.的16L. Brim等人/理论计算机科学电子笔记135（2006）3商图的高度是商图中最长路径的长度如[19]中所述，模型检查图的商图高度通常较低，因此MAP算法往往只有几次迭代。在存在接受循环的情况下，迭代次数通常仅为1。此外，在某些情况下，您可以注意到，在较少的工作站上进行计算比在较多的工作站上进行计算花费的时间更少这些不规则性是由用于分区的哈希函数引起的，与算法的行为无关从实验中得出的另一个观察结果是，在某些情况下，完成计算所需的迭代次数在不同的排序下是完全不同的，但最终的时间非常接近。 这是由于在一次迭代中重新探索的次数是奇数。然而，较低的迭代次数通常导致更快的计算。在排序方面，尽管BFS和BFS Spreds都是基于BFS遍历的，但BFS Spreds在大多数实验中的性能优于BFS。事实上，我们的实验表明，在所比较的排序中，BBFSpreds排序是最好的一个。从理论的角度来看，可以认为是一个有前途的排序，因为它试图模仿最佳的CFDFS排序。然而，它未能很好地扩展。大量的迭代是由图的分布对顶点排序的直接影响和分布图中大量的交叉边引起的。由于这些原因，分销的积极影响受到抑制。随机排序的RND可以被归类为“更好的 它 有趣的是注意到，尽管它的随机性，它有时优于已被设计为采用特定图形特征的排序。最后，对于RMBFS、RMBFSpreds和RMBRND排序，该算法可以同时计算map函数和执行循环检测。实验清楚地表明，在存在接受循环的情况下，算法能够在第一次迭代中检测到它因此，没有必要生成整个图。对于不接受循环的图，工作站的数量通常对迭代次数的影响很小（除了排序的循环DFS）。6结论本文补充了基于最大可接受前辈概念的分布式LTL模型检测算法MAP首先，我们证明了对于每一个图，都存在图的顶点的最优排序，L. Brim等人/理论计算机科学电子笔记135（2006）317MAP算法在一次迭代中终止最优排序可以在时间上与图的大小成线性关系计算，但是问题本身是P-完全的，因此很难并行化。因此，我们提供并评估了几个算法计算顶点排序上的-的-的，所以他们很容易纳入分布式MAP算法。从理论和实验评估的结论是，没有一个化学家优于其他。平均而言，最可靠的启发式算法是基于广度优先搜索的BFSpreds，其次是基于（随机）哈希的BFRND所提出的方法的MAP算法的时间复杂度的优化，旨在减少算法的迭代次数另一个方向是在每次迭代中优化映射这种计算是基于图边的松弛（与Belmann-Ford算法中的方式相同），我们并不认为这太有希望。引用[1] 巴纳特湖Brim，and J. Chaloupka. 并行宽度优先搜索LTL模型检测。自动化软件工程（ASEIEEE Computer Society Press，2003.[2] J. 巴尔纳特湖 Brim，andJ. 是的。 D istr i d LTLMod el-Ch ecki ng inS PIN. 在SPIN软件模型检查研讨会（SPIN'01），LNCS的第2057卷，第200-216页中Springer，2001年。[3] G.贝尔曼时间自动机中的分布式可达性分析。Software Tools for Technology Transfer，7（1）：19[4] A. Bell 和 B. R. 哈 弗 科 特 Petri 网 规 范 的 顺 序 和 分 布 式 模 型 检 验 。 并 行 和 分 布 式 模 型 检 查（PDMCElsevier，2002年。[5] S. Ben-David，T. Heyman，O. Grumberg和A.舒斯特可扩展的分布式动态符号模型检测。在Formal Methods in Computer-Aided Design（FMCAD 2000）中，LNCS的第1954卷，第390-404页。斯普林格，2000年。[6] S. Blom和S.奥赞分布式状态空间最小化。在Formal Methods for Industrial Critical Systems（FMICSElsevier，2003年。[7] B. Bollig，M. Leucker和M.韦伯无交替μ-演算的并行模型检测。在Tools and Algorithms for theConstruction and Analysis of Systems（TACASSpringer，2001年。[8] B. Bollig，M. Leucker和M.韦伯无交替μ演算的局部并行模型检测。在SPIN软件模型检查研讨会（SPIN施普林格，2002年。[9] L. 布林岛 Cern'a，P. Moravec，and J. 是的。在分布式LTL模型检测中，一种新的预处理方法是基于块边的预处理。在计算机辅助设计的形式方法（FMCADSpringer，2004.[10] I. C和R都不存在。 Pel'an ek. D是Tib u tedExpl icitFairCycleDettion。在SPINWorkshoponModelChecking of Software（SPINSpringer，2003年。18L. Brim等人/理论计算机科学电子笔记135（2006）3[11] Divinehttp：//anna.fi.cz/divine。[12] H.加拉韦尔河马提斯库和我M. Smarandache。用于模型检测的并行状态空间构造。在SPINWorkshop on Model Checking of Software（SPINSpringer，2001年。[13] R. Greenlaw，H. Hoover和W.鲁佐并行计算的极限：P-完备性理论。牛津大学出版社，1995年。[14] B. R. Haverkort，A. Bell和H. C.博嫩坎普基于随机Petri网的超大型马尔可夫链的高效顺序和分布式生成。在Petri网和性能模型（PNPMIEEE Computer Society Press，1999.[15] T. Heyman，O. Grumberg和A.舒斯特可达性分析的一种工作效率分布式算法。计算机辅助验证（CAVSpringer，2003年。[16] R. E.拉德纳电路值问题是P.SIGACT News，7（1）：18[17] F. Lerda 和R.西斯托使 用SPIN 进行分布 式内存模型检 查。在SPIN Workshopon ModelChecking of Software（SPIN'99），LNCS的第1680卷，第22-39页中。Springer，1999年。[18] S.奥赞分布式验证和验证分布。博士论文，阿姆斯特丹自由大学，2004年。[19] R. Pel'an ek.典型的结构可在空间中创建一个过程。在SPINWorkshoponModelChecking ofSoftware（SPINSpringer，2004.[20] J. H.赖夫深度优先搜索本质上是顺序的. Information Processing Letters，20（5）：229[21] 联合Stern和D. L.迪尔将Mur验证器标记化。计算机辅助验证（CAVSpringer，1997年。[22] M. Y. Vardi和P. Wolper。自动程序验证的自动机理论方法。在逻辑计算机科学（LICSIEEEComputer Society Press，1986.
我的内容管理
展开
