基于消息传递通信的分布式内存集互模拟约简算法的设计和实现

《理论计算机科学电子札记》68卷第4期（2002年）URL：http://www.elsevier.nl/locate/entcs/volume 68. html16页s状态空间Stefan Blom1，3 Simona Orzan2，3CWI，P.O.Box 94079，NL-1090 GB Amsterdam，The Netherlands摘要已知的问题是，状态空间可以变得非常大，这使得由于内存不足而对它们进行操作（包括减少它们）变得困难。为了扩展可处理的状态空间的大小，我们设计并实现了一种基于消息传递通信的分布式内存集互模拟约简算法。通过使用消息传递，可以在大型SMP机器和工作站集群上使用相同的实现。该算法实现了大标记迁移系统模强互模拟的约简。我们证明它的正确性和终止。我们提供了一个评估的最坏情况下的时间和消息的复杂性和一些性能数据的原型实现。理论和实践都表明，该算法的规模与工人的数量。1介绍模型检测是一个资源密集型应用。提供这些资源的最常见的因此，开发分布式模型检查工具是很自然的这些工具可分为三类：象征性的、非正式的和列举性的。在所有三种方法中，都在进行分配方面的工作（[11]、[5]、[14]、[3]、[13]）。我们重点介绍枚举方法，然后是µCRL工具集（[4]）和CADP工具集（[8]）。在那里，首先生成一个规范的状态空间，将其以一个等价关系为模进行约简，然后对约简后的状态空间进行模型检查。状态空间生成已经成功地被分发（[9]），幸运的是，减少的状态空间足够小，可以在单个机器上进行模型检查然而，如果生成的状态空间太大，无法在单个机器上运行，那么1 电子邮件地址：sccblom@cwi.nl2电子邮件地址：simona@cwi.nl3我们感谢Hynek Mlcousek提出的有益意见。2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。布洛姆和奥尔赞2P需要分布式的还原工具。在本文中，我们提出了一个分布式算法，减少状态空间模强互模拟等价。相关工作。已经描述了非常好的顺序算法用于双相似性减少和双相似性检查：[12]，[16]以及基于这些，[7]。文献[2]证明了双相似性检验问题是完 全 的 ， 这 意 味 着 它 很 难 被 有 效 地 并 行 化 。 在 [18] 、 [17] 中 给 出 了Kanellakis-Smolka和Paige-Tarjan并行算法它们是为共享内存机器设计的，即使有可能在分布式内存计算机上模拟它们，也不太可能产生可接受的性能。我们的设置是不同的：我们正在寻找一种消息传递算法，它可以处理非常大的问题实例，并且可以很好地用于表示状态空间的特定类型的标记转换系统概况. 我们的算法是一个简单但令人惊讶的有效算法的分布式版本，在[12]中被称为“天真方法”。在第2节的一些描述之后，我们将在第3节讨论这个简单的算法，然后我们将在第4节介绍它的分布式版本第5节包含一些关于实现的统计数据最后，我们总结了结果并讨论了未来的工作（第6节）2预赛在本节中，我们为标记的转移系统定义了一个符号，我们回顾了强互模拟的定义，并陈述了互模拟约简问题。我们还提到了许多已知解决方案所使用的一般划分细化方案让Act是一组固定的标签，代表动作。定义2.1（LT S）一个标记的转移系统（LT S）是一个三元组（S，T，s0），由一组状态S，一组转移TS×Act×S和一个初始状态s0∈S组成。定义2.2（强互模拟）设（S，T， s0）是LT S.二元关系R<$S×S是强互模拟，如果对所有p，q∈S，使得pR q：• p−→• q−→pJ，<$qJ∈S：q−→aqJ，<$pJ∈S：p−→aqJpJR qJ和pJpJR qJ如果存在强互模拟R，使得p R q，那么我们说p和q是强双相似的如果两个跃迁系统（S1，T1，s1）和（S2，T2，s2）的初始状态s1和s2在化合物LT S（S1<$S2，T1<$T2，s1）中是双相似的，则它们是我们所关注的问题，即互相似性约简，是在给定的LT S上找到最大强互相似性的等价类。或者换句一一布洛姆和奥尔赞3π：=π0;π不稳定选择一组块{B1···Bn}<$ππ：=π−{B1···Bn}<${B11···B1m1，B21···Bnmn}其中，ni：{Bi1···Bimi}是Bi的分区，使得j=/k图1. 一个分区细化算法的框架。对于一个LT S，找到与它强双相似且具有最小状态数的LT S对于LT S（S，T，s0），S的元素的一个划分（用π是不相交块的集合{B i|i ∈ I} s.t. i∈IBi=S.大多数算法用于解决互模拟约简问题的方法是基于某种形式的分区细化，即它们执行连续的迭代，其中当前分区的块被分割成更小的块，直到没有任何块可以再被在分割块时，无法区分的状态保留在同一个块中。如果两个状态中的一个状态允许具有特定标签的到特定块中的状态的转变，并且另一个状态不具有具有相同标签的到相同块中的状态的转变，则可以区分这两个状态节点s相对于分区π的签名是s到sigπ（s）={（a，B）|s−→asJ且sJ∈B∈π}因此，通过定义，两个状态相对于一个划分是可区分的，当且仅当它们相对于该划分具有不同的签名。一个划分π被称为稳定的，如果该划分中每个块的每两个成员关于π具有相同的签名。使用签名的基本分区细化算法在图中概述1.一、该算法从给定的初始分区开始，并将具有相同签名的节点保持在同一块中。分区细化算法的正确性来自两个事实。首先，稳定划分是互模拟关系（如果节点在同一块中，则它们是等价第二，双相似节点对于每个计算的细化具有相同的签名因此，计算的互模拟关系是粗互模拟关系。为了LT S约简的目的，从初始划分{S}开始是方便的。 我们将在本文的其余部分这样做。布洛姆和奥尔赞4→→≥OO3序贯算法作为我们分布式实现的起点，我们选择了一个非常简单的互模拟约简算法，即[12]中称为“朴素方法”的算法从理论复杂度的角度来看，它无法与Paige-Tarjan算法[16]（（MN+N2）vs.（MlogN）），但实际上它表现得相当好。此外，它的简单性使其非常适合用于并行和分布式实现。与有界扇出Kanellakis-Smolka（[12]）和Paige-Tarjan算法相比，它们非常仔细地选择和分割块，朴素算法试图在每次迭代中分割所有块这意味着许多不可能分裂的块然而，由于其执行分区细化步骤的积极方式-将所有块分割成尽可能多的新块-朴素方法需要的迭代步骤数量要少得多此外，这种方法适合状态空间的特殊情况在图2中，我们已经描述了用于输入标记的转换系统（S，T，s0）的朴素算法的实现。其思想是相对于当前分区计算的签名确定下一个分区，即新分区的块是具有相同签名的节点集合跟踪当前分区是通过单射部分函数ID：2Act×N来完成的N，它为每个签名分配一个唯一的标识符（因此，每个区块）。 为方便起见，我们还将使用ID函数（ID：SN）的范围在状态上，值由状态签名的ID给出单个语句Assign N ew ID涉及到为ID赋值，使得ID（x）= ID（y）sig（x）= sig（y），x，y∈S。哈希表用于此目的。请注意，与一般的分区细化方案不同，SBR只计算新的签名，而不会显式地下面的引理证明，在初始划分为{S}的假设下，以这种方式计算的划分引理3.1对于n 0，将IDn，sig n表示为执行SBR的第n次迭代的步骤4之后的ID和sig函数（第一次迭代的索引为0）。则对于每个n> 0和对于每个x，y∈S：sig n−1（x）/= sig n−1（y）= sig n（x）/= sig n（y）。（一）证明让我们首先回顾一下，分配N个新ID需要注意，对于每个n>0且x，y∈S，IDn（x）= IDn（y）sig n−1（x）= sig n−1（y）。（二）我们证明了引理归纳n。初始划分是{S}，这意味着sig0（x）=sig0（y），<$x，y∈S。因此，对于n=1，该断言成立布洛姆和奥尔赞51. 对于所有x∈S ID（x）：= 0;2. 0;newcount：= 1;3. whileoldcount/=newcount一4.对于所有x∈Ssig（x）：={（a，ID（y））|x−→y};5.分配新的ID;6.oldcount：= newcount; newcount：=|{ID（x）|x ∈ S}|;F7. 对于所有x∈S ID （x）：=ID（x）;图2. （SBR）朴素算法设n> 1且x，y∈S使得sign−1（x）/=sign−1（y）。那么一定有一对（a，IDn-1（z）），（w.l.o.g.）发生在sign−1（x）中，不发生在sign−1（y）. 我们讨论了两种情况：（1）这两种情况都不是y−→a的过渡 t. Thensign（y）将不包含任何形式为（a，）的对，而sign（x）将具有at最小（a，IDn（z））。（ii）有从y出发的跃迁，用a标记。在这一点上，让你−→a 别跟他们过不去。 IDn−1（t）mutbe/=IDn−1（z），因为（a，IDn−1（z））∈/sign−1（y）.然后，从（2）可以得出，sign−2（t）sign−2（z）并且，通过使用归纳假设，sign−1（t）sign−1（z）。此外，本发明还我们应 用 （2）一个多时间，以获得IDn（t）=/IDn（z）. 我们已经准备好了sig n（x）将包含对（a，IDn（z）），但sig n（y）不包含。✷4分布式算法分发分区细化算法的明显方法是分发数据，同时保持全局控制。更准确地说，工作者执行迭代，在迭代中他们独立地做一些细化，然后同步结果。这种方法在理论上是可行的，但在实践中，同步可能会花费很多时间。这是选择朴素算法的另一个原因：通常它需要比KS和PT少得多的迭代，因此同步更少。4.1框架、假设我们的框架是一个无故障的分布式系统（即。worker消息传递是通过执行发送和接收操作来实现的。send（destination node，message）是非阻塞的，receive（message）是阻塞的。我们还假设具有相同源和目的地的消息消息是一种结构布洛姆和奥尔赞6i=0时FWW1.读Inji（j），读Outij（j）;2.return 1;3. 回路4.对于所有x∈Sisig（x）：={（a，p）|<$x，a，p<$∈ Outij，0 ≤ j0<$N expected answers> 0receive（msg）;casemsga哈希插入：j，s d在Hi和计算机ID中插入s;send（j，ahash ID：j，s，ID（s）d）;aendsig：jdN活跃工人−−;ahash ID：j，s，siddID（s）：=sid;N个预期答案−−;newcount i= |H i|;图5. WORKER i的Handle Messages例程这些签名。它还负责管理在步骤5J中使用的散列表的一部分。我们用H i表示i设Tij是具有在Si中的源状态和在Si中的目的地状态的转换的索引列表。关于Tij中的转换，工作者i将希望知道其源状态、其标签以及其目的地状态的签名的当前ID，以便能够计算源状态Workerj因此，工人i和布洛姆和奥尔赞8一一→{···−}→对于所有j：0≤jWsend（j，a update：i，[ID（y）]|y ∈Inji] d）; received：= 0;当收到Wreceive（aupdate：w，IDListd）;received++; updateOutiw;图6. 工作人员的更新ID例程是j被捕获在两个列表中，这两个列表按与Tij相同的索引排序：Ou tij=[x，a，ID（y）] |x−→y<$x∈Si<$y∈Sj]，驻留在i的第i个元素y中，Inij=[y|x−→y<$x∈Si<$y∈Sj]，在j的mem或y中。注意，元素可以在列表中重复出现-例如，如果一个状态是来自i上的节点的两个转换的目的地，则它在Inij中出现两次。Inji和Outij中元素的前两个字段表示有关LT S结构的静态信息。在整个算法运行过程中发生变化的数据是函数sig和ID。此外，工作者需要知道在当前和先前迭代中Si中状态的不同签名的数量，基于此决定是否已经达到最终分区。LT S以列表Inij，i = j和Outij，i = j的形式提供给工作器，后者使用恒定的初始ID函数：ID（x）= 0，其反映初始分区{S}。在每次迭代的第一阶段（步骤4），每个工作者计算其节点的签名。在第二阶段（步骤5、 5J，在图4和5中详细描述），所有签名被插入分布式哈希表中，并被分配唯一ID。插入基于散列函数hash：2 Act×NN，并且散列表的分布由函数wrk：N完成0 W1 .一、 我们假设wrk能够确保工作者的签名负载均衡WORKERi运行两个线程。其中一个忙着将每个签名发送给负责哈希表中应该插入签名的部分的工作者（使用wrk确定）。当所有的签名都被发送后，发送给所有的工人，标志着河流的结束另一个线程处理传入的消息。在本地哈希表中插入签名的请求（哈希插入）是通过查找签名并获取其ID来处理的，或者，如果没有找到，则将其添加到表中并为其分配新ID。然后将ID返回给签名的所有者当接收到对发送签名之前发送的请求的应答（哈希ID）时，Handle Messages将填充新的布洛姆和奥尔赞9我的天|⟨⟩}F−ID值并减少预期答案的计数器。最后，在接收到流结束消息（endsig）时，它会减少可能仍然发送哈希插入请求的工作线程的计数器。当所有工作线程宣布它们没有更多的签名要发送给i，并且所有i的请求都已被应答时，Handle Messages线程可能会在第二阶段之后，我们计算有多少不同的签名如果签名的数量没有增加w.r.t.在前一次迭代中，已经达到稳定分区，计算必须停止。在第三阶段（图6中详细描述的步骤6jj）中，列表Outij得到更新。对于LT S的每个转换，目的地状态的签名的新ID更准确地说，每workerj将ID（Inij）发送给workeri，worker i将在其Outij的最后字段上替换此信息。这是正确的，因为列表Inij和Outij具有相同的索引。在循环迭代结束时，IDs是简化的LT S和i，j的状态ID（x），a，px，a，p∈Outij是它的一组转换。 在最终将ID重新编号为连续的状态号之后，它们可以由工人独立地转储在实际的MPI实现中，发送签名中发送的消息的大小可能会因签名的不同而不同我们选择发送多个较小的消息而不是单个大消息，因为这样可以节省时间，尽管这需要程序员做更多的工作此外，通过手动划分消息，可以开始处理已经接收的部分，而消息的其余部分仍在接收中。为更新阶段（6J J），我们发出所有的发送消息和接收请求，然后等待所有的接收完成。来自步骤5J的两个线程利用显式交织来实现4.3分析我们现在证明上述算法是正确的，即。它终止并且它产生与输入LT S双相似的最小LT S。我们还分析了它的性能方面的时间，内存和计算过程中所需的消息数定理4.1（正确性）设S ∈（S，T，s0）是LT S.然后DSBR应用于S的任何分布终止，并且得到的ID满足：（{IDf（x）|x ∈ S}，{|<$x，a，y<$∈ T}，IDf（s0））是与S的最小LT S双相似。证明我们首先认为DSBR的每次迭代（步骤4和6 JJ）都会终止。为此，我们仔细研究涉及通信的步骤（5J，6和6JJ）。步骤5J的第一个线程显然会终止，因为它只执行有限数量的发送调用（总是成功的）。处理消息布洛姆和奥尔赞10∧DWWNNMN+N22退出条件（N活动工作者= 0N预期答案 = 0）将最终得到满足。当发送给i的W哈希ID消息将被接收到时，N活动工作器变为0。 注意，N个活动工作者为0是指向i的所有散列插入消息已经被接收的标志，并且还表明源自所有工作者（包括i本身）的所有散列插入消息都是“广播”的。特别地，这意味着当i的N个活跃工作者为0时，i的N个期望答案将不再增加。此属性排除了不希望出现的情况，即退出条件已满足，而i的消息仍处于挂起状态。计算分布计数的总和Wi=0时newcount i）是用一个MPI调用实现的。因此，我们可以假设这是正确的更新ID的终止主要是由固定数量的消息交换。每个worker成功地发送了W条消息（这些消息可能非常大，但这不是问题，因为我们假设了无限的信道），然后从网络中获取寻址到它的W通过归纳可以很容易地证明DSBR忠实地模仿了图2所示的顺序型SBR。 也就是说，形式上：对于任何r，如果我们认为IDs= SBRWORKERiIjIDd（x）=IDd（y）IDs（x）=IDs（y）.由此以及从DSBR和SBR的退出条件相同的事实，得出DSBR的步骤3最终终止。此外，由IDf值确定的LT S正是由SBR找到的LT S，因此我们的问题的解决方案。✷为了评估DSBR的性能，我们使用分布式算法的经典时间/消息复杂度度量，如[1]所定义。定理4.2（复杂度）在最坏的情况下，DSBR的时间复杂度是时间复杂度为O （n），时间复杂度为O（N）。为了计算签名，必须考虑每个状态，并且我们假设每个状态的成本与该状态的传出转换次数成线性关系。由于工人独立地进行计算，并且我们假设节点均匀分布，因此所需时间为O（M+N）。每个工作进程必须插入到全局哈希中的签名数table最多是它处理的状态数：[N|. 假设wrk是一个完美的哈希函数，每个工人都必须发送，西北，[W|每隔一个签名Wworker. 因此，每个工人最多只能得到W·、、、[W|W签名. （请参阅在本地哈希表中插入需要恒定的时间，以及计算时间。新的ID）。同样数量的回复必须发回。. 因此，成本计算签名的全局唯一标识符的方法是OW·[W|W（.布洛姆和奥尔赞11WOWWWWWWOOOON→−在他的命令下。在西方，我们可能会忘记一个b四舍五入了pards我们得到O W的成本。为了决定终止，我们需要计算不同签名的总数该操作的成本为W。为了交换新的ID，每个工作者必须准备总大小为（M）的W缓冲器，表示具有到其自己的状态的转换的状态的总数（在传入和传出转换均匀分布的假设它还必须接受和处理来自负责继承国的工人的这种总的来说，迭代的成本是O（M+N）。因为只要N由于可能需要迭代，计算复杂度为O（MN+N2）。消息复杂度由算法整个运行过程中所有工作进程发送的消息总数给出在最坏的情况下，交换签名需要N条消息（如果每个签名都必须发送给另一个签名worker），以及更新阶段W2消息。在步骤6处的同步总是需要W个消息。这导致在整个运行中最多N（N + W + W2）条消息，即O（N2+ NW2）。我们可以假设W与N相比是微不足道的，并得出消息复杂度为O（N2）。✷迭代次数是影响算法性能的最重要因素。最坏的情况是迭代次数就是状态数。具有这种最坏情况行为的示例是LT S，其状态为数字0. N，并且跃迁是i i + 1（i = 0. （N1））。然而，这样长的一系列事件在状态空间中并不典型状态空间中的典型现象是状态空间爆炸：系统将由P个进程组成，每个进程有N个并行运行的状态状态空间的大小将是NP，这对于相对较小的N和P来说是一个巨大的数字。然而，如果过程是完全独立的，那么约简算法最多需要N+1次迭代。当然，长线程或进程的完全独立性在实践中都不会发生，但它给出了一些直觉，说明为什么最坏的情况不太可能发生。一个工作者所需的内存可以估计如下：（M+N）用于签名信息，（M）用于传入转换的目的地ID/目的地状态，（M）用于传出转换的源状态/标签/目的地ID。总的来说，（M+N），这是我们可以实现的最好的，比单线程实现所使用的空间少W5实验我们已经写了两个顺序实现和一个分布式实现的天真算法。第一顺序实现忠实地遵循图2中的描述。第二个顺序实现标记不稳定块，并且仅计算不稳定块的签名如果一个块中的状态有一个到块的转换，则该块被标记为不稳定布洛姆和奥尔赞12表1问题大小。问题卡介苗明天真优化mem时间mem时间mem时间139419M18.5s14M6.2s21M3.3s缓存18M15.0s20M21.3s18M4.5s电梯5184M113s123M64s214M43s表2单线程强互模拟简化工具的比较那是分裂的分布式原型实现了图1中的算法3.第三章。我们已经在一个小问题集上测试了这些工具，该问题集包括火线链路层模型（[15]），缓存一致性协议（正在进行中）和具有5/6腿的分布式升降机系统（[10]）。这些问题是使用µCRL工具集进行的案例研究（[4]）。它们在减少之前和之后的尺寸可以在表1中找到在表2中，我们将单线程实现的内存使用和运行时间与bcg minreduction工具5的内存使用和运行时间进行了比较，bcg minreduction工具5是CADP工具集的一部分（[8]）。从该表中，我们得出结论，我们的顺序工具的性能与BCG min的性能相当。因此，使用朴素算法是可行的。为了测试分布式实现，我们使用了8节点双CPU PC集群和SGI Origin2000。6我们运行了三个系列的实验：在集群上，我们在1-8个节点上使用一个或两个CPU运行系列图7和8，我们显示所需的实际时间5这些测试在运行Linux的PC上运行，配备双AMD athlon MP1600+ CPU2G内存使用的bcg min版本为1.3。6集群节点为双AMD Athlon MP 1600+机器，每台2G内存运行Linux并通过千兆以太网连接。Origin 2000是一台ccNUMA机器，具有32个CPU和64 G内存，运行IRIX，其中我们使用1-16 MIPS R10 k处理器。在集群上，我们使用LAM/MPI 6.5.6（http://www.lam-mpi.org/）。在SGI上，我们使用原生MPI实现。问题原始减少国过渡国过渡13943.7 1056.4 1053.4 1047.6 104缓存2.1 1056.8 1057.7 1042.4 105电梯52.2 1068.7 1063.2 1041.4 105电梯63.4 1071.7 1081.2 1056.6 105布洛姆和奥尔赞13群 集 、 单 CPU/ 节 点 群集 、 双 CPU/ 节 点 群集、单线程SGISGI，单线程群集、单CPU/节点群集、双CPU/节点SGISGI，单线程图7. 5号电梯运行时间300 750250 625200 500150 375100 25050 1250 01 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16CPU图8. 6号电梯运行时间9000 225008000 200007000 175006000 150005000 125004000 100003000 75002000 50001000 25000 012345678910111213141516CPU减少状态空间。 因为集群处理器比SGI中的处理器快大约2.5倍，所以我们对不同的机器使用不同的规模。为了比较分布式工具和单线程工具，我们为单线程工具添加时间（群时间（群时间时间布洛姆和奥尔赞14我们还测量了SGI上的内存使用情况。lift 5问题在141 M中运行单线程，并在291- 385 M中分布。lift 6问题在2.7G中运行单线程，并分布在5.4G-5.5G中。由于这些内存需求，lift6分布式实现使用的内存是顺序版本的两倍，这一事实并不意外：所有签名的至少两个副本必须保留（本地副本和全局副本），ID信息使用缓冲器发送，其大小与转换次数成线性关系总的来说，我们可以看到lift5的性能然而，lift5仍然足够小，可以在一台机器上减少。对于更大的lift6问题，分布是必不可少的，运行时间可以很好地扩展，内存使用几乎可以完美地扩展在我们对lift6的实验中，我们发现降低LTS并不是唯一的问题。Linux 2.4内核中实现的ext 3文件系统不适合并行读取/写入多个大文件因此，从磁盘读取LTS实际上比减少它花费更多的时间。PVFS（[6]）将解决此问题问题.当前的实现可以在时间和存储器复杂度上都得到改进。算法中的三个阶段：计算签名、交换签名和交换分区信息现在是严格分开的。通过重叠这些阶段，我们可以摆脱用于交换分区信息的大传输缓冲器，以获得内存使用。由于处理器在交换阶段会显示一些空闲时间，因此我们也可以预期时间上的增益6结论我们采用了一种简单的强互模拟约简算法，并设计和分析了它的分布式版本我们实现了算法的顺序和分布式版本通过几个实验，我们表明，简单的算法的性能是相当不错的，分布式实现显示出一个体面的加速大的问题，理论分析预测分布式约简工具的实现可以通过几种方式来改进一个概念上的改进可能是应用在连续案件中证明有用的标记技术这将以使用更多内存为代价减少运行时间另一个值得注意的事实是，这三个阶段现在是按顺序执行的。通过重叠它们，我们可以获得运行时和内存使用的改进同时，我们使用一个随机哈希函数来分配状态。开发一个散列函数可能很有用，它可以最小化不同元素之间的边布洛姆和奥尔赞15P工人这将通过最小化通信来提高性能。进一步的工作还包括设计和实现一个工具，用于显示-贡献分支互模拟约简引用[1] Attiya ， H. 和 J. Welch ， “ 分 布 式 计 算 ： 基 础 、 模 拟 和 高 级 主 题 ” ，McGraw-Hill，1998年。[2] Balcazar，J.，Gabarro和M. Santha，判定双相似性是完全的，计算的形式方面4（1992），pp. 638-648[3] Behrmann，G.，T. Hune和F.分布式定时模型检测- 查询顺序如何重要，载于：Proceedings CAV[4] Blom，S.，W. Fokkink，J.Groote，I. Langevelde湾Lisser和J.v. d. Pol，µCRL：a toolset for analyzing algebraic specifications，in：Proc. 2001年（2001年），[5] Bollig ， B. ， M. Leucker 和 M.Weber ， Parallel model checking for thealternation freeµ-calculus，in：T.Margaria和W. Yi，编辑，第7届国际会议的工具和算法的建设和分析系统（TACAS543-558[6] Carns，P.H.，W. B. L. III河B.罗斯和R. Thakur，PVFS：A Parallel FileSystem For Linux Clusters ， in ： Proceedings of the 4th Annual LinuxShowcase and Conference，2000，pp.317-327[7] Fernandez，J.，一个有效的互模拟等价算法的实现，计算机编程科学13（1990），pp。219-236[8] Fernandez，J. C.的方法，H. Garavel，A. 克尔布拉特湖 穆尼耶河Mateescu和M. Sighireanu，CADP-协议四三七四四零[9] Garavel，H.，R. 马提斯库和我Smarandache，用于模型检测的并行状态空间，在：M。B. Dwyer，editor，Proceedings of the 8th International SPINWorkshop on Model Checking of Software SPIN'2001 ， LNCS 2057（2001），pp. 217-234[10] Groote ， J. ， J.Pang 和 A. Wouters， A Balancing Act ： Analyzing aDistributed LiftSystem，in：S. Gnesi和U. Ultes-Nitsche，编辑，第六届工业关键系统形式化方法国际研讨会，2001年，pp. 1-12号。[11] Grumberg，O.，T. Heyman和A.Schuster，分布式符号模型检验的μ-演算，在：G。贝里，H。Comon和A. Finkel，editors，Proceedings of the 13thConference on Computer-Aided Verification（CAV350-362.布洛姆和奥尔赞16[12] Kanellakis，P.和S. Smolka，Ccs表达式，有限状态过程和三个等价问题，在：第二届ACM分布式计算原理研讨会论文集，蒙特利尔，加拿大，1983年，pp. 228-240[13] Lerda，F.和R.Sisto，Distributed-Memory Model Checking with SPIN，in：Proc. 第五届国际SPIN研讨会，LNCS 1680（2000）。[14] Leucker，M.和T. Noll，Truth/SLC -并发系统的并行验证平台，在：G。贝里，H。Comon和A. Finkel，editors，Proceedings of the 13th Conference onComputer-Aided Verification（CAV255-259URLleucker_nollTruthSLC.ps.gz[15] Luttik，S.， P1394链路层的描述和正式规范，在：I. Lovrek，编辑，第二届系统设计应用形式化方法国际研讨会论文集，1997。[16] 佩奇河和R. Tarjan，Three partition refinement algorithms，SIAM Journal ofComputing16（1987），pp. 973-989.[17] 拉贾塞卡兰河，巴西-地和I.李，关系粗划分问题的并行算法，IEEE并行和分布式系统学报9（1998），pp.687-699.[18] Zhang ， S. 和 S. Smolka ， Towards efficient parallelization of equivalencechecking algorithms，in：Proceedings of FORTE133-146.