共享存储结构模型检测的有效状态探索

《理论计算机科学电子札记》68卷第4期（2002年）网址：http://www.elsevier.nl/locate/entcs/volume68.html16页共享存储结构模型检测的有效状态探索科妮莉亚山口Inggs1，2和Howard Barringer3，4曼彻斯特大学计算机科学系英国摘要在本文中，我们提出的结果，从实验研究调查的实现策略显式状态的时间逻辑模型检测的虚拟共享内存的高性能并行机架构。特别是，一个并行状态探测算法，使用两个队列结构的负载平衡的建议，其性能分析的手的实验研究。然后，我们讨论了并行自动机理论模型检测使用这种并行状态探索算法的实现问题。1介绍模型检查是一种成熟的设计自动验证技术这主要是由于在过去十年中，在开发专门的编码和算法以减少状态爆炸问题的负担方面取得了巨大的进步[4，10，15]。然而，状态爆炸仍然是一个研究得很好的研究问题，最近获得更多兴趣的一项技术是模型检查的并行化。通常，开发人员可以访问大型并行计算机，但不能充分利用它们，因为大多数模型检查器是为单处理器系统设计然而，在大型并行体系结构上的成功实现，使处理器能够访问速度明显更快的本地内存（例如在我们的1在英国大学ORS奖的全力支持下，曼彻斯特大学计算机科学奖学金，和南非哈里·克罗斯利奖学金。2cinggs@cs.man.ac.uk3由EPSRC赠款GR/M05744提供部分支助。第howard@cs.man.ac.uk2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。英格斯和巴林杰2Manchester Computing机器，SGI Origin 3000具有512个处理器和512 GB内存）和加速潜力-三倍或四倍的加速可能看起来不太显著，但是，等待一天比等待四天发现一个错误要在本文中，我们提出了从实验研究的结果调查的实现策略显式状态的时间逻辑模型检测的虚拟共享内存的高性能并行机架构。提出了一种高效的并行状态探测算法，并讨论了基于该算法的并行自动机模型检测器的实现。相关工作：大部分现存的并行模型检测研究都集中在分布式网络上的实现上，主要是通过方便地访问这些计算场[13，20]。在分布式和共享存储器架构上并行模型检查的一种常见方法是使用切片函数跨处理器划分状态空间已经采用了不同的切片技术，但是在大多数情况下，切片算法是静态的，即，切片取决于状态而不是工作负载的分布[20，18，12]。Stern和Dill [20]通过使用随机负载平衡在进程中划分访问状态来并行化Murφ模型检查器;即，用散列函数（在给定状态的情况下，返回两个预定边界之间的数值该算法实现了近线性的加速比和其他一些作者基于他们的实现这个算法。首先是Lerda和Sisto [18]，他们实现了SPIN的分布式版本[14]来检查安全属性。他们用切片函数取代了随机哈希函数，该函数试图通过使用状态的结构来最小化交叉转换（属于不同进程的状态之间的转换）。他们的算法只显示了对于太大而无法在单个处理器上探索的状态图的加速Behrmann等人[6]在符号模型检查器UPPAAL的分布式实现中使用了[20]的散列函数技术，但是由于他们的模型检查器使用广度优先搜索执行得更好，他们添加了一个启发式算法来排序每个处理器的状态，以便分布式搜索尽可能接近广度优先搜索，这在某些情况下导致了超线性加速。Garavel等人[12]为CADP验证工具集[17]实现了分布式状态它们的切片算法独立于状态的结构属性来划分状态，因此独立于所使用的特定语言。最近的工作并行模型检测算法使用类似的静态切片，ING技术集中在检查活性的属性。马丁和哈达特[19]提出了一种活锁分析的算法，其中通过英格斯和巴林杰3修剪图;删除没有外出弧的节点，直到没有这样的节点剩余。该算法尚未实现，并且具有必须在修剪开始之前构建整个图的缺点Barnat等人[2]扩展了Lerda和Sisto的算法[18]以允许活性检查。该算法执行分布式深度优先搜索（DFS），如[18]所示，但每当达到接受状态时，它被存储在一个特殊的数据结构中，以便可以从该状态执行嵌套DFS所有等待其嵌套DFS的状态都被发送到管理器进程，在该进程中保存一个接收状态然后，管理器确保在任何时候都只执行一个嵌套DFS该算法允许对比顺序版本更大的状态空间进行LTL属性的模型检查Brim等人[3]用负循环检测算法代替嵌套DFS算法，以解决单源最短路径问题。其实施允许合理分配。Bollig等人。[7]试图通过开发一种没有循环检测的算法来克服并行循环检测他们研究了无交替μ演算的博弈论模型检查算法，并确定了μ演算的无交替片段的一个特征，该特征允许他们定义一个使用着色机制而不是循环检测的顺序算法，这允许一个有效的并行实现，并且可以很好地扩展。据我们所知，实现动态切片算法的唯一模型检测算法是Heyman等人的分布式符号算法[13]第10段。每当内存变得不平衡时，通过重新分区状态空间来保持内存平衡。这种方法的缺点是，当对特定处理器执行重新切片时，这些处理器不能继续进行状态探索。最后，我们提到了一个并行的状态空间探索算法从非模型检查的背景。该算法由Allmaier和Horton [1]开发，用于共享内存架构上的随机建模该实现使用共享堆栈进行动态负载平衡，并使用修改后的B树存储访问状态。对B树的访问它们实现了加速，本文件：提出了一种在虚拟共享内存并行机上进行状态探测的并行算法该算法实现为N个状态探测器进程的并行组合，其中每个进程都有一个私有和共享队列。负载平衡通过工作窃取来维护，并且与用于存储未扩展状态的两个队列结构一起，它允许以最小的同步进行隐式和动态负载平衡然而，可见状态被保存在一个全局哈希表中，而不是分布在进程中-英格斯和巴林杰4以可能的冗余工作的小成本实现同步锁我们的技术将在下一节中描述，其性能将在第2.2节中根据实验结果进行在第3节中，我们讨论了使用所提出的并行状态探索算法的交替自动机模型检查器的实现问题我们的结论在第4节中概述。2并行状态探索在我们开始描述并行状态探索算法之前，澄清一些术语会有所帮助。处理器指的是硬件，因此可用的处理器数量对于特定机器是固定的，而进程指的是控制线程，并且可以变化。在我们的例子中，一个进程在一个处理器上运行，所以五个进程将在五个处理器上执行。值得注意的是，在分布式共享内存架构中，系统将内存视为全局共享实体，但内存实际上是物理分布在处理器上考虑在单个处理器上的搜索，它恰好是DFS，其中堆栈用于存储未扩展的状态（没有计算后继的该算法从堆栈上的初始状态和存储空开始。它重复地从堆栈中弹出一个状态，计算它的后继并将它们推送到堆栈上。当堆栈为空并且从初始状态可到达的所有状态都在存储中时，算法终止在简单的并行化中，搜索被划分到多个进程中，通过添加两个互斥锁，可以在所有进程之间共享单个堆栈和存储，以分别同步对两个数据结构的访问。但是对这种技术和类似技术的实现的实验表明，在共享架构上使用锁进行同步几乎可以串行化否则并行实现[16]。实验还显示，我们最初选择的实现语言Java在SGI Origin机器上存在重大缺陷。首先，全局堆上的内存分配和垃圾收集涉及非常昂贵的同步，其次，没有工具可用于识别瓶颈。目前我们所有的实现都是C语言的我们实现了几个原型来实验不同的负载平衡技术，并分析了不同技术的同步成本我们最有效的解决方案，关于并行探索期间的加速，使用共享和私有数据结构的混合来进行负载平衡和存储结果，并使用[11]中描述的基于低开销令牌的算法来检测终止下一节将更详细地描述并行设置英格斯和巴林杰5州生成州生成2.1实现细节参与状态探索的每个进程都有状态生成器的私有副本状态生成器是一致的，即，它们都为任何给定的状态产生完全相同的继任者数据结构，如图所1中，包括用于存储访问状态的单个共享存储，以及用于存储未扩展状态的每个进程的两个队列第一个队列是无界私有队列，第二个队列是有界共享队列。一个进程只能将状态添加到自己的私有和共享队列中，而不能添加到任何其他进程的队列中，但它可以从其他进程的共享队列中删除状态（这称为工作窃取）。因此，每个共享队列都有一个锁来同步对它的读写访问。存储是一个哈希表，没有互斥锁来同步访问。然而，当多个进程创建相同的状态时，这可能会导致重复的工作，但由于可用的并行计算比自然并行任务多得多，执行冗余工作并不是一个显著的开销。共享队列共享队列私有队列私有队列...Fig. 1. 并行图搜索体系结构所有资源管理器进程执行完全相同的算法。然而，选择一个资源管理器进程来执行两个额外的任务：第一个是启动终止检测算法，第二个是在检测到终止每个资源管理器进程执行以下任务集，直到计算出所有可到达的状态并检测到终止：(i) 移除一个状态。当一个进程空闲时，它会尝试按以下顺序从队列中删除一个状态它首先检查其私有队列的状态。如果未找到状态，则进程获取互斥锁以从其自己的共享队列中删除状态。如果再次删除状态失败，它会搜索所有其他共享队列，直到找到一个非空队列或所有共享队列都为空。(ii) 检查终止。当一个空闲进程不能从它可以访问的任何队列中删除一个状态时，终止检测算法被执行：空闲进程检查它是否有终止令牌，如果有，则将令牌传递给下一个进程。不需要锁来检查终止。✲✲✲✲Explorer进程N探索者进程1共享商店英格斯和巴林杰6(iii) 计算继任者。如果一个进程删除了一个状态，则会生成该状态的所有后继计算出的第一个新的后继进程将由当前进程扩展，其他的将添加到它的一个队列中。如果共享队列未满，则将状态添加到该队列，否则将状态添加到私有队列。由于每个进程都有足够的工作可用，因此这些进程在大多数时间都使用自己的私有队列，这使得共享队列用于负载平衡目的。然后，当需要负载平衡时，因为进程已经变得空闲，两个队列结构确保空闲进程窃取工作不会中断任何繁忙进程。为了最小化共享队列上的争用，空闲进程pi总是开始搜索非空的share dqueueat过程sp（i+1）modN，其中N是过程的第n个ber，并且过程由p0，p1，.，p N-1。负载平衡和进程间状态图划分的效率取决于状态图结构和共享队列大小的组合。例如，一个纯线性图，其中每个状态有一个后继，将只在一个处理器上生成，这比在几个进程之间共享此任务更快共享队列的大小完全不影响对这种图的探索。但是考虑一个分支因子为4的图在进程pi生成初始状态的后继进程之后，已经有足够的工作量供四个进程使用然而，对于一个一次保存一个状态的共享队列，pi-1也可以开始工作，因为另外两个额外的状态将在过程中P1 小型共享队列可以因此妨碍负载平衡。然而，对于非常大的共享队列，处理器会将本来可以添加到其私有队列的状态添加到其共享队列，由昂贵的互斥锁控制。共享队列大小和分支因子之间的关系是通过在具有4GB内存的16处理器SGI Origin 3400上探索几个人工生成的图来研究的;获得的结果在下一节中总结。2.2实验结果实验已经在许多人工生成的具有不同结构和不同大小的图上运行然而，本节中报告的性能结果是从一组具有以下结构的图中获得的：图中的每个状态都有x个唯一的后继状态和一个到旧状态的转换（在计算此转换时已经访问过的状态）。对于每种情况，后继者的数量（x）和共享队列的大小是固定的，然后对图进行5次探索5次运行的平均值用于图1中的性能图2和3平均英格斯和巴林杰7因为存在许多影响运行时间的变体，例如，由高速缓存争用推断的高速缓存线使用的不可预测性，或者状态被物理存储在哪里在单用户模式下运行的结果分析显示，平均值稳定在5次运行内图1左侧的性能图图2显示了具有固定分支度x= 3的2500万个状态图的探索时间，而共享队列大小从1到4不等，图2右侧的性能图。图2显示了2500万个状态图的探索时间，其中固定的共享队列大小为4，分支度不同，x= 1， 2， 3， 4。0.30.250.20.150.10.05(a) 分支度3，共享队列大小1-40.250.20.150.10.05(b) 分支度1-4，共享队列大小402 4 6 8 10 12 1416数量的处理器02 4 6 8 10 12 14 16数量的处理器图二.具有不同分支度和共享队列大小的图的探索性能。从这些图中可以清楚地看出，最佳共享队列大小等于分支度或比分支度大一这里没有显示的其他性能图表证实了这种关系。最坏的情况是，当探索具有高分支因子的图时，使用非常小的共享队列大小对于分支因子为2的图，最小共享队列大小1并不昂贵，但是对于更高的分支因子，当处理器数量大于某个阈值时，性能开始下降，如图1左侧的图所示二、图1右侧的性能图图2表明，对于分支度小于或等于4的图的有效负载平衡，固定的共享队列大小为4是足够的 总的来说，发现比最优共享队列大小稍大的共享队列大小优于比最优共享队列大小稍小的共享队列大小。对于大于最优的共享队列大小，具有不同分支因子的图的性能变化不是数量级的。因此，为了探索具有不同分支度的一组图或具有不同分支度的单个图（如在模型检查期间探索的图所常见的），如果优选运行上的静态队列大小，则应选择更接近较高分支度的最优分支对于最小和最大分支度之间存在显著差异的图，也可以考虑改变共享队列大小dy。12341/时间12341/时间英格斯和巴林杰8或者仅当被扩展的状态具有多于特定数量的后继者时才将后继者添加到共享队列另一个比动态改变队列大小更便宜的策略是从共享队列大小（比如x）开始，然后使用每个状态生成的平均成功数来确定剩余搜索的共享队列大小如果需要，可以每k个状态重复该计算。0.50.450.40.350.30.250.20.150.10.050(a) 分支度3，共享队列大小31000万个州2 4 6 8 10 12 1416数量的处理器0.080.070.060.050.040.030.020.010(b) 分支因子3，共享队列大小31亿个州2 4 6 8 10 12 14 16数量的处理器图三. 小图和大图的探索性能。分别探索1000万状态图和1亿状态图的性能图图1左边的图表图3显示了大约1000万个状态或更少的状态图的一般性能加速几乎是线性的，直到性能达到平台的某个阈值。这是因为探索只有1000万个状态的状态图的工作不足以充分利用所有的处理器;即使在单个处理器上，完整的探索也在18秒内完成。对于更大的图，加速比在16个处理器内不会达到平稳状态，如图3右侧的图所示研究还发现，虽然加速率并没有显着变化的图形与许多超过10万个国家，加速率略有增加，图形大小的增加。目前还没有在具有512个处理器的SGI Origin 3000上执行实验，只有在16个处理器的SGI Origin3400上执行实验，但预计加速将继续增加，直到处理器的计算能力超过正在搜索的图形所需的计算能力，并且处理器的同步开销变得占主导地位。国家探索，即，计算系统的可达状态是模型检查的一个组成部分。事实上，单独检查安全属性是一个可达性分析问题，而活性检查则是在有限个循环中识别额外的结构。在下一节中，我们将讨论基于并行状态探索算法的安全性和活性特性的并行模型检查器的实现。1/时间1/时间英格斯和巴林杰9|≤3基于交替自动机和博弈论的并行模型检测一个状态图可以表示为一个Kripke结构：一个四元组K=（S，T，s0，L），其中S是一个有限的状态集，T<$S×S是一个必须是全的转移关系（对于每个si∈S，至少存在一个sj使得（si，sj）∈T），s0是一个初始状态，L：S<$→2Prop将每个状态映射到一个在该状态下为真的原子命题集。则对于Kripke结构K和时序逻辑公式φ，模型检查器确定K=φ。在我们考虑的自动机理论模型检查上下文中，时序逻辑公式首先被转换为自动机Aφ，它精确地接受满足公式的所有计算。然后模型检查器构造乘积自动机AK，φ=K×Aφ，如果AK，φ接受的语言非空，φ对K成立，否则不成立[23，21，9，5]。在我们的上下文中，我们使用犹豫交替自动机[5]来表示分支时间公式（CTL*），并并行化Visser [22]开发的面向游戏的作为简要介绍，有限树上的自动机（树自动机）运行在无树标记树上。交替自动机A在树T上的游程r是一棵树，其根标为s0每隔一个节点用（N×S）的元素标记。 r的每个节点对应于T的节点。r中的节点（x，s）对应于自动机在状态s中读取T中的节点x。注意，r中的许多节点可以对应于T中的同一个节点。节点及其后继节点的标签必须满足转移函数。如果运行的所有无限路径满足接受条件，则运行是接受的请注意，我们可以在树中得到表示运行的有限个分支，当在transition函数中读取true或false在接受运行中，只有在有限分支的末尾才能找到true。不 同 类 型 的 交 替 自 动 机 有 不 同 的 接 受 条 件 。 在 犹 豫 交 替 自 动 机（HAA's）中HAA的集合可以划分为不相交的集合Si，并且集合之间存在偏序。集合可以进一步分类为瞬时的、存在的或泛的，使得对于每个Si，以及对于所有s∈Si，a∈N，并且k∈N，以下成立：• 如果Si是瞬态的，则δ（s，a，k）不包含来自Si的元素• 如果Si是存在的，则δ（s，a，k）只包含Si的• 如果Si是泛的，则δ（s，a，k）只包含Si的合取相关从HAA的这种限制性结构可以得出，每一条无限路径π要么被困在一个存在集S i中，要么被困在一个泛集Si中。路径满足（G，B）当且仅当Si是存在的且inf（π）<$G/=<$或Si是泛的且inf（π）<$B=<$（inf（π）是路径π上无限重复的状态集）。英格斯和巴林杰10给定一个分支时间公式φ和一个Kripke结构K，模型检验可以使用HAA通过遵循本节开始时概述的基本步骤来解决，但当然要使用为HAA定义在Visser [22]中，乘积自动机的非空性检查被定义为一个两人博弈，其中参与者1试图表明交替自动机是空的，而参与者2试图确定它是非空的。一个博弈是一个可能无限的状态序列（q0，s0），（q1，s1），. . ，其中每个状态是Kripke结构和al-1结构的乘积中的节点公式的自动循环产品自动机的结构决定了当在游戏中发现标记为真（2胜）或假（1胜）的节点时，找到乘积自动机中的无限路径当一个无限的路径被发现时，接受条件被认为是决定游戏的赢家当参与人2陷入存在的Si时，如果inf（playπ）<$G/=<$，请注意参与人1因为它只在有选择的情况下移动。当参与人1被困在一个普适的S i中时，如果inf（play π）<$B=<$B，那么这盘棋将被接受。病例总结见表1。1号玩家获胜2号玩家获胜游戏达到一个假的游戏达到一个真正的在参与人2移动之后，重新访问当 前游 戏中 的位 置 ，并且inf（playπ）G=在参与人2移动之后，重新访问当前游戏中的位置，并且inf（playπ）<$G/=<$在参与人1移动之后，它会重新访问当前游戏中的位置，并且inf（playπ）<$B/=<$在参与人1移动之后，它重新访问当前游戏中的位置，并且inf（playπ）B=表1非空博弈中一局的获胜条件该实现使用DFS算法和堆栈来存储当前路径。然后，由堆栈上的所有元素在重新访问位置的深度和堆栈的当前深度之间给出无限路径为了效率，存储器用于跟踪已经做出所有移动的状态的结果，使得当它们被重新访问时，结果可以被重新使用，但是随后可能发生存储不正确的结果，因为每当位置被重新访问时，播放被截断。为了确保结果在存储时是正确的，一旦从该状态开始的所有移动都已经进行，则针对该状态进行新的游戏这个新的游戏使用了一个新的结果存储和堆栈，所以任何在上一个游戏中可能被截断的无限次游戏都可以英格斯和巴林杰11−游戏将被玩到完成。新的博弈可以递归地进行一旦一个州的新游戏已经完成，新游戏的堆栈和结果存储就被删除，结果存储在原始结果存储中。[22]中讨论的进一步优化是推迟新游戏，但在随后的并行实现讨论中没有考虑并行算法：并行模型检查算法的基本设置和数据结构与第2节中描述的为并行图搜索而开发的并行模型检查算法和图1所示的并行模型检查算法相同有了这样的设置，图形不再像上面的串行案例那样以深度优先的方式虽然一个过程将继续从一个特定的状态，直到它到达一个旧的状态DFS路径，没有回溯机制。相反，未扩展的状态从队列中删除，因此可以是图中任何位置的随机状态其结果是一组路径，每个路径在进程之间划分的可能不同的生成阶段;因此没有存储当前路径的堆栈第二个结果是，一个进程可能会到达一个结果未知的旧状态，因为另一个进程仍然忙于计算它。因此，需要一种机制来跟踪等待结果的状态我们并行循环检测：一种策略是在本地而不是全球玩新游戏。每当一个状态被重新访问时，局部循环搜索在处理器上使用深度优先堆栈执行，就像在单处理器的情况下一样，但是这可能不会有效地使用可用的处理器。另一个策略，也是当前实施的策略，是对路径段5进行编号，使得状态图中的每个状态与唯一的段号相关联因此，状态被映射到节号及其在该节上的深度。当一个状态被展开时，它的第一个未访问的后继者被分配与其父状态相同的部分，并且深度比父状态大一个。它的父母的深度每个其他未访问的后继者都被赋予一个新的节号。段号由创建状态的处理器分配。 每个进程i都有一个唯一的数字序列i，i + N，i +2N，. （其中N等于参与搜索的处理器的数量，并且处理器从0到N1编号），其可以分配给新的路径部分。已访问的继任者将已经分配了一个区段编号。当存在从路径部分πi上的状态到路径部分πj上的状态的转变时，部分πj被称为部分πi的分支。5路径的任何子序列都可以称为该路径的一段。英格斯和巴林杰12⟨ ⟩ ⟨⟩请考虑图4所示的状态图它是由4个过程（N= 4）。遇到六个新的路径段，并分别用线程1（路径段1、5、9）、2（路径段2）和3（路径段3、7）编号路径截面π1= s0，s1，s3，s6，s11，. 有两个分支，即部分π5=s2，s4，s10，s12，. 并且π9= s7，s15，. . .2013年3月，2月见图4。 一个状态被标记为i，j，节号及其分支存储在路径表中，其中路径表中的每个条目具有以下字段：(i) 第X节(ii) 树枝条目i，y，j的列表，其中i，y，j表示存在从路径x上深度i处的状态到路径y上深度j处的状态的转换;因此路径y是路径x的分支。作为示例，图4的路径表在表2中给出路径表在物理上分布在进程之间每个进程i只能将新的路径段添加到路径表的其部分中，并且由于每个进程都具有其可以分配的唯一编号序列，因此不需要锁来分配新的段编号并将新的路径段添加到路径表中。然而，多个处理器可以将分支添加到同一路径部分，因为多个处理器可以重新访问同一部分上的状态，因此需要互斥锁来同步分支的插入通过该实现，每当达到访问状态时，执行以下算法以检测周期。给定父状态和重访状态的路径区段，算法搜索路径区段的序列，其中每个区段开始于大于或等于从前一区段的转变到达它的深度的深度，并且最后一个区段开始于大于或等于从前一区段的转变到达它的深度的深度。s01，1第1条第1款，第2款第2条第5款，第1款第3条第1款，第3款s45，2s 52，1s61，479，1 105，382，2第9条第3、1款s111，5s 159，2s 125，4s 132，3第16条第7款，第1项S14英格斯和巴林杰13截面数B牧场（深度）11，5，151，2，19∅21，3，13∅7∅图4中图形的路径部分序列中的区段到达深度小于或等于搜索开始的深度的转发结果：当处理器重新访问一个结果未知的状态时，它只需在旧状态插入一个指针。然后，一旦旧状态的结果已知，遍历指针列表，并将结果转发给所有等待结果的状态。在此期间，当前处理器可以继续进行其他工作。执行问题：在并行模型检查器实现中，在每个进程上执行的并行状态探测算法被模型检查算法所取代，队列中不再存储状态，而是存储工作项。然后，工作项存储产品自动机中的状态或结果，并且每个工作项保持该工作项所属游戏的游戏计数器。如果工作项在产品自动机中存储了一个状态，则会计算新的后继状态，并按上述方式分配节号如果工作项存储了一个结果，那么需要考虑几种情况如果它是一个状态的结果，对于该状态，新的游戏还没有被玩过，或者在这个或任何其他游戏中没有被玩过，则从该状态开始新的游戏如果结果是针对一个已经在进行新博弈的状态，则该过程放弃并继续进行其他工作，因为一旦该状态的新博弈完成，正确的结果将被转发;必须注意确保两个新博弈不会等待对方的结果。来自已完成的新游戏的结果存储在原始存储中，并转发到挂起的工作项（等待当前结果的工作项而对于需要结果来计算多个结果的合取或析取的工作项，只有在组合结果已知时，才会存储和转发结果英格斯和巴林杰14生成反例：反例（轨迹）可以从路径部分及其分支生成。对于活性属性，路径部分关闭一个循环。每个分支指向另一个路径部分上的特定状态一个大纲反例可以作为这些状态的序列快速生成更详细的计数器示例可以通过将循环开始时的状态加载到状态生成器中并递归地仅生成循环路径上的后继状态直到再次到达开始状态来生成对于安全属性，从初始状态到最终状态的路径上的路径部分通过递归地遍历路径部分从其分支的父节点来计算，直到计算出初始路径部分与前一种情况相同的方法用于生成大纲或详细的反例。4结论我们已经提出了新的战略，并行状态图探索和模型检测的虚拟共享内存并行机架构。首先，我们提出了一个并行状态探索算法，使用一个组合的共享和私有队列，最小的同步效率和动态负载平衡。然后讨论了利用并行探索算法的双队列结构实现一种并行的在线模型检测算法对并行模型检测算法的初步实验表明，目前路径表的实现方式内存效率不高，需要进一步改进。 连同循环检测策略的改进，计划的未来工作包括使用实数图对并行模型检查算法进行实验分析，并调查其他并行化策略以进行比较。在实验中的并行状态探索算法接近线性加速比得到了一系列的图形类型和大小的16个处理器的限制。虽然在实际图上的实验仍然是必不可少的，但由于人工图的性质，我们希望在真实问题的状态图上的结果是相似的。本文提出的并行状态探测算法不仅可以实现高效的并行模型检测，而且可以有效地应用于其它基于状态探测的应用，如死锁检测、状态不变量检测、调度分析等。确认除了我们的赞助商之外，我们还要特别感谢计算机科学系的CNC（新计算中心），他们对并行化方法和实现进行了有益的讨论，并专门访问了他们的SGI Origin 3400机器。英格斯和巴林杰15引用[1] S.C. Allmaier和G.霍顿随机建模中的并行共享内存状态空间计算机科学讲义，1253，1997。[2] J.巴尼亚特 湖 布瑞姆， 还 有杰。 是的。 在S PI N中，Dis tr ibtdLTLmodel-check ing 。 在 Proceedings of the 8th International SPINWorkshop on Model Checking ofSoftware ， 卷 2057 的 Lecture Notes inComputer Science。Springer-Verlag，2001年5月。[3] L.布里姆岛Cerna，P. Krcal，and R.佩拉尼克基于负循环检测的分布式LTL模型检测。计算机科学讲义，2245，2001。[4] D. Bosn acki，D. Dams和L. 霍林和埃尔斯克岛。 SYMMETRICSPI N. 在SPIN模型检查和软件验证，计算机科学讲义第1885卷，第1-19页。Springer–Verlag,[5] O.伯恩霍尔茨分支时间时序逻辑的模型检测。博士论文，以色列海法理工学院，1995年6月。[6] G. Behrmann，T. S. Hune和F. W.凡德拉格分布式定时模型检查-搜索顺序如何重要。第12届计算机辅助验证国际会议论文集，1855卷，计算机科学讲义，第216-231页。Springer–Verlag,[7] B. Bollig，M. Leucker和M.韦伯无交替μ演算的局部并行模型检验。第九届国际SPIN软件模型检测研讨会论文集，计算机科学讲义。Springer–Verlag, April[8] E. Brinksma和A.疯了验证和优化PLC控制计划。SPIN Model Checking andSoftware Verification，1885卷，Lecture Notes in Computer Science，第73-92页。Springer–Verlag,[9] O. Bernholtz，M. Vardi和P. Wolper。 分支时间模型检测的自动机理论方法。第六届计算机辅助验证国际会议论文集，计算机科学讲义第818卷。Springer–Verlag,[10] E. M. Clarke，O. Grumberg和D. A.佩尔德。模型检查。麻省理工学院出版社，英国剑桥，1999年。[11] E. W. Dijkstra，W. H. J.Feijen和A. J.M.加斯特伦分布式计算终止检测算法的推导。InformationProcessing Letters，16：217-219，June 1983.[12] H. 加拉韦尔河马提斯库和我Smarandache。用于模型检测的并行状态空间计算机科学讲义，2057，2001。[13] T. Heyman，D.盖斯特岛Grumberg和A.舒斯特 实现可伸缩性并行可达性分析非常大的电路。InProceedings of the英格斯和巴林杰16第12届计算机辅助验证国际会议，第1855卷，计算机科学讲座笔记。 Springer–Verlag,[14] G. J. 霍尔茨曼计算机协议的设计与验证。Prentice Hall，Englewood CliJersey，New Jersey，1991.[15] G. J. Holzmann和Doron Peled。形式核查的改进在1994年10月，瑞士伯尔尼，FORTE'94会议记录[16] C. P·英格斯简化不同的模型检查范例。续报，曼彻斯特大学，2000年12月。http://www.cs.man.ac的网站。联合王国/~inggsc.[17] J.C. 费尔南德斯，H. Garavel，A. 克尔布拉特湖 穆尼耶河 Mateescu，以及M. Sighireanu CADP：协议验证和验证工具箱。在Proceedings of the 8 thInternational Conference on Computer Aided Verification CAV ， 卷 1102 的Lecture Notes in Computer Science，第437-440页，1996年[18] F. Lerda和R.西斯托使用SPIN进行分布式内存模型检查在第五届国际SPIN研讨会论文集，1999年7月[19] J. M. R. Martin和Y.赫达特并发系统死锁和活锁分析的并行算法。 在通信过程架构中，第1-14页。IOS Press，2000.[20] 联合Stern和D.迪尔将Murφ验证器标记化。在第九届计算机辅助验证国际会议上，计算机科学讲义卷1254。Springer–Verlag,[21] W. 托马斯无限对象上的自动机 在j. van Leeuwen，编辑，Handbook ofTheoretical Computer Science：Formal Models and Semantics，B卷，第135-191页。Elsevier Science，1990年。[22] W. 维瑟和霍华德·巴林杰实用的CTL模型检验：SPIN应该Software Tools forTechnology Transfer，2（4）：350-365，March 2000.[23] M. Y. Vardi和P. Wolper。自动程序验证的自动机理论方法。第一届计算机科学逻辑研讨会，第322-331页