从分布式内存周期检测到并行LTL模型检测

理论计算机科学电子札记133（2005）21-39www.elsevier.com/locate/entcs从分布式内存周期检测到并行LTL模型检测1J·巴纳特， L.布里姆， J. 沙洛普卡捷克共和国布尔诺马萨里克大学信息学院摘要在文献[2]中，我们提出了一个并行图算法，用于检测分布在工作站网络上的非常大的有向图中的圈。该算法采用由广度优先搜索计算的后台边缘。在本文中，我们描述了如何把该算法变成一个显式的状态分布式内存LTL模型检测器，通过扩展它与检测的接受周期，反例生成和部分订单减少。我们讨论这些扩展，并显示实验结果。关键词：LTL模型检测，广度优先搜索，分布式记忆1介绍模型检验[10]成为系统验证领域中最常用的形式化方法之一一般来说，模型检查问题询问被验证系统的抽象模型是否满足通过时序逻辑表示的期望属性[16]。不幸的是，所有已知的算法解决方案的模型检测问题的SUPERLER从大的空间需求需要回答的模型检测问题。这些要求是由以下事实引起的：模型的状态空间的大小随着系统中组件的数量呈指数增长最近出现了几种通过利用工作站网络的聚合内存来解决状态爆炸的尝试（参见例如，[18、14、12、5、6]）。1捷克共和国资助机构资助的研究，资助号：201/03/05091571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.05622J. Barnat等人/理论计算机科学电子笔记133（2005）21在本文中，我们考虑线性时态逻辑（LTL），一个主要的逻辑用于形式验证。它以基于自动机的非常有效的顺序算法和在几个验证工具中的成功实现而闻名。所有现有的显式状态分布式内存方法LTL模型检查（[4，7，1，15，9]）已知有各种缺点和不足，防止每个单独的算法被认为是明显的赢家。因此，分布式内存LTL模型检测的研究仍然是一个具有挑战性和开放性的课题。LTL模型检测问题的最优序贯解是基于状态空间的深度优先搜索（DFS）遍历，特别是DFS计算的后序对LTL模型检测的核心问题--循环检测至关重要。然而，当并行地探索状态空间时，由于所涉及的工作站的不同速度。因此，并行化基于DFS的LTL模型检查的那些算法支持在分布式存储器环境中维护DFS后序所必需的附加技术机器。在文献[2]中，我们提出了一种并行图算法，用于检测分布在工作站网络上的超大型有向图中的圈。主要的转折是，我们的新算法不使用DFS后序进行周期检测，因为它是基于广度优先搜索（BFS）。它利用了这样一个事实，即每个循环都有最远和最近的顶点，并且当穿过任何（非平凡）循环时，我们必须至少一次“返回”到更接近源的顶点。因此，图中的路形成圈的一个必要条件是它包含这样的后台边。后台边缘由BFS计算，BFS可以（不像DFS）合理地并行化。在本文中，我们描述了如何把图算法变成一个真正的显式状态分布内存LTL模型检查器，通过扩展它的检测接受循环，反例生成和部分订单减少。本文的其余部分组织如下。在下一节中，我们回顾了[2]中给出的图算法的主要思想。下面几节分别讨论接受循环检测、反例生成和偏序约简。在一个单独的部分中，我们总结了算法的实验评估。2并行检测周期文[2]中给出的算法是在工作站网络上实现的. 它的任务是判断一个分布图中是否存在环J. Barnat等人/理论计算机科学电子笔记133（2005）2123分布式图是这样一种图，其顶点被划分为与参与工作站一样多的不相交集合。特别地，引入parti- tion函数来为每个顶点分配顶点所属的工作站（工作站拥有顶点）。整个分布式计算由其中一个工作站启动和终止。这种特殊的工作站称为管理器。图应该是隐式给定的，即由初始顶点和一个函数，对于给定的顶点返回其直接后继。在算法的计算过程中，所有生成的图的顶点都存储在相应的工作站上。因此，每个工作站保持其自己的分布式图的一部分。如果探索应该继续到不属于工作站的顶点，则包含顶点的消息被发送到拥有它的工作站，并且跳过顶点的本地探索。顶点由目的地工作站进一步处理。在解释算法的思想之前，我们回顾一下后台边缘的定义。简而言之，后级边是图中不增加与初始顶点的距离的边。为了简单起见，我们假设给定图的所有顶点都是可达的。定义2.1设G =（V，E）是一个以s为初始顶点的图，u 是任意的顶点。顶点u的距离，用d（u）表示，是s和u之间的最短路径的长度。边（u，v）∈E称为后级边当且仅当d（u）≥d（v）。具有相同距离的所有顶点的集合被称为一个级别。用Level k表示距离为k的所有顶点的集合，即Level k={u∈V|d（u）=k}。很容易看出，对于图中的每个圈，都有一个最大的k，使得该圈包含一个来自第k层的顶点。此外，从Levelk中的顶点开始的循环上的任何边都必须是back-level边。由于循环中的所有顶点都有后继，因此很明显，图中的每个循环都至少包含一个后台边。循环检测算法的工作原理如下。该算法有两个过程交替执行。第一个过程的任务（以下称为主过程）是通过逐步逐层探索图来找到所有的后台边，而第二个过程的任务（以下称为嵌套过程）是测试每个发现的后台边是否是循环的一部分。主要过程被实现为图的水平同步广度优先搜索。一旦一个级别被完全探索，嵌套的过程被启动，用于从当前级别上的顶点发出的所有后台边缘（称为当前后台边缘），以检测循环。因此，为后台边缘启动的嵌套过程的目标是24J. Barnat等人/理论计算机科学电子笔记133（2005）21以击中后级边从其发出的顶点（称为目标）。如果至少有一个嵌套过程成功，则确保存在循环，并终止算法。否则，主要程序将继续探索下一个级别。每个嵌套过程都以深度优先的方式搜索其目标。由于有许多嵌套过程并发执行，每个嵌套过程的目标必须由过程本身传播。与标准DFS不同，顶点未标记为已访问，因此可以重新访问。请注意，嵌套过程的搜索空间可以被限制为已经被主过程访问过的顶点。显然，嵌套过程可能会多次重新访问某些顶点。为了防止这种情况，我们提出了几个优化，以减少重访因素公平。第一个想法是消除由同一嵌套过程进行的重复访问。为此，我们在每个顶点存储遍历该顶点的最后一个嵌套过程的标识（目标）。如果一个嵌套过程访问一个它以前访问过的顶点，则不允许它通过该顶点，除非该顶点同时被另一个嵌套过程访问。为了说明优化，让我们考虑图1中的图a）。可以容易地看出，在没有优化的情况下，针对后级边缘（A，B）发起的嵌套过程将访问顶点G四次（沿着从B到G的所有路径），但是如果考虑优化，则仅访问两次（从E和F）。我们建议的另一个优化减少了由不同嵌套过程进行的顶点重新访问。为了做到这一点，我们引入了一个排序的嵌套过程诱导其目标的顺序在每个顶点上，我们存储通过它的最高嵌套过程的标识符。只有具有更高标识符的过程才允许通过顶点。这种技术大大减少了顶点的重新访问。不幸的是，它破坏了循环检测功能，因为可能显示循环的嵌套过程可能在到达其目标之前停止。图1中的图表b）说明了这种情况。让我们假设一个排序，其中A > F。如果嵌套过程[A]（对应于后级边缘（A，C）并且将A作为其目标的嵌套过程）在嵌套过程[F]之前到达顶点C，则嵌套过程[F]在顶点C处停止。然而，嵌套过程[A]继续通过顶点E，F，B到顶点C，在那里它结束而不显示循环。为了解决这个问题，我们将每个嵌套过程的标识更改为一对[T，n]，其中T是目标顶点，n是过程已通过的当前后台边缘的数量因此，随着程序的继续，识别被动态地修改。我们还需要重新定义J. Barnat等人/理论计算机科学电子笔记133（2005）2125，，、，J，J，JJJ得双曲余切值.、、、，，、，J，J，JJ，JJ、、、、得双曲余切值.z，J，C，`，\Ea）、J、B、`、\、b）你，，，，、、、Jz，J，B，`，\，J，C，`，\，，J，D，`，\、、、、、、J， J，J，E，`，\，s、、、，Jz，F，`，\、、、、、J，A，A`，J，J，J.G，`，\J，J，J.H，`，\，J，A.A.，`，\，J，F，`，\c）、，J，C，`，\，，J，B，`，\你，，，J，J，C.D.，`，\d），J，CIB，`，\J，A，A`，\，sJ、、、、、J，`，，`z，，\，s，zJ，J，J.G，`，\，J，A.A.，`，\，J，F，`，\Fig. 1. 重新访问减少和接受周期检测嵌套过程的顺序。如果A B或A=B，则标识为[A，x]的嵌套过程小于标识为[B，y]的嵌套过程，并且x y. 现在，一个循环可以通过一个嵌套的过程来检测，它的目标，或通过一个嵌套过程，其通过的当前后台边缘的数量注意，后一种情况仅在存在作为循环的一部分的后级边缘时才是可能的。为了解释这种情况，让我们再次考虑图1中的图b）和A > F的排序。当前级别上有两个后台边缘，因此有两个嵌套过程启动，即[A，0]和[F，0]。当它们到达顶点C时，它们都通过了一个当前的后台边缘。如果后级边（A，C）的嵌套过程[A，1]在后级边（F，B）的过程[F，1]之前到达顶点C，则后一个过程停止。在这种情况下，用于后级边缘（A，C）的过程在图的探索中继续。当它第二次访问顶点C时，它的标识是[A，2]，明显大于[A，1]，因此该过程不会停止，并再次通过顶点C继续它、26J. Barnat等人/理论计算机科学电子笔记133（2005）21经过顶点E和F，并在到达顶点B时增加其经过的当前后台边的数量。 在该时刻，通过用于后级边缘（A，C）的过程的通过的当前后级边缘的数量超过当前后级边缘的总数（其为2），检测到循环的存在并且算法终止。我们现在把注意力集中在模型检测问题上，并展示如何将分布式内存周期检测算法扩展为显式状态分布式内存LTL模型检测器，通过检测接受周期，生成反例，我们展示如何将其与偏序约简相结合。3验收周期LTL模型检测问题可以归结为Bu？hi自动机的语言空问题[19]。 该系统由一个系统自动机来描述，其中一些状态被标记为接受，并且验证的LTL公式（的否定）被转换为属性自动机。这两个自动机结合在一起，形成一个同步的产品自动机，测试语言的空虚。如果自动机的语言是空的，那么系统的模型满足被验证的属性。在另一种情况下，产品自动机的接受运行（所谓的反例）给出了模型的一个behaior，它破坏了propery。一个布希自动机接受一个空语言当且仅当在相应的图中没有可达的接受圈。至于术语，我们切换到一个更方便的一个，并在适当的时候谈论状态而不是顶点和过渡而不是边。除非在特殊情况下，否则我们不能直接用文献[2]中的算法来检测布希自动机的空圈数，因为算法不能区分接受圈和非接受圈。然而，我们可以利用已验证的性质将所检查的图分解成若干个分量（每个分量是图的强连通分量的集合一般来说，这些成分可以是三种类型之一[11]：不接受，完全接受和部分接受。非接受组件不包含接受状态，完全接受组件仅包含接受状态，部分接受组件包含两者。显然，对于模型检验，接受循环检测根本不需要在图的非接受组件中进行，并且可以由图的完全接受组件中的简单循环检测代替。由于组件的类型完全由已验证的属性确定，J. Barnat等人/理论计算机科学电子笔记133（2005）2127能够预先容易地计算乘积自动机的分解。在[2]中，我们对那些仅由非接受或完全接受组件组成在部分接受组件中检测接受循环的基本思想是防止算法检测到非接受循环。为此，每个嵌套过程都维护一个附加的（接受）位，以指示它自上次进入接受状态以来已经通过了接受状态。穿过当前的后级边缘。特别地，每当过程达到接受状态时，该接受位被设置为真，并且每当过程通过当前后级边缘时，该接受位被设置为假。该位最初设置为假。该算法有两种检测循环的方法：通过命中过程的目标或通过超过当前后台边缘的数量 为了防止嵌套过程在非接受周期上超过当前后台边缘的数量，我们修改嵌套过程，以便仅在接受位设置为真时才对当前后台边缘进行计数。关于第一种方式（命中目标），我们修改嵌套过程，仅当它到达目标状态并且位设置为true时才报告图2中给出了过程S-FOR-ACCEPTING-CYCLE的伪代码。我们在图b）和d）上证明了该过程的行为，图1.用于后级边缘（A，C）的嵌套过程作为过程[A，0]到达状态C，因为A不是接受状态，并且接受位最初被设置为假，这意味着当过程通过边缘（A，C）时，过程不增加其通过的后级边缘的计数器。类似地，用于后台边缘（F，B）的嵌套过程作为过程[F，0]到达状态B。让我们首先假设过程[F，0]在过程[A，0]之前到达状态C，或者A F。在这种情况下，过程[F，0]继续通过状态C和E并命中其目标（状态F）。在图d）中，过程到达其目标，接受位被设置为真，而在图b）中，过程到达其目标，接受位被设置为假。显然，这可以区分接受和不接受的周期。现在让我们假设A > F并且过程[A，0]在过程[F，0]之前到达状态C。在这种情况下，过程[F，0]在到达状态C时停止，而过程[A，0]继续搜索。在图b）的情况下，过程[A，0]传递当前后级边缘（F，B）而不增加其传递的当前后级边缘的计数器，因为其接受位保持设置为假。这意味着该过程不会改变其标识，因此当它第二次到达状态C在图d）的情况下，[A，0]过程设置其28J. Barnat等人/理论计算机科学电子笔记133（2005）21接受循环的处理器（nmbrbl）while（<$$>（）<$BBLQ/=<$）doif（BBLQ/=<$）then（q，prelevel，target，bl，bit）：=dequeue（BBLQ）;如果d（q）<水平如果（IsAccepting（q））然后是：=truefi如果（q=目标位=真）然后ACEPTING-C-DECTED（）fiif（prelevel=Level−1）那么bl：=bl+1位：=假如果（bl > nmbrbl）然后ACEPTING-C-DECTED（）fifiif（（Level−1> q.level）（Level−1 =q.level（target > q.target）（target=q.targetbl > q.bl）（target=q.target）bit> q.bit）然后q.target：=targetq.bl：=blq.level：=Level−1q.位：=位foreacht∈Successors（q）doif（Owner（t）/=WorkstationId）然后发送消息给所有者（t）：入队（BBLQ，（t，d（q），target，bl，bit））elsepush（BBLQ，（t，d（q），target，bl，bit））菲奥德fififi奥德J. Barnat等人/理论计算机科学电子笔记133（2005）2129恩德图二. 改进的过程C检查-BL-边缘与接受循环检测30J. Barnat等人/理论计算机科学电子笔记133（2005）21当它通过接受状态E时，接受位为真，这允许该过程在它通过后级边缘（F，B）时增加其通过后级边缘的计数器注意，当计数器增加时，接受位被重置为假。然后，该过程第二次到达状态C，被标识为[A，1]。这意味着程序不会停止，而是继续搜索。在状态E，它将其接受位设置为真然后，将其转换为[A，2]。然后它第三次通过状态C。 在状态E，它再次将接受位设置为真，并且在通过后级边缘（F，B）之后，它超过当前后级边缘的数量。因此，接收周期的存在被正确地检测。请注意，如果将算法修改为仅检测接受周期，则可能会发生完全高于当前水平的非接受周期。参见图1中曲线c）中的循环B、D、B。然而，这些非接受周期根本不影响周期检测，因为它们既没有接受状态，也没有电流后级边沿。最后，请注意，可能存在无法通过第一种循环检测方法（即通过击中目标）检测到的接受循环。让我们考虑图1中的图c）和G > A的排序。嵌套过程[A，0]在状态G停止，因为[A，0][G，0]。<嵌套过程[G，0]在状态E将其接受位设置为真，因此当通过后台边缘（A，C）时将其自身变为[G，1]。因此，每当它到达其目标时，其接受位被设置为假。因此，在这种情况下，通过超过当前后级边沿的数量，将在状态C处由过程[G，3]检测到周期。定理3.1当且仅当产品自动机图中存在接受循环时，接受循环检测算法总是终止并报告接受循环的存在。该证明利用了[2]中提出的分布式后台边缘检测算法的正确性。此外，还必须考虑到几个事实。如果在图中存在接受循环，则至少一个（最浅）循环被嵌套过程完全探索，因为在处理图的下一级之前清空所有队列BBLQ另一个重要的事实是，没有嵌套过程可以无限多次地通过非接受循环。更详细的证明见论文全文[3]。J. Barnat等人/理论计算机科学电子笔记133（2005）21314反例生成模型检查算法应该能够在被验证的属性被违反的情况下为用户提供一般来说，计算的反例可以是相当长的，这可能使其难以定位错误。因此，计算最短的反例极大地方便了调试过程。在本节中，我们将介绍一种生成简短反例的技术一个反例由两部分组成：一个接受循环和一条从初始状态s到达它的路径。在顺序嵌套DFS算法中，反例的生成是简单地遵循DFS搜索栈：嵌套搜索的DFS栈用于重构接受循环，而主搜索的DFS栈给出了一条通向接受循环的路径，但在我们的算法中，我们没有任何DFS搜索栈，因此必须考虑不同的方法。回想一下，我们的算法使用了类似于嵌套DFS的两个搜索过程。与嵌套DFS不同，主要搜索是广度优先搜索。这两个搜索过程都建立了用于实例生成的父图更准确地说，对于每个顶点v，在主搜索期间存储值par（v），其是搜索中顶点v的父（称为BFS父）。请注意，在整个计算过程中，它只被分配一次。此外，我们还存储值par-dfs（v），它是嵌套搜索中顶点v的父节点（称为DFS父节点）。每次允许嵌套过程通过顶点时，都会分配该值。在这两种情况下，父节点都以下列方式引入边。如果v是一个顶点，par（v）是v的BFS父图，则（v，par（v））是BFS父图中的诱导边，类似地，DFS父图定义了DFS父图。下面我们将展示如何通过遍历BFS和DFS父图来找到反例。反例的接受循环部分是使用DFS父代生成的。一旦检测到图中存在接受循环，人们可能会试图跟随DFS父循环回到并通过该循环。然而，由于可以并行运行多个嵌套过程，因此每次更改其DFS父节点时， 因此，DFS父图可能不包含循环，即使输入图包含循环。一种可能的情况如图3所示。假设第一个嵌套过程从顶点F开始，DFS父图随着过程的继续而构建（见图3.a）。假设程序经过顶点C后进行第二次嵌套搜索32J. Barnat等人/理论计算机科学电子笔记133（2005）21、、J你，，，，J，，JJ，，J你，，，，JJ，，CTJa），J，B，`，\b），J，B，`，\，，J，J，C，`，\，J，A.A.，`，\，J，F，`，\，J，A.A.，`，\R，J，F，`，\图三.中断DFS父图形在第一个过程实际关闭循环之前，从顶点A开始的循环访问顶点C。进一步假设A > F.当通过第二个过程探索顶点C时，C的DFS父图被重置为指向顶点A，因此DFS父图中可能的循环被中断（参见图3.b）。为了解决这个问题，我们为检测到循环的嵌套搜索分配一个新的（最高）标识，然后独立地重新执行它在图3的例子中，我们再次从顶点F开始嵌套搜索，不执行从A开始的第二次搜索在生成反例的过程中，管理员工作站被用作“收集器”，所有参与生成的工作站都向其发送信息。请注意，形成反例的顶点根据分区函数分布在网络上。反例分两步生成。 在第一个图中，DFS父图 从检测到循环的状态开始遍历。标记访问过的顶点以发现循环。一旦访问了已标记的顶点，就可以从已发送并保存在管理员工作站上的顶点重建循环。此外，管理器能够确定循环上具有最小距离的顶点v。在生成的第二步中，BFS父节点从v遍历回到图的初始顶点。完成第二步后，可以使用存储在管理员工作站上的信息将整个对比示例放在一起。我们算法的一个显著的积极特征与它提供的反例的长度有关。由于该算法主要基于广度优先搜索探索，因此反例往往很短。参见实验部分的一些例子。J. Barnat等人/理论计算机科学电子笔记133（2005）21335偏序约简在本节中，我们将描述如何将偏序约简与我们的分布式内存算法相结合。在解释所提出的分布式方法之前，我们首先简要回顾主要是[10用图作为语义模型来描述偏序约简方法是不够的我们分析的并发系统是mod-更恰当的说法是状态转换系统（标记为转换系统）。如果S是状态集，则跃迁是关系α<$S×S。一个状态转移系统被定义为一个元组M =（S，s0，T，L），其中s0∈S 是一个初始状态，T是一组跃迁α<$S×S，L：S→2AP是一个标记函数，它为每个状态分配一个原子集合AP的子集，提议如果存在状态sJ使得α（s，sJ），则在状态s中使能转移α∈T在状态s中启用的所有转换的集合被表示为启用（s）。我们假定过渡是确定性的，即，对于每个α和s至多是一个SJ，其中α（s，SJ），记为α（s）=SJ。 如果α（s，SJ），我们说SJ是s的后继。偏序方法利用了并发转换可以以任意顺序交错的事实。这可以通过定义转换对上的独立关系来形式化。独立关系I<$T×T是一个对称的反自相关关系，对于每个状态s∈S和每个（α，β）∈I，满足以下两个条件：(i) Enabledness – If(ii) 交换性依赖关系是I的补语。根据上述条件，利用启发式方法有效地计算依赖关系。独立关系表明，通过从源自状态s的独立转移中仅选择一个，可以对状态转移系统进行潜在的还原。然而，这不能保证简化状态转换系统是完整状态转换系统的正确替代，因为它没有考虑要检查的属性。此外，消除中间状态α（s）或β（s）中的一个可能会导致它的一些后继状态（对于验证很重要）无法探索。还需要附加条件来证明简化的正确性。下文对它们进行了描述。首先，我们要明确一个属性被纳入34J. Barnat等人/理论计算机科学电子笔记133（2005）21通过定义过渡可见性的概念来对于命题集合APJ<$AP，转移α∈T是不可见的，如果对于每对状态s，sJ∈S，使得α（s，sJ），L（s）<$APJ=L（sJ）<$APJ成立。如果变换不是不可见的，则它是可见的。集合APJ通常为由包含在已验证公式中的原子命题集合导出。减少的状态转换系统由修改的生成算法生成，该算法仅探索转换的子集，在生成期间遇到的每个状态下启用，称为样本集。样本集可以用一种不依赖于生成状态转移系统的特定方式的方式来定义。这是通过一组条件来实现的，这些条件将完整的状态转换系统与相应的简化的状态转换系统相关联。注意，对于一个给定的状态，可能有不止一个样本集满足条件。我们说，只要empty（s）=enabled（s），状态s就完全展开。设APJ是一组原子命题。关于集合APJ的充分条件是：C0样本= 0，如果启用=0。C1沿着完整状态图M中从s开始的每条路径，以下条件成立：如果没有首先发生的样本转换，则不能执行依赖于样本转换的转换。C2如果启用APJ。（1）凡所有相，皆是虚妄。 到C3（循环关闭条件）如果简化状态图MR中的循环包含某个转换α被启用的状态，则该循环是不允许的，但该状态从不包含在该循环上的任何状态s的样本这些条件刻画了生成满足安全性和活性检验要求的简化状态转移系统所需的充分集。我们的目标是结合偏序约简与我们的分布式内存算法。简化系统由生成算法计算，该生成算法系统地探索状态，对于每个状态s，它选择一组启用的样本，并仅从样本进行转换。毫无疑问，这种算法的关键部分是分布式存储器检查充足的条件。虽然检查条件C0和C2很容易，可以在本地完成，但检查条件C1和C3与解决可达性问题一样困难。尽管如此，条件C1可以使用与序列情况相同的近似解析法进行局部检查（参见[10]）。因此，循环关闭条件C3是唯一难以检查的条件 分布式环境。在探索状态的顺序情况下，J. Barnat等人/理论计算机科学电子笔记133（2005）2135图通过深度优先搜索，条件C3使用搜索栈在恒定时间内检查。事实上，下面的更强的条件被用来代替C3。C3-dfs如果一个状态s没有完全展开，那么在example（s）中没有任何转换会导致在搜索堆栈上的状态。我们的目标是开发一个对应的条件C3-dfs的广度第一搜索为基础的生成的状态转移系统，分布在几个工作站。一个新的但书是基于这样一个事实，即在广度优先搜索中关闭一个循环的必要条件是关闭循环的状态已经在搜索期间被访问过。因此，我们使用下面的循环关闭条件，可以很容易地检查。C3-bfs如果状态s未完全展开，则样本（s）不包含后台边缘，即一个过渡，导致一个状态，是在当前或前一级的广度第一搜索。为了在我们的分布式内存上的算法中利用偏序约简，我们使用了类似的方法，例如在模型检查器SPIN [13]中实现。该方法将状态空间的构造与通过探索乘积图来检查它是否满足规范相唯一需要注意的条件显然是循环条件C3-bfs。可以证明，检查产品循环的条件是正确的。我们已经实现了该方法，并通过实验证实了空间和时间的减少6实验评价我们从头开始实现算法，因此实现错过了标准顺序工具（例如SPIN）中常用的许多优化。特别是，我们的实现的部分订单减少是相当远离最佳。出于比较的原因，我们实现了嵌套DFS算法，没有任何优化。所有的实验都是在一个由12个工作站组成的同构网络上进行的，这些工作站通过100Mbps交换式以太网互连。每个工作站都配备了Intel Pentium 4 2.6 GHz CPU和1GB RAM。我们测量了各种模型检测问题的算法的性能这些模型包括电梯模型（elev）、领导者选举协议（lead）、Peterson互斥解决方案（pet）、哲学家就餐问题（phil）和实时以太网协议（rte）。所有的模型都被参数化了：电梯由服务的电梯数量决定，领导者选举，彼得森和哲学家由服务的电梯数量决定。36J. Barnat等人/理论计算机科学电子笔记133（2005）21问题型号（M）已验证财产（美元）？M|=电梯1电梯G（r1 =<$（<$p1 U（p1U（p1 <$o）没有电梯2电梯G（r1 =（<$p1 U（p1 U（< $p1 U（p1 U是的lead1领导人选举FG（一个领导人）是的lead2领导人选举F（更多领导者）没有pet1彼得森G（p0 in cs =<$F（<$p0 in cs））是的pet2彼得森G（<$p0 in cs =<$F（p0 in cs））没有pet3彼得森误差GF（Someone in CS）没有phil1哲学家GF（phil0 eats）没有phil2哲学家GF（Someone Eats）是的RTE 1RT以太网G（r0 =（<$ce U（<$ce（rt0 R<$ce）是的RTE 2RT以太网G（w0 =（<$ce U（<$ce（rt0 R <$ce）没有见图4。模型和验证的属性参与进程，RT以太网由网络节点的数量决定。对于每个模型，我们验证了一些LTL公式，试图涵盖两种情况，即模型满足公式的情况和不满足公式的情况。请参见图4中的表格，以获得我们使用的模型检查问题的列表图5中的表格显示了为选定的模型检查问题生成的反例的长度。“反例长度”列给出了由我们的算法产生的反例的长度，而“反例长度（NDFS）”列给出了由嵌套DFS算法产生的反例的长度。可以看出，我们的算法产生的反例比标准的嵌套DFS要短得多。另一方面，嵌套DFS算法发现和生成反例所需的时间一般较短。这种差异显然是由于我们的算法在发现接受循环之前，与嵌套DFS算法相比，我们的算法探索了更多的状态。生成反例所需的时间（以秒为单位）见同一表。进行其他实验以评估基于条件C3-bfs的偏序约简。参见图6中的表格。我们测量了完整图（“无POR”列）中的状态数和简化图（“POR”列）中的状态数。此外，我们测量了图中通过[10]中给出的标准偏序约简减少的状态数（列“POR-DFS”）。使用标准顺序DFS算法测量该值（注意，仅实现了减少J. Barnat等人/理论计算机科学电子笔记133（2005）2137问题反例长度反例长度（NDFS）时间时间（NDFS）电梯1（9）853231361电梯1（10）653565271中文（简体）747431中文（简体）9292691中文（简体）396311中文（简体）8512871中文（简体）1221511中文（简体）1262511中文（简体）5411611中文（简体）51857911中文（简体）51857912中文（简体）51207301635中文（简体）20717478544中文（简体）244605207618图五、反例长度和生成时间问题无POR国家数目国家数目电梯2（10）111306211130621113062中文（简体）1105376068160681领导1（5）362901114878911487891中文（简体）242923351815中文（简13210413096510396338J. Barnat等人/理论计算机科学电子笔记133（2005）21体）中文（简体）95161429478643-中文（简体）847653847653847653中文（简体）24685482468548-中文（简体）575927757592775759277见图6。 偏序约简关于领袖选举和彼得森模型的在Leader选举模型下，基于C3-bfs条件的约简与标准的偏序约简相同，而在Peterson模型下，基于C3-bfs条件的约简略差.最后，我们测量了所建议的偏序约简的影响J. Barnat等人/理论计算机科学电子笔记133（2005）2139关于反例的生成。图7中的表格显示了反例长度（可以看出，如果采用偏序约简，则最浅的接受循环可以稍微更深。这可能会增加在发现接受循环之前由算法探索的状态的数量以及发现和生成反例所需的时间（参见行pet2（4））。然而，偏序约简对反例长度的影响通常是最小的。问题CE长度CE长度（POR）时间时间（POR）水平水平（POR）中文（简体）7474337373中文（简体）929269619191中文（简体）3938112021中文（简体）858973943133中文（简体）12141179中文（简体）121511710见图7。偏序约简对反例生成7结论和相关工作我们提出了一个扩展的算法在[2]中提出了一个完整的LTL模型检测算法，而不会失去任何积极的功能。特别是，我们将展示如何检测接受周期，生成反例，以及如何采用偏序约简。与嵌套DFS算法返回的反例相比，该算法的反例非常短.这是由于状态空间生成的广度优先性质。然而，找到反例的时间通常更长，必须探索更多的状态。我们强调，反例的简短是至关重要的调试。该算法的另一个积极特征是它在具有少量后台边的图上的行为。在这种情况下，我们的算法的行为完全LTL模型检测实际上等于可达性分析。有几个模型证实了这一点。另一方面，广度优先方法也有一些缺点我们已经提到，通常需要更多的时间来找到一个反例。此外，嵌套DFS算法有时能够在非常大的图中找到错误，而我们的算法只有在这些情况下错误距离初始顶点不远另一40J. Barnat等人/理论计算机科学电子笔记133（2005）21当图包含许多后台边缘时，会出现缺陷。此外，如果图不包含接受循环，则必须对其进行充分探索，并且频繁地重新访问状态会导致计算时间比简单的可达性分析时间正如在[14]中首先讨论的那样，利用C3-dfs条件的偏序约简技术很难转换为分布式存储器状态空间生成。另一方面，我们的算法结合C3-bfs条件实现的减少在许多情况下实际上相当于减少标准的顺序嵌套DFS算法。当然，在某些情况下，C3-bfs太弱而不能给出显著的减少。在[17]中，提出了分布式算法TwoPhase与顺序嵌套DFS算法相比，TwoPhase算法简单得多，因为它只适用只要没有满足充分条件的单例，状态就完全扩展。我们没有直接将我们的al-tax m与TwoPhase算法进行比较。最近，在[8]中提出了另一种在分布式环境中进行偏序约简该技术用于生成缩减的状态空间，但不可能将其直接与即时呼吸优先搜索算法相结合。分布式反例生成（如果考虑的话）通常被执行为两个可达性过程：第一个将可达顶点定位BFS父图已用于[9，7]中的第一次搜索。引用[1] J. 巴尔纳特湖我和布里姆。 不知道。 PropertyDrivenDistributionofNestedDFS. 在M。Leuschel和U.Ultes-Nitsche，编辑，第三届验证和计算逻辑国际研讨会论文集（VCL[2] 巴纳特湖Brim，and J. Chaloupka.并行宽度优先搜索LTL模型检测。第18届IEEE自动化软件工程国际会议（ASEIEEE计算机协会，10月。2003年。[3] 巴纳特湖Brim，and J. Chaloupka.基于广度优先搜索的分布式内存LTL模型检测。TechnicalReport FIMU-RS-2004-07，Faculty of Informatics，Masaryk University Brno，2004.[4] J. 巴尔纳特湖 Brim和J。 是的。在S P I N中进行分布式LTLMDel-Checking。 我是马特。Dwyer，editor，Proceedings of the 8th International SPIN Workshop on Model Checkingof Software（SPIN施普林格出版社。[5] G.贝尔曼分布式时间自动机可达性分析之效能研究。在proc 并行和分布式模型检查研讨会，第68卷，理论计算机科学电子笔记。Elsevier Science Publishers，2002.[6] B. Bollig，M. Leucker和M. 韦伯 平行无交替μ演算的模型检验。在Tiziana Margaria和Wang Yi编辑的第七届系统构建和分析工具和算法国际会议论文集（TACASSpringer-Verlag，2001.