《分布式时间自动机可达性分析及性能优化研究》

《理论计算机科学电子札记》68卷第4期（2002年）网址：http://www.elsevier.nl/locate/entcs/volume68.html17页分布式时间自动机可达性分析Gerd Behrmann1丹麦奥尔堡大学计算机科学系摘要我们实验评估现有的分布式可达性算法的时间自动机在Linux Beowulf集群。 发现该算法存在负载均衡问题和较高的通信开销。负载平衡问题是由包含检查之间的符号状态唯一的时间自动机可达性算法。我们建议增加一个比例负载平衡控制器的算法之上。我们评估各种方法，以减少通信开销，增加本地化和减少消息的数量。这两种方法都可以提高性能，但会使负载平衡变得更加困难，并且会产生不必要的副作用，导致工作负载增加1引言在过去的5年里，人们对并行和分布式模型检测的兴趣有所增加。这并不是说它解决了固有的性能问题（状态爆炸问题），而是通过购买额外的处理单元来实现线性加速的承诺吸引了客户和研究人员。UPPAAL[3]是一个流行的稠密时间时间自动机模型检测工具该工具的设计目标之一是，正交功能应该以正交的方式实现，以便可以比较竞争技术。UPPAAL[4]的分布式版本的设计又基于分布式版本或Murpal [19]的设计，确实符合这一想法，并允许分布式版本利用几乎任何以前在工具中实现的现有技术。[4]中提出的分布式算法得到了非常积极的结果，但主要是在提供非常快速和低开销通信的并行平台 在分布式体系结构（Beowulf clus-ter）上的实验是初步的，不确定的。后来在另一个贝奥武夫1电子邮件：behrmann@cs.auc.dk2002年由ElsevierScienceB. V.操作访问根据C CB Y-NC-N D许可证进行。贝尔曼2集群表现出相当差的性能，即使在调整实现，我们也只能得到相对较差的加速，如图所示1.一、更仔细的检查发现了负载平衡问题和非常高的通信开销。我们还发现，虽然UPPAAL中的大多数选项与分布正交，但它们对分布式算法的性能有至关重要的影响特别是[17]的状态空间缩减技术另一方面，最近数据结构的变化[10]也对分布式版本产生了非常积极的影响加速：noload-bWCap14131211109876543211 2 4 6 8 10 12 14节点Fig. 1.用非优化的分布式可达性算法对一些模型进行加速。贡献我们分析了分布式版本的性能在一个14节点Linux Beowulf集群。分析表明，意外的负载平衡，ING问题和高通信开销。 我们贡献了在[4，19]中先前使用的现有随机负载平衡之上添加额外负载平衡层的结果。 我们还评估了使用替代分布函数和缓冲通信的效果。相关工作所使用的分布式状态空间探索算法的基本思想已经在许多相关领域中进行了研究，例如离散时间和连续时间马尔可夫链、Petri网、随机Petri网、显式状态空间搜索等[8，1，9，15，16，19]，尽管替代方法正在出现[5，12]。在大多数情况下，接近线性加速和非常好的负载平衡总线耦合器3dacapo_simfischer 6IRmodel3加速比贝尔曼3→→→∈ ×→δ时间自动机的分布式可达性分析的工作很少。虽然非常类似于所提到的显式状态空间枚举算法，但经典的时间自动机可达性算法使用符号状态（不要与符号模型检查的工作混淆，其中转换关系用符号表示），这使得算法对探索顺序非常敏感。纲要第2节总结了时间自动机的定义，时间自动机的符号语义，[4]中提出的时间自动机的分布式可达性算法，并介绍了本文其余部分中使用的基本定义和实验设置 在第3节中，我们讨论了算法的负载平衡问题。 在第4节中，提出了通过增加局部性来减少通信的技术，在第5节中，我们讨论了缓冲区对算法性能的影响，特别是对提出的负载平衡技术的影响。2预赛在本节中，我们总结了时间自动机的基本定义、符号语义、分布式可达性算法和实验设置。定义2.1（时间自动机）设C是时钟的集合。 设B（C）是形式为x da c和x − yda c的简单条件下的合取集，其中x，y ∈ C且da∈ {<，≤，=，≥，>}。C上的时间自动机是一个元组（L，l0，E，g，r，I），其中L是一组位置，l0∈ L是初始位置，E L L是一组边，g：E B（C）为边分配保护，r：E 2 C为边分配要重置的时钟，I：L B（C）为位置分配不变量。直观地说，时间自动机是一个用非负实值时钟的条件和重置注释的图时钟赋值是从时钟集合到非负实数的函数u：CR≥0设RC是所有时钟估值的集合。我们跳过具体语义，支持基于RC中称为区域的凸多面体的精确有限状态抽象（区域可以是由B（C）中的连词表示这种抽象导致了下面的符号语义。定义2.2（符号TA语义）设Z0=x，y∈Cx=y是初始区 时间自动机（L，l0，E，g，r，I）的符号语义定义C上的一个转移系统（S，s0，n），其中S=L×B（C）是符号状态集，s0=（l0，Z0<$I（l0））是初始状态，n ={（s，u）∈S×S|t：setδu}：是变换r，并且：• （l，Z）<$（l，norm（M，（Z<$I（l））↑<$I（l）贝尔曼4e{|∈ }联系我们|∈}×→{|{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy110}通过A=等待A={（l0，Z0<$I（l0））|h（l0）= A}当结束时，（l，Z）=waitingA.popState（）如果n（l，Y）∈通过A：Z/n ∈Y，则<$（lJ，ZJ）：（l，Z）<$（lJ，ZJ）do通过A=通过A{（l，Z）}d=h（lJ，ZJ）如果<$（lJ，YJ）∈waitingd：ZJ/<$YJ则endif多内恩迪夫做等待d=等待d<${（lJ，ZJ）}• （l，Z）<$（lJ，re（g（e）<$Z<$I（l））<$I（lJ））如果e=（l，lJ）∈E.其中Z↑=u +duZdR≥0 （未来运算），并且re（Z）= [r（e）0]uuZ。 函数norm：NB（C）B（C）将时钟约束相对于定时时钟的最大常数M归一化。自动机注意，符号语义的状态（l，Z）实际上是一组具体的状态（l，u）u Z。区域的经典表示是差分边界矩阵（DBM）。有关时间自动机的更多细节，请参见例如[2，7]。符号语义可以扩展到通信时间自动机（导致使用位置向量代替位置）和具有数据变量的时间自动机（导致添加变量向量）的网络该算法给定符号语义，构造可达性算法是简单的该算法的分布式版本如图所示（2）见（4）。该算法的两个主要数据结构是等待列表和传递列表。前者包含所有未探索的可达状态，后者包含所有已探索的可达状态。状态从等待列表中弹出，并与传递列表中的状态进行比较，以查看它们以前是否已被如果没有，它们将被添加到已通过列表中，所有后继者将被添加到等待列表中。图二.分布式时间自动机可达性算法在节点A上参数化。等待列表和传递列表使用函数h在节点上划分。状态从本地等待列表弹出并添加到本地通过列表。后继者被映射到目的地节点d。贝尔曼5→⇒传递列表和等待列表使用分布函数在节点上划分。分布函数可以是简单的散列函数。重要的是要注意，由于使用了符号状态，在等待列表或传递列表中查找状态涉及到找到状态的超集。哈希表用于快速找到列表中的候选状态这也是为什么分布函数只依赖于状态的离散部分的原因定义2.3（节点，分布函数）图中的一个例子。 2称为节点。所有节点的集合被称为N。 分布函数是从位置集合到节点集合的映射h：L N。定义2.4（生成节点，拥有节点）状态（l，Z）的拥有节点是h（l），其中h是分布函数。如果存在（lJ，ZJ）s. t，则节点A是状态（l，Z）的生成节点.（lJ，ZJ）（l，Z）和h（lJ）= A.终止众所周知，符号语义导致有限数量的可达符号状态。因此，在某个点上，每个生成的后继者（l，Z）将被包括在传递A的n∈N中，或者更准确地说，被包括在传递h（l）中，原因与连续的情况相同。终止是一个检测当所有节点变为空闲并且没有状态处于被发送的过程中时存在用于执行分布式终止检测的公知算法我们在[11]中使用基于令牌的算法的简化版本过渡状态在[17]中描述了一种同样适用于顺序和分布式算法的常见优化这个想法是，并不是所有的状态都需要存储在传递列表中以确保终止。我们称这种状态为瞬态。瞬态倾向于减少算法的存储器消耗在第4节中，我们将描述瞬态如何增加局域性。搜索顺序之前对分布式算法的评估[4]表明，由于遗漏的包含检查和非确定性通信模式导致的非广度优先搜索顺序，分布式可能会增加生成状态的数量人们发现，这个效应可以通过根据与初始状态的距离对等待列表中的状态进行排序来减少，从而近似于广度优先搜索顺序。对于本文进行的实验也是如此，因此使用了这种排序。贝尔曼6××平台我们之前的实验是在配备24个CPU的Sun Enterprise 10000并行计算机上完成的2本文的实验是在一个集群上进行的，该集群由7台双733MHzPentium III机器组成，每台机器配备2GB内存，与Linux内核2.4.18相兼容，并通过交换式快速以太网连接它仍然使用消息传递接口3的非阻塞通信原语，但许多MPI相关的性能问题已经得到修复。实验使用六个现有模型进行实验：众所周知的FischerDACAPO模型非常小（可达状态空间在几秒钟内构建）。总线耦合器的模型是最大的，并且具有几百万个状态的可达状态空间在1、2、4、6、8、10、12和14个节点上测量分布式算法的性能实验通过名称和节点的数量来引用，例如。Fischer 6 8在8个节点上进行实验在所有实验中，生成了完整的可达状态空间，并且两个列表中的每个列表的总哈希表大小保持不变，以避免这两个数据结构的效率取决于节点的数量（在[4]中没有这样请注意，图1是在实现本文中描述的技术之前使用较旧版本的UPPAAL生成的从那时起，UPPAAL变得相当快，因此通信开销变得相对较高。3平衡分布式可达性算法使用随机负载平衡来确保均匀的工作负载分布。这种方法在具有快速互连的并行机器上工作得很好[4，19]，但是如在介绍中所提到的，当在集群上运行时，结果非常差图3显示了采用与图1相同算法的总线耦合器3 2的负载在本节中，我们将研究为什么负载不平衡以及如何解决这个问题。定义3.1（负载、传输速率、探测速率）负载2该论文还报告了对一个小的、集群3我们使用的LAM/MPI实现可以在www.example.com上http://www.lam-mpi.org。贝尔曼7×负载：noload-bWCap，总线耦合器3，2个节点800007000060000500004000030000200001000000 20 40 60 80 100 120 140 160 180 200时间（秒）图三.对于未优化的分布式可达性算法，总线耦合器3 2的负载随时间的变化。表示为load（A）的节点A的等待列表的长度，即，负载（A）=|瓦特A|.节点的传输速率是状态被传输到其他节点的速率。 我们区分传出和传入的传输速率。 探索率是状态从等待列表中弹出的速率。注意，等待列表的插入时间不为O（1）。哈希表中的冲突可能导致线性时间插入（节点负载的冲突是可以预料的，因为几个状态可能共享相同的位置向量，从而哈希到同一个桶因此，探测速率取决于节点的负载和传入传输速率。显然，正在发生的事情如下。由于通信延迟和其他随机效应，预计负载会出现小的差异。如果节点A上的负载比节点B稍微高一些，那么在等待列表中插入状态所花费的时间就会更多，因此A的探索率就会下降。当这种情况发生时，A的传出传输速率下降，导致B的探索速率增加，这反过来又增加了A的传入传输速率。因此，A和B的负载的微小差异会导致差异增加，从而导致一个不稳定的系统，其中一个或多个节点的负载迅速下降到零。虽然节点仍然从其他节点接收状态，但由于以下几个原因，具有不平衡的系统是不好的：首先，这意味着节点在某些时间是空闲的，其次，它阻止了在等待列表上成功进行包含检查。事实证明，后者对于良好的性能非常重要我们采用两种策略来解决这个问题。第一种方法是将等待列表中的哈希表与将传递的列表转换为一个统一的哈希表。这一变化是最近负载（状态）贝尔曼8一记录在[10]中。这倾向于减少负载对探索速率的影响，因为通过列表比等待列表大得多。对于大多数模型，系统平衡的影响是积极的，尽管Fischer 6仍然显示出不平衡的迹象，见图4。425000负载：noload-bWCap，总线耦合器3，2个节点14000负载：noload-bWCap，fischer 6，2个节点12000200001000015000800010000600040005000200000 10 20 30 40 50 60 7080时间（秒）(a) 母线耦合器3 ×200 10 20 30 40 50 60时间（秒）(b) fischer 6 ×2见图4。统一传递列表和等待列表的哈希表可以解决某些模型的负载平衡问题（a），但不能解决其他模型的负载平衡问题（b）。第二种策略是在随机负载平衡之上添加显式负载平衡方案这个想法是，只要系统是平衡的，随机负载平衡就能正常工作。希望显式负载平衡器可以在不引起两个太多开销的情况下保持为每个后继者调用负载均衡器它决定是否将状态发送到其所属节点或将其重定向到另一个节点。重定向的效果是状态被存储在错误的节点上，这会降低效率，因为某些状态可能会被探索多次。我们将应用一个简单的比例控制器来决定是否应该重定向一个状态。该控制器的设定点将是系统的当前平均负载请注意，重定向它的是生成状态的节点，而不是所属节点本身。因此，状态只被转移一次。关于节点负载的信息与状态一起捎带。定义3. 2（Loadaveragouge，Rdirectionprobabiliy）年龄定义为平均载荷=1|N|A∈N 负载（A）。一个国家的概率是重定向到节点B而不是拥有节点A是PA→B=P1·P2，其中：P1=A B如果load（A）−loadavg≤0，如果load（A）−loadavg≥c，则为1load（A）−loadavgC否则4仅显示了2个节点的设置的负载，以减少图中的混乱。 当运行所有14个节点时，结果是相似的，但在一个小图中解释起来要困难得多。负载（状态）负载（状态）贝尔曼9一B一×一ΣP2=0 max（loadavg−load（A），0）max（loadavg−load（B），0）B∈N1是节点A所拥有的状态被重定向的概率，是它被重定向到节点B的概率。请注意，如果A的负载低于平均值，则P1为零（我们不从负载不足的节点获取状态如果B的负载高于平均值，则P2为零（我们不重定向状态B2-1到过载节点），并且A∈NPA= 1，因此B∈NPA→B=PA。的值C确定负载平衡器的积极性。 如果a节点高于平均值C个以上的状态，则该节点所拥有的所有状态将被重定向。此时，我们让c=loadavg。两个小的增加减少了负载平衡的开销。首先是引入死区，即，如果实际负载和负载平均值之间的差异第二个是，如果后继者的生成节点和拥有节点是相同的，那么状态将不会被重定向。后者倾向于减少通信开销，但也减少了负载均衡器的积极性实验表明，除了Fischer 6之外，比例控制器可以使大型系统的负载几乎完全平衡。图5（a）显示了负载均衡器在保持Fischer 6平衡方面的困难（尽管它比没有它的情况下更平衡），但仍然可以提高加速，如图5所示。5（b）.800070006000500040003000200010000负载：load-bWCap，fischer 6，2个节点平均平衡0 10 20 30 40 5060时间（秒）(a) Fischer 6 ×2的负载加速：load-bWCap14131211109876543211 2 4 6 8 10 12 14节点(b) 加速比图五.显式负载平衡的增加对系统的平衡有积极的影响。(a)显示Fischer 6 2的负载和每个节点每秒重定向的平均状态数，（b）显示获得的加速比。总线耦合器3dacapo_simfischer 6IRmodel3负载（状态）加速比P贝尔曼104局部性上一节所述的结果并不令人满意。即使负载平衡，获得的加速比也约为线性的50%。问题是节点之间的通信引起的开销。在本节中，我们评估两种通过增加局部性来减少通信开销的方法。(a)（b）第（1）款见图6。给定数量的节点使用的总CPU时间分为用户空间/内核空间（左列）或接收/发送/将状态打包到缓冲器/非mpi相关操作（右列）所花费的时间。图（a）显示了带负载平衡的总线耦合器3的时间，图（b）显示了不带负载平衡的Fischer 6的时间由于所有通信都是异步的，因此验证算法对通信延迟具有相对鲁棒性原则上，延迟的唯一后果应该是负载信息稍微过时，并且宽度优先搜索顺序的近似值不太准确。另一方面，消息传递库、网络堆栈、存储器和网络接口之间传输的数据以及由到达的数据触发的中断图6（a）显示了总线耦合器3系统中所有节点使用的总CPU时间。CPU时间显示在两列中：左边分为用户空间和内核空间的时间，右边分为发送，接收，将数据打包到缓冲器和从缓冲器中取出的时间，以及剩余时间（非mpi）。可以看出，与不同机器上的节点之间的通信相比，同一机器上的两个节点之间的通信开销较低（比较1，2和4个节点的列对于4个节点和更多节点，我们看到了显著的通信开销，但实际验证（非mpi）所花费的时间也显著增加在1和2个节点之间看到的增加可能是由于两个节点共享贝尔曼11nn2nn这台机器的内存总线。UPPAAL是非常内存密集型的，共享存储器总线将导致开销。在2到4个节点之间看到的增加可能是由于通信引起的中断数量增加通信开销与传输的状态数量直接相关。假设n = |N|是节点的数量，m是位于单个物理机器上的节点的数量，并且S是生成的状态的总数。如果所有的机器都执行相同的工作量，我们希望每台机器节点生成Sstates. 假设分布函数分布状态一致，我们期望每个节点发送S状态到任何其他节点（包括自己）。对于任何给定的节点，在同一台机器上有m-1个其他节点，在其他机器上有n-m个节点。设tlocal是向位于同一台机器上的节点发送状态的开销，tremote是向另一台机器上的节点发送状态的开销。然后，我们得到以下通信表达式间接费用：Sth=nn2（tlocal（m−1）+tremote（n−m））（1）图6显示了th+tv（理论值），其中tv是实际验证所用的时间（非mpi）。两个常数tlocal和tremote是根据2和4个节点上的测量开销计算的th的定义假设传输状态的开销是恒定的，这不一定是这种情况，例如当带宽要求高于可用带宽或负载不平衡时，使得节点执行阻塞接收。图6（b）显示了Fischer 6的不平衡验证，并且用于阻止接收呼叫的时间很长。因此，预测的通信开销不太精确。值得注意的是，计算开销往往低于实际开销。这表明，随着节点数量的增加，发送状态的成本变得更高，这是由于网络上的负载增加或MPI实现中的开销（后者是更可能的解释）。减少状态转移量的一种方法是选择一个分布函数，该函数在保持平衡的同时增加生成节点也是拥有节点的换句话说，分布函数应该增加局部性。定义4.1（局部性）分布函数的局部性l是生成节点拥有的状态数相对于生成的状态总数S的关系。在（1）中，我们假设分布函数的局部性为1。一个好的分布函数具有高的局部性，同时保持负载均匀分布，即每个节点探索S结局部性为1，这是不期望的，因为它阻止了任何负载平衡。假设所有的非局部状态都是均匀分布的，我们得到下面的负载表达式贝尔曼12nn间接费用：t（l）=n1−l S（t（m−1）+t（n-m））n−1nS−L当地远程（二）=n−1（tlocal（m−1）+tremote（n−m））其中1−lSn−1n 是每个节点发送到任何其他节点的状态数（例如，包括自身），L是生成节点所拥有的状态的总数很容易看出t（1）= th。一般来说，很难构造保证具有高局部性同时保持良好负载分布的分布函数对于具有大量整数变量的输入模型，一个很好的启发式方法是只根据变量向量计算拥有节点。由于不是所有的转换都更新整数变量，这往往会增加后继节点被生成它的节点所拥有的机会图7（a）显示了作为节点数量的函数的结果局部性比较一下1本地-通过对位置向量和变量向量进行散列而获得的值图7（b）显示了总线耦合器3的CPU时间。将其与Fig进行比较。图6（a）显示通信开销显著减少。局部性：load-local-bWCapD 110.950.90.850.80.750.70.650.60.550.51 2 4 6 8 10 12 14节点(a)地点（b）总线耦合器3见图7。基于整数向量的只分配状态的效果。 我们没有包括Fischer 6，因为它只包含一个整数。另一种增加局部性的方法是在局部探索所有的瞬态无论如何，瞬态不会存储在传递列表中，因此仍然保证终止。图8（a）显示了仅将提交的5个状态标记为瞬态所获得的加速。 图8（b）使用[17]的技术来5提交位置的概念是对时间自动机的一个UPPAAL扩展。提交的位置用于创建过渡的原子序列一个国家承诺是否有任何一个地点被占用总线耦合器3dacapo_simIR模型3当地探索的国家贝尔曼13dacapo_simfischer 6IR模型3当地探索的国家n通过将所有非循环入口点标记为瞬态来增加瞬态的数量这两种方法都增加了局部性，但实验表明，使用后一种技术实际上会降低性能。不向拥有节点发送瞬态可能会导致显著的开销，因为这些状态不再能被拥有节点的等待列表合并。使用[17]的技术将瞬态的数量提高到一定程度，其中等待列表执行的合并比通信引起的开销更重要。本地化：local-bWCap1本地化：local-bWCapS 210.9 0.950.8 0.90.7 0.850.6 0.80.5 0.750.4 0.70.3 0.650.2 0.60.1 0.5501 2 4 6 8 10 1214节点0.51 246 8 10 12 14节点(a) 只有提交的状态是暂时的。(b) 所有非循环入口点都是暂时的.见图8。增加局部性的另一种方法是局部地探索所有瞬态。注意Fischer 6没有提交状态，因此图（a）中这个模型的局部性是1。5布赫林在上一节中，我们试图通过减少节点之间需要传输的状态数量来减少通信量众所周知，通信开销可以通过将几个状态放入每个消息中来减少事实上，前面几节中的结果是用8的缓冲器大小获得的，即，每个MPI消息包含8个状态。在本节中，我们将研究缓冲对负载平衡算法的影响。图9显示了发送前缓冲状态的效果。仅显示Fischer 6 ×14和总线耦合器3×14的结果可以看出，随着缓冲器大小增加，加速比增加，直到加速比再次降低的每个缓冲器20到24个状态的大小似乎是最佳的。有人可能想知道为什么当进一步增加缓冲器大小有几种解释。增加缓冲器dacapo_simfischer 6IR模型3当地探索的国家贝尔曼141210母线耦合器3-bWCap-负载母线耦合器3- bWCap -空载母线耦合器3-bWCapD 1-负载母线耦合器3-bWCapD 1-空载fischer 6- bWCap -负载fischer6 -bWCap-noload8642010 20 30 40 50 60 70 80 90 100缓冲区大小见图9。当在一条消息中存储和发送更多的状态时，所获得的加速比会增加。20到24个州的规模似乎是最佳的。显示了有和没有负载平衡的结果。对于总线耦合器3，还显示了仅基于可变向量分配状态的结果（bWCapD1选项）。增加了系统中的延迟。这反过来又使负载信息过时，并延迟负载平衡决策的效果比较图中母联3 ×14的负载当使用缓冲器大小1和缓冲器大小96时，图10说明了这一点，因为后者的平衡性要差得多，重定向的状态的平均数量要高得多，这又增加了生成的状态的数量另一个因素与广度优先搜索顺序的近似值有关如果延迟增加，则近似将不太精确。这反过来可能会增加探索的符号状态的数量，因为成功的包含检查较少最后，当一个状态被buffered时，它不能与其他状态合并（这只发生在拥有节点上），这反过来可能会增加探索的状态数量。生成的状态数量的增加如图所示十一岁6结论本文给出了在Beowulf Linux集群上对用于UPPAAL的时间自动机分布式可达性分析算法实验表明，非恒定时间操作在探索算法中这些平衡问题被证明可以通过使用算法中使用的传递列表和等待列表数据结构的统一表示以及添加额外的负载平衡层来减少或解决（取决于输入模型）。即使在一个加速比贝尔曼15平均平衡×3000负载：load-local-bWCap.B1，总线耦合器3，14个节点4500负载：load-local-bWCap.B96，总线耦合器3，14个节点2500400035002000 30001500250020001000 1500100050050000 10 20 30 40 5060时间（秒）00 5 10 15 20 25 30时间（秒）(a) Unbu加密（b）每条消息见图10。使用无缓冲器（a）和缓冲器大小为96个状态（b）加载总线耦合器314。增加缓冲器的大小会使系统变得不平衡，从而导致显著的开销。2.42.221.81.61.41.210.8010 20 30 40 50 60 70 80 90 100缓冲区大小见图11。由大缓冲器导致的增加的延迟和不平衡导致生成的状态的数量增加。相对于由算法的顺序版本生成的状态的数量平衡系统，MPI over TCP/IP over Fast Ethernet的通信开销这种开销可以通过使用仅在状态的子集上进行散列的替代分布函数来减少，从而增加算法中的局部性。此外，缓冲通信在减少通信开销方面是有效的，但是以增加的延迟为代价，这又降低了负载平衡和搜索顺序的有效性平均平衡母线耦合器3-bWCap-负载母线耦合器3- bWCap -空载母线耦合器3-bWCapD 1-负载母线耦合器3-bWCapD 1-空载Fischer 6-bWCap -负载fischer6 -bWCap-noload负载（状态）状态（相对于1个节点）负载（状态）贝尔曼16在[4]中引入了启发式。对于进一步的工作，我们计划研究替代比例控制器中使用的负载均衡器，例如，使用PI控制器或PID控制器。通信开销可以通过使用多线程设计来进一步减少在我们的集群上，这将有效地将负载平衡和通信问题减少到7个节点，而不是14个节点。最后，应该评估在TCP/IP上使用MPI的替代方案，例如直接访问以太网设备。引用[1] S. Allmaier，S. Dalibor和D.克赖舍共享和分布式内存机器的并行图生成算法。并行计算：基础，应用和新方向，会议论文集ParCoElsevier，Holland1997.[2] R. Alzheimer和D. L.迪尔时间自动机理论。理论计算机科学，126：183[3] 放大图片作者：John Bengtsson，Pedro R. D’Argenio, Alexandre Hune，BertrandJeannet ， KimLarsen ， OliverMüoler ， PaulPettersson ，CarstenWeise，，anddWan g Yi. UPPAAL- 现在，下一个，和未来。在MOVEPSpringer-Verlag，2001.[4] Gerd Behrmann，Thomas Hune，and Frits Vaandrager. 分布式定时模型检查-搜索顺序如何重要。第12届计算机辅助验证国际会议论文集，计算机科学讲义，芝加哥，2000年7月。史普林格出版社[5] S. Ben-David，T.Heyman，O. Grumberg和A.舒斯特可扩展的分布式在线符号模型检查。2000年11月，第三届计算机辅助设计形式化方法国际会议[6] 约翰·本特森。减少计时系统符号状态空间探索的记忆体使用。《2001-009年技术报告》，乌普萨拉大学信息技术系，2001年5月。[7] Patricia Bouyer，Catherine Dufourd，Emmanuel Fleury，and Antoine Petit.时间自动机是可更新的吗？在Proceedings of the 12th Int. Conf. on Computer AidedVerification，卷1855的Lecture Notes in Computer Science。Springer-Verlag，2000.[8] S. Caselli，G. Conte，and P. Marenzoni. gspn模型的并行状态空间探索。在应用和理论的Petri网，卷935的讲义在计算机科学。Springer-Verlag，1995.贝尔曼17[9] G. Ciardo，J.Gluckman，andD. 妮可离散状态随机模型的分布式状态空间生成。INFORMS Jounal on Computing，10（1）：82-93，1998.[10] Alexandre David，Gerd Behrmann，Wang Yi，and Kim G.拉森乌帕尔的下一代。提交给RTTOOLS 2002。[11] E. W. Dijkstra和C. S.斯科尔滕使用计算进行冲突的终止检测。InformationProcessing Letters，11（1）：1[12] O. Grumberg，T. Heyman和A.舒斯特μ演算的分布式模型检验。在计算机辅助验证国际会议（CAVSpringer-Verlag，2001年7月。[13] K. Havelund，K.Larsen和A.Skou. 功率控制器的正式验证使用实时模型检查器UPPAAL。在Joost-Pieter Katoen，编辑，实时和概率系统的形式化方法，第5届国际AMAST研讨会，ARTSSpringer-Verlag，1999.[14] K. Havelund，A. Skou，K. G. Larsen和K.隆德音频/视频协议的形式化建模和分析：使用UPPAAL的工业案例研究。第18届IEEE实时系统研讨会论文集，第2-13页，1997年12月。美国加利福尼亚州旧金山[15] B. R. Haverkort，A. Bell和H.C.博嫩坎普从随机petri网高效顺序和分布式生成极大马尔可夫链第八届国际Petri网和性能模型研讨会论文集PNPMIEEEComputer Society Press，1999.[16] W. J.Knottenbelt和P.G.哈里森大型马尔可夫模型的分布式磁盘求解技术在第三届马尔可夫链NSMC'99数值解国际会议的会议记录萨拉戈萨大学[17] 放大图片作者：Kim G. Larsen，Paul Pettersson，and Wang Yi.实时系统的有效验证：紧凑的数据结构和状态空间缩减。 在proc 第18届IEEE实时系统研讨会，第14-24页。IEEE Computer Society Press，December 1997.[18] H. LonnanddP. Petttersson. 用于TDMA预编译备份机制的验证。 在proc 环太平洋国际集团（Paci fic Rim Int.）Symp. 《容错系统》，第235-242页，1997年12月。[19] 联合Stern和D. L.迪尔使穆尔河的水化。Orna Grumberg，编辑，计算机辅助验证，第9届国际会议，LNCS第1254卷，第256-67页。Springer-Verlag，1997年6月。6月22日至25日，以色列海法。