分布饱和状态空间中的推测射击预报模式识别方法

理论计算机科学电子笔记135（2006）65-80www.elsevier.com/locate/entcs分布饱和状态空间中推测射击预报的模式识别方法一代钟明英1及 Gianfranco Ciardo2University of California，Riverside，CA 92521摘要符号状态空间生成的饱和策略对全局异步局部同步系统特别有效。SaturationNOW是SaturationNOW的一个分布式版本，它使用工作站网络上可用的全部内存来有效地分散内存负载，但它的执行本质上是顺序的。为了实现真正的并行性，我们探索了一种推测性的并行性，其中真实的工作流将在预存的未来中运行，从而实现了一种推测性的并行性。一个新的方法，其中所有可能的火灾可能会探索一个先验，给定足够的空闲时间，可能会导致过多的内存需求。因此，我们引入了一种基于历史的方法来进行点火预测，该方法可以识别点火模式并仅探索符合这些模式的点火。实验表明，我们的启发式算法提高了运行时间，并具有较小的内存开销。关键词：状态空间生成，决策图，分布式系统，并行和分布式计算，推测计算，模式识别1介绍形式化验证技术，如模型检查[10]，在工业中被广泛用于质量保证，因为它们可以用于在生命周期的早期检测设计一个重要的步骤是一个详尽的，非常内存密集的状态空间生成。即使像二进制这样*部分由国家科学基金会（NSF）资助的工作，资助号为0219745。02039711 电子邮件地址：chung@cs.ucr.edu2电子邮件：ciardo@cs.ucr.edu1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.01966M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）虽然决策图（BDD）[2]有助于处理状态空间爆炸，但复杂系统的分析仍然可以求助于虚拟内存的使用。许多研究都集中在并行和分布式计算的应用。[1，20，25]使用工作站网络（NOW）进行显式状态空间探索或模型检查。[16]在共享内存多处理器上并行化BDD操作，而[21]使用分布式共享内存。[27]通过在共享和分布式共享存储平台上的香农扩展期间在处理器之间共享图像计算来并行化BDD构造[11]在广度优先的BDD遍历中发现并行性[13，17，26]通过将图像计算切片到NOW上来并行化BDD操作，其中主工作站平衡内存负载。在[4]中，我们提出了饱和算法的分布式版本[6]，称为SaturationNOW，用于在NOW上执行符号状态空间生成，其中执行是严格顺序的，但利用了整个NOW内存。与[23]一样，采用基于级别的水平此外，我们提出了一个启发式的动态平衡的内存负载，以帮助应付不断变化的峰值内存需求的每个工作站。然而，水平切片方案有两个缺点。首先，虽然它可以以最小的时间和空间开销均匀地分布决策图，但它并不促进并行性（它对应于工作站的顺序化，其中大多数计算需要工作站与其邻居合作）。其次，由于一组连续的决策图级别被分配给每个工作站，决策图级别很少的模型对方法的可扩展性施加了限制虽然将单个级别分配给多个工作站解决了这个问题，但额外同步的成本将消除我们的水平切片方案的主要在本文中，我们解决了第一个缺点，即，我们通过使用空闲工作站时间来规范性地触发决策图节点上的事件的想法来改进SaturationNOW的运行时，即使这些事件中的一些可能永远不需要。在一个简单的方法中，无限制的推测可能会导致内存消耗的过度增加，达到适得其反的程度。然而，基于历史的方法来预测哪些事件应该基于过去的触发模式被触发，而是有效地减少了运行时间，只有很小的内存开销。我们的论文组织如下。节2给出了可达性分析，决策图，克罗内克编码和饱和度的背景节3详细介绍了我们的朴素和模式识别方法，以投机性火灾预测。第4节显示了实验结果。第5节简要调查M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）67e∈Ei∈S第六节讨论了未来的研究方向。2背景一个离散状态模型是一个三元组（S^，s_int，N），其中S^是点集Bs_init∈S^为初始状态，N：S^→2S为初始状态。下一个状态函数，指定从单个步由于我们的目标是全局异步系统，因此我们将N分解为下一个状态函数的析取[15]：N（i）=Ne（i），其中E是有限的事件的集合，并且Ne是与事件e相关联的下一状态函数。可达空间S_S^是包含s_init且关于N是闭的集合：S={s_init}<$N（s_init）<$N（N（s_init））<$···=N<$（s_init），其中“<我们假设一个模型由K个子模型组成。因此，（全局）状态是K元组（i，K，.，i1），其中ik是子模型k的局部状态，K≥k≥1，S^=SK×·· ·× S1，K10个局部状态的交叉过程是随机的.所有这些都使用了针对利用系统结构，特别是符号结构的技术基于决策图存储状态空间的技术2.1状态空间S和下一状态函数 N虽然不是一个要求（局部状态空间Sk可以通过交错符号全局状态空间生成与显式局部状态空间生成[ 7 ]来“在线”生成然后我们使用映射Sk：Sk→ {0，1，.， nk−1}，withnk=|SK|，i确定locals tateik，其中索引xik=k（ik），其中Sk与h{0，1，.，nk-1}，并将一个新的集合X∈S^以一个关于S^的拟重定向多路判决诊断（MDD）进行编码。形式上，MDD是一个有向无环边标记的多重图，其中：• Eachnodepelongstoa水平{K，.， 1，0}，denotedp. LvL.• 在K层有一个根节点r。• 级别0只能包含两个终端节点零和一。• 一个在k> 0的节点p有nk条向外的边，标记为从0到nk−1。由ik标记的边指向k−1层的节点q;我们写为p[ik] =q。• 给定k层的节点p和q，如果对所有ik∈ Sk，p[ik] =q[ik]，则p=q。MDD编码一组状态B（r），由递归公式定义B（p）=K K{ik} ×B（p[ik]）如果p. lvl=k>1，B（p）={i1：p[i1]=On e}如果p. lvl=1。采用一种受马尔可夫研究启发的N的链[3]，我们假设一个Kronecker相容模型[5，6]，其中Ne被共轭分解为K个局部下一状态函数Nk，e，对于K≥k≥1，满足68M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）f ying（iK，.， i1）∈S^，Ne（iK，.， i1）=NK，e（iK）×···×N1，e（i1）. 通过定义K·|E|矩阵sNk，e∈{0，1}nk×nk，withNk，e[ik，jk]=1惠jk∈Nk，e（ik），weNe作为（布尔）克罗内克积：j∈ Ne（i）惠K≥1Nk，e[ik，jk] =1，其中，矩阵表示为S中的混合矩阵，并且注意，Nk，e矩阵是非常稀疏：对于标准Petri网，每行最多包含一个非零条目。2.2基于饱和度的迭代策略除了有效地表示N之外，Kronecker编码还允许我们识别和利用事件局部性[5]并使用饱和度[6]。我们说事件e与水平k无关，如果Nk，e=I，单位矩阵。LetTop（e）并且Bot（e）表示最高和最低水平，对于所述最高和最低水平，Nk，ei=1。节点p在水平k被称为是饱和的，如果它是一个关于所有Ne的固定点，则Top（e）≤k，即， B（p）=B（p）<$N≤k（B（p）），其中N≤k=e： Top（ e）≤ kNe.为了在节点p的所有后代都饱和时使节点p饱和，我们在适当的位置更新，使得它也对Nk，e× ··· ×N1，e（B（p））中的任何状态进行编码，对于任何事件e，使得Top（e）=k。这可以在低于k的级别上创建新节点，其在完成P的饱和之前立即饱和。如果我们从编码初始状态sinit并自底向上饱和其节点的MDD开始，则根r将在最后编码S=N（sinit），因为：(1)N<$（sinit）<$B（r）<${sinit}，因为我们只添加状态，并且只通过合法的事件触发，以及（2）B（r）<$N≤K（B（r））=N（B（r）），因为r是饱和的。换句话说，饱和度由许多“轻量级”嵌套的“局部”定点图像计算组成[6，7，8]中的结果一致表明，饱和度在记忆和时间上都大大优于呼吸第一次符号探索，使其成为全局异步局部同步离散事件系统的最有效状态空间因此，尝试并行化是有意义的，而并行化效率较低的广度优先方法不会带来巨大的加速和饱和内存减少。2.3饱和的例子图1显示了一个三位Petri网的可达图。每个全局状态由位置x、y和z的局部状态按此顺序描述，我们通过相应位置的标记数索引局部状态可达性图显示三个全局状态（0，1，1）、（0，0，2）和（0，2，0）从初始状态（1，0，0）可达Kronecker描述M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）69800 1 210900 1 2101000 1 21001234561 1 1 x> x>0000 10 100000 10 10 1 210101010Xa火灾d火灾Xb火灾XXc火y一Bzy一Bzy一Bzy一BzCDCDc火CDCDb火灾Fig. 1. 可达性图。a b c dXyz图二.下一状态函数N的克罗内克描述。700 1 21010012012012图三. 饱和示例（实心节点饱和，虚线节点不饱和）。的下一个状态函数是在图中所示二、例如，克罗内克描述的矩阵Ny，b表明，触发事件b将减少位置y中的令牌数量，从2减少到1，或者从1减少到0。然后，在该模型上基于饱和度的状态空间生成可以如下执行（参见图11）。3）。1 初始配置：设置初始全局状态（1，0，0）。2 在z层饱和节点：不需要进行点火，因为1 →0我我0 →10 →11 →02 →10 →11 →21 →00 →10 →11 →22 →11 →01 →070M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）120120101没有事件，Top（event）=z。 节点被定义饱和。3 在y级饱和节点0：Top（b）= Top（c）= y，但b和c在y和z两级都未启用，因此，不需要进行点火，节点因此饱和。4 在级别x饱和节点0：Top（a）= x，并且a对所有级别都启用，因此必须在节点上触发事件a。由于通过触发事件a，局部状态1对于级别y和z都是从0可达的，因此两个节点，级别y处的1和级别z处的2。这也意味着发现了新的全局状态（0，1，1）。5 在z层饱和节点：不需要进行点火，因为没有事件，Top（event）=z。再一次，节点被定义饱和。 6饱和节点1在级别y：Top（b）=y并且b对于所有级别都被启用，因此，必须在节点上触发事件B因为，通过触发事件B，0从级别y的1到达，本地状态2从级别y的1到达z，节点1在水平y处，和节点2在水平z上创建。这也意味着发现了一个新的全局状态（0，0，2）7 在z层饱和节点：不需要进行点火，因为没有事件，Top（event）=z。 再一次，节点被定义饱和。8 在级别y处饱和节点：Top（c）=y并且c对于所有级别被启用，因此，必须在节点上触发事件C。由于通过触发事件c，局部状态2可从级别y处的1到达，并且局部状态0可从级别y处的1到达，因此，z，节点在水平y处，和节点0在水平z，已创建和饱和之前，引用。这也意味着发现了一个新的全局状态（0，2，0）9 y层的饱和节点：由于所有可能的事件触发都已被完成后，节点饱和。10 在x层饱和节点：由于没有事件触发可以找到新的全局如果是这样，根节点就饱和了。2.4饱和度的分布式版本[4]提出了SaturationNOW，这是一种消息传递算法，它将状态空间分布在NOW上，以研究大型模型，其中单个工作站必须依赖虚拟内存。在具有W≤K个工作站的NOW上，从W到1，每个工作站w都有两个邻居：一个最初，我们将K个MDD级别相应 地 均 匀 分 配 给 W 个 工 作 站 ， 方 法 是 将 文 件 级 别 s[w·K/W] 到 [ （ w-1）·K/W]+1分配给w或k-0120101M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）710 10 122e23e50 1e0 11 280 10 10 12e40 20 10 120 0 1 200 1 21 200 1 21 20 22 1 2 2 1 2 0 1 2 1 2 0 11113mytop3=6w=3mybot=5mytop2=4w=2mybot2=3w=1mytop1=2mybot1=10 1 20 1 20 1 2见图4。 发射预期。西车站在每个工作站w中，局部变量mytopw和mybotw分别指示其拥有的最高和最低编号级别（mytopW=K，mybot1 = 1和mytopw ≥mybotw 对于任何W）。 我们强调，在这方面-贡献饱和度算法，我们使用一个簇来增加可用内存，而不是实现并行计算。每个工作站w首先为那些事件和水平生成克罗内克矩阵Nk，e，其中Nk，e/=I且mytopw≥k≥mybotw，没有任何同步。这是一个简化的事实，这些矩阵需要很少的空间，并且可以单独生成然后顺序饱和算法开始，除了当工作站w>1通常会发出递归调用到级别mybotw-1时，它必须改为发送请求以在工作站w-1中执行此操作并等待回复。工作站的线性组织是可行的，因为每个工作站只需要与它的邻居通信为了应对动态内存需求，[4]使用了嵌套方法重新分配MDD级别，即，改变两个邻居的mybotw和mytopw-1由于内存负载平衡请求可以传播，可以有效地依赖于整个NOW存储器，而不仅仅是它的邻居，而不需要全局同步或广播。利用我们的水平切片方案，即使水平到工作站的最佳静态分配也可能仍然不如良好但次优的动态方法。 这是因为，给定MDD级别的节点数量通常在执行期间急剧增加和减少工作站w可能正在使用在某个时间点，内存比wJ少得多，而反过来可能会发生通过在两者之间动态地重新分配级别，可以更好地满足高峰需求当然，这种重新分配并不违反规范，因为它保留了MDD结构。0 1 2 30 1 2 30 1 2 30 1 20 1 21 2 31 2 30 1 21 2 30 1 272M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）pQRpQR        图五. 基于历史的射击预测方法。3投机性火灾预测[4]的分布式方法有效地将内存负载划分到工作站上，但它是严格顺序的。我们现在探索一个空闲的工作站在先验的k级饱和节点p上触发Top（e）>k的事件e的想法，希望减少使p以上的节点饱和所需的时间。如第2节所解释的，如果任何Top（e）=k的事件e已经在p上被穷尽地触发，则k级的MDD节点p是饱和的。 然而，事件如果存在，则Top（e）=l> k≥Bot（e）的e仍然需要在p上发射路径（11，...，ik+1），使得e是“局部en-1”。“能够”，即， N1，e（i1）/=0，...，Nk+1，e（ik+1）≠.按要求的时间为了使这样的假设节点q饱和，我们的推测性预测创建了（可能断开的）MDD节点pJ，对应于在p上激发e的结果的饱和，并缓存结果。稍后，在p上执行e的任何操作都会立即返回在缓存中找到的结果pJ图4显示了工作中的投机性解雇预测在中间，工作站2和1预测并计算了e3和e5在第4级的触发，e8在第3级，e4在第2级（因此是断开的在右边，由于触发e3或e8而产生的节点现在连接起来了，因为它们实际上是需要的，并且在缓存中找到了：在这种情况下，推测性预测是有效的。我们强调MDD仍然是规范的，尽管有额外的断开连接的节点。此外，即使工作站w可能先验地知道该事件如果满足Top（e）>mytopw=k≥Bot（e）≥mybotw，则在节点p的k级上激发e仍然需要在下面的工作站w-1中进行计算，因为结果pJ必须饱和，导致工作在下面的级别上传播换句话说，由于事先不知道是否可以在本地计算事件触发的饱和度，因此连续的空闲工作站可能需要一起执行推测性事件触发3.1基于历史的推测性射击预测方法由于我们不知道在状态空间生成过程中事件e是否会在k级节点p上触发，因此最简单的推测性触发预测让空闲工作站彻底计算从“上面”开始的所有可能触发。           p qrM.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）73对于S的MDD的每个节点p，即，Eall（p）={e：Top（e）>k≥Bot（e）}。显然，只有当|E|相对于K是小的，因为，那么，在几个事件上用尽所有可能的触发相对便宜，从时间和空间的角度来看然而，对于大多数模型，这种方法引入了太多从未连接到状态空间MDD的节点。现在，我们根据射击模式进行更明智的预测。对于k层的每个节点p，设Epatt（p）是p饱和后将在p上触发的事件e的集合，因此Top（e）>k且Epatt（p）Eall（p）。我们可以然后根据它们的模式在级别k处划分节点，即，节点p和q在同一类中当且仅当Epatt（p）=Epatt（q）。不幸的是，Epatt（p）只是后验已知的，但应该注意到，大多数模型在饱和期间显示出清晰的点火模式，即，大多数类包含许多节点，并且大多数模式包含若干事件。我们的目标是仅基于到目前为止在p上发生的事件的历史来预测给定节点p的模式，Ehist（p）Epatt（p）。关键思想是，如果Ehist（p）= Ehist（q），我们可以推测Ehist（q）\Ehist（p）中的事件最终也需要在p上触发，即，Epatt（p）=Epatt（q），端图图5示出了一个示例，其中p、q和r是相同的饱和节点，MDD水平。图的中间图5示出了这些节点在运行时间期间的当前事件触发历史：Ehi st（p）={β，δ}，Ehi st（q）={α，β，γ，δ}，以及Eh i st（r）={γ}。图5的左侧显示了实际的事件触发历史在生成状态空间之后，即，它们的真实模式为：Epatt（p） ={α，β，δ}，Epatt（q） ={α，β，γ，δ}，和dEpatt（r） ={γ，δ}。 相反，应用我们基于历史的方法将导致图1右侧的火灾。5：由于Ehist（p）= Ehist（q）和Ehist（r）= Ehist（q），拥有此MDD级别的工作站将提前在p上触发β和γ，在q上触发α、β和δ，如果它是空闲的。因此，p上的γ和q上的α和β的无用激发将被推测性地计算（这些在图中用圆圈突出显示）。5）。当然，我们不想在预测中过于激进我们可以对几个不同的节点q有Ehist（p）<$Ehist（q），这些节点的历史除了Ehist（p）之外几乎没有公共元素如果，对于这些节点q中的每一个，我们在p上的Ehist（q）\ Ehist（p）中触发每个e，那么这些预测的触发中的许多可能是无用的，即，它们可能实际上没有被请求，因为e∈ Epatt（p）。上另一方面，任何基于历史的预测都保证在级别k处的节点的模式不相交的罕见情况：即，如果对任意两个p和q，eiterEpatt（p）=Epatt（q）或erEpatt（p）=Epatt（q）。3.2我们基于历史的方法除了有用之外，我们的启发式算法在内存和时间开销方面也需要便宜因此，我们的技术只使用了74M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）FirePredict（请求：堆栈，类：数组）whileRequests/=paddo（e，p）←Pop（Requests）;Enqueue（e，Ehist（p））;q←Class p. [e];如果Ehist（p）≠ Ehist（q），则p级。int[e] int n;对于每个eJ∈ Ehist（p）\ Ehist（q）do在q上触发eJ并缓存结果;否则如果Ehist（p）≠ Ehist（q），则对于每个eJ∈ Ehist（q）\ Ehist（p），在p上执行eJ并缓存结果;• 对于每个事件，• 记录事件触发历史• E代表节点• Ehist（p）是一个更好的模式• p成为新的代表• 用模式预测事件触发见图6。 射击预测算法。历史和一个有效的基于数组的预测方法，每次查找需要O（1）时间和O（K·|E|）内存整体。每个工作站都有：• 仅存储C（例如，10）Ehist的节点的最新元素• 保持一个列表Requestsw，其中包含满足的触发请求（e，p）。• 对于它拥有的MDD的每个级别k，使用大小为{e：Top（e）>k≥Bot（e）}的数组Classk一个元素Classk[e]是指向一个节点的指针，初始为null。通常，工作站w处于饱和模式：它计算发出请求（e，p）的结果，Top（e）> p。lvl=k，并且请求w中的记录（e，p）。当w变为空闲时，它就转到预测模式：它删除一个元素（e，p），将e添加到（截断的）历史Ehist（p），并检查k（e）类。如果Classk（e）=null，我们将Classk（e）设置为p;如果Classk（e）=q且Ehist（p）≠ Ehist（q），我们将Classk（e）设置为p，并且我们在q上推测性地触发Ehist（p）\Ehist（q）中的事件;如果Classk（e）=q且Ehist（p）≠ Ehist（q），我们保持Classk（e）不变，并且我们在p上推测性地触发Ehist（q）\Ehist（p）中的事件（参见图6）。为了最小化换句话说，我们使用类k（e）来预测到目前为止e被触发的所有节点中哪个节点具有这种启发式可以从“反演”中得到支持并且Ehist（p）<$Ehist（q）当e在p上被触发时，我们将Classk（e）设置为p;稍后，q的进一步触发可能导致Ehist（p）<$Ehist（q），但是Classk（e）将永远不会被设置为q，因为e在q上的触发已经在缓存中并且将永远不会被设置为q。再次请求。然而，这种启发式具有最小的簿记要求，特别是在饱和模式下，以及快速查找时间;其存储器要求也很低，因为空闲的工作站越多，请求w被清空的速度就越快，而k类和截断的历史在实践中使用的存储器比MDD的节点少第4节表明，这种启发式可以M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）75W时间（秒）总内存（MB）最大内存（MB）DISTRNAIVEHISTDISTRNAIVEHISTDISTR NAIVEHIST时隙环网协议N= 200 |= 8。|= 8. 38· 10211使用284MB在108秒内完成SEQ2119-24%−13%286+3%+45%197+1%+53%4139-27%−15%286+11%+51%127+61%+58%8182-32%-24%286+129%+62%69+239%+62%N= 300 |= 8。|= 8. 38·10 211SEQ 使用512MB无法在5小时内完成2s552s+5%s−5%962+25%+11%562+8%+7%4d490>5小时d-16%962-+34%352-+12%8564>5小时−39%962-+50%252-+23%柔性制造系统循环互斥协议N= 800 |= 1。|= 1. 20· 10196使用290MB在27秒内完成SEQ229+37%+6%293+110%+85%215+52%+63%436+33%+8%293+348%+109%130+186%+65%851+33%+5%293+807%+148%73+433%+73%N= 1100 |= 3。|= 3. 36· 10334使用 512MB2D65s+62%s+18%794+46%+6%379+79% +30%447S+131%d+10%794+119%+38%265+104%+40%856d+164%+7%794+299%+50%173+126%+38%跑道安全监控器表1实验结果。减少大型模型的运行时间。最后，我们观察到我们的方法可以放松：如果我们在p上发射e，类k（e）=q，并且Ehist（q）<${f}<$Ehist（p）但f/∈ Ehist（q），我们仍然可以决定在p上投机地发射Ehist（q）\ Ehist（p）;然而，这种咄咄逼人的做法往往导致太多无用的开火。4实验结果我们在SMARTNW[4]中实现了一个简单的Ch，这是我们的工具S m A r T[9]的基于MPICH的分布式版本我们通过使用饱和度来评估其性能N= 300 |= 3。|= 3. 64· 1027使用241MB在55秒内完成SEQ279−8%−8%243+12%+24%121+26%+52%491d+67%−9%243+102%+30%119+205%+50%8260-−30%243-+42%103-+47%N= 450 |= 6。|= 6. 90· 1029使用 512MB，2S257s+12%S−14%826+16%+5%512+15%+7%4d311>5小时d-18%826-+33%372-+6%8959>5小时−25%826-+61%343-+6%Z= 2|= 1。|= 1. 51· 1015使用314MB在236秒内完成SEQ2731>10小时−2%332-+39%191-+48%4938>10小时−8%332-+88%190-+30%81480>10小时-22%332-+128%173-+13%Z= 3 |= 5。|= 5. 07· 1015使用 512MB，2S11280>10小时s−1%962-+10%595-+16%76M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）生成后续模型的状态空间• 时隙环网络协议[22]模拟了一种用于局域网的协议，其中N是网络内的节点数量（K = N，|SK| = 10对于所有k，|E| =3N）。• 柔性制造系统（Flexible Manufacturing System）[18]是一个制造系统模型，它有三台机器来处理三种不同类型的零件，其中N是每种类型的部件的数量（K = 19，|SK|= N + 1对于所有k，除了|= 4时，|的12 |= 3和|S 7 |= 2时，|E| = 20）。|= 20).• 循环互斥协议[12]模拟了互斥算法的循环版本，其中N是涉及的处理器数量（K=N + 1，|SK| = 10对于所有k，除了|S1|= N + 1，|E| =5N）。• 跑道安全监控器[24]模拟了一个航空电子系统，用于监控X ×Y ×Z跑道上S速度的T个目标（K = 5（T +1），|S5+5i|= 3时，|S4+5i|= 14，|=1+ X（10+6（S −1）），|S2 +5i| =1+ Y（10+6（S −1）），|S1+ 5i| =1+ Z（10+ 6（S-1）），对于i =0，...，|= 1+ Z (10+ 6(S−1)),for i = 0,..., T，除了|S4+5T|= 7，|E|= 49 + T（56+（Y − 2）（31+（X − 2）（13 + 4 Z））+3（X − 2）（1 +Y Z）+2 X +5 Y +3 Z））。我们运行我们的实现在这四个模型上使用一个集群的奔腾IV 3GHz的工作站，每个与512 MB的RAM，连接千兆以太网和运行Red-Hat 9.0 Linux与MPI 2的TCP/IP。表1显示了W个工作站的运行时间、总内存需求以及W个工作站的最大和原始的SMARTNOW（DISTR），并且P eeentagechangew. r. t.DISTRforthenaévé（NAéIVE），andthehistory-baseds（HIST）speculativeferingpre-referred-dictions;尽管前两个模型具有不同的特征（开槽环具有固定大小的节点和K级和事件数|E|在参数N中是线性的; FMS的节点大小在N和固定K中是线性的，|E|），均显示模式识别方法提高了DISTR的运行时间，随着W的增加，运行时间增加了39%。实际上，当W= 2时，对于N = 200的开槽环，NA-IVE和HIST甚至比SEQ更快此外，使用HIST，触发预测是非常有效的：大多数情况下，只探索有用的触发模式，导致内存需求适度增加。然而，NAIVE工作仅在存在可用内存的情况下才有效，例如，开槽环，N=200。然而，即使这样，增加工作站W的数量也可能是适得其反的，因为这增加了它们的性能。闲置时间，导致他们追求过度的投机性融资。这反过来又会使缓存和节点内存不堪重负，并触发昂贵的M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）77动态内存负载平衡甚至内存交换，最终将计算速度降低到低于DISTR的水平，就像N= 300时的情况一样。此外，当W增加时，负载最大的工作站的内存需求应该减少，因为额外的工作站应该共享整个内存负载。这适用于DISTR和HIST，但不适用于NAIVE。这是FMS的最好证据。循环互斥是我们方法的一个最坏情况的例子，因为不存在有用的事件触发模式。我们提出它是为了公平，但也是为了强调我们的HIST方法的弹性。虽然记忆和时间的纳伊夫E在-由于它探索了许多无用的投机性触发，HIST的触发只略有增加，这表明HIST由于缺乏触发模式而无法提供帮助，至少在开销方面没有太大的影响最后，RSM是美国国家航空航天局（NASA）[24]正在开发的一个真实系统，K= 15，太接近W，我们的水平切片方案无法很好地工作SEQ的结果确实比任何分布式版本都要好，但只有在SEQ可以运行的情况下。当SEQ由于过多的内存需求而失败时，DISTR和HIST仍然可以为第二组参数运行。在这种情况下，我们的HIST启发式算法以最小的额外内存开销减少了运行时间，事件触发模式存在于现实模型中。5NOW上的符号状态空间生成大多数关于符号状态空间生成的并行或分布式工作采用垂直切片方案，通过以呼吸优先方式分解布尔函数并将计算分布在NOW上来并行化BDD操作[14，17，26]。这允许算法重叠图像计算。然而，如果切片选择很差，则会创建大量额外的节点，并且通常认为找到一个好的切片并不是微不足道的[19]。因此，需要一些同步来最小化冗余工作，这会降低此方法的可伸缩性。[13]建议采用主处理器来管理用于负载平衡目的的作业队列，并通过根据使用变量的最佳选择的布尔函数进行切片来减少图像计算中的冗余，以便最小化所需的决策图节点的峰值数量，从而最小化工作站之间的最大工作负荷。然而，没有报告加速。相反，[4，23]将决策图水平地划分到一个NOW上，这样每个工作站都独占一个连续的决策图级别范围。由于分布式图像计算根本不会产生任何冗余工作，因此避免了同步。另外，通过水平切片78M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）SSSS1S2S3见图7。垂直切片与水平切片与射击预测。阴谋只需要对等通信，因此可伸缩性不再是问题。然而，为了保持分布式决策图的规范性，分布式计算是顺序化的，这意味着没有容易的加速机会事实上，我们用于事件触发预测的模式识别方法在保留水平切片方案的同时克服了这一限制然而，就像垂直切片引入的冗余工作一样，我们的方法引入了一些无用的工作。更准确地说，即使MDD保持规范，也可以生成其他断开连接的MDD节点图图7显示了这两种方法之间的差异，其中实心框表示状态空间，阴影框表示无用的MDD。当然，垂直切片方法可以重新排序MDD变量以改善节点分布，但变量重新排序操作是昂贵的，需要大量的同步。相反，在我们的方法中，每个工作站可以在运行时清理断开的MDD节点，而不需要任何同步。因此，我们的方法不会损害可扩展性，这是水平切片方案的优点之一我们的方法并没有实现一个明确的加速方面的最佳顺序实现。然而，至少，它打开了可能性，加快符号状态空间生成的NOW结合水平决策图切片计划。6结论我们提出了一种模式识别方法来指导事件触发的推测计算，并使用它来提高状态空间生成的分布式饱和算法实验表明，在饱和期间在运行时识别事件触发模式在一些模型上是有效的，包括NASA正在开发的现实系统。我们设想了几种可能的扩展。首先，虽然我们的想法是实现饱和式迭代，但它也适用于（分布式）CTL模型检查中所需的更简单的广度优先迭代第二、M.- Y. 钟湾，澳-地Ciardo/Electronic Notes in Theoretical Computer Science 135（2006）79在展示了推测性点火预测的潜力之后，我们计划探索更复杂但仍然是低开销的方法，其改进预测事件的有用性，同时在许多工作站空闲时在预测中更积极。最后，我们的算法应该被扩充，以包括关于当前内存消耗的信息。7确认我们要感谢拉杜·西米尼恰努和克里斯蒂安·谢尔顿对预测方法的讨论，以及裁判们的有益建议。引用[1] A. Bell和B.哈弗科特Petri网的顺序和分布式模型检验。STTT，7（1）：43[2] R.布莱恩特基于图的布尔函数操作算法。IEEE Trans. Comp. ，35（8）：677[3] P. Buchholz，G. Ciardo，S.多纳泰利和P.肯珀。 记忆高效克罗内克运算的复杂性及其在马尔可夫模型解中的应用。INFORMS J. Comp. ，12（3）：203[4] M.- Y. Chung和G. Ciardo.现在饱和。Proc.QEST，第272 -281页[5] G.Ciardo ， G.Luéettgen 和 R.我 是 你 的 儿 子 。 异 步 系 统 的 异 步 异 步 并 行 中 断 。Proc.ICATPN，第103 -122页[6] G. Ciardo，G. Luéttgen和R.我是你的儿子。 S aturn at ion：用于符号状态空间生成的一种新的逻辑结构。Proc. TACAS，第328 -342页[7] G.恰尔多河Marmorstein和R.西米尼恰努饱和度解除。Proc.TACAS，第379 - 393页[8] G. Ciardo和R.西米尼恰努异步系统的结构符号CTL模型检验。Proc.CAV，第40 -53页[9] G.恰尔多河琼斯，A. Miner和R.西米尼恰努使用SMART进行逻辑和随机建模。业绩评价，出现。[10] E. Clarke，O. Grumberg和D.佩尔德。模型检查。1999年[11] S.盖，M。Rebaudengo和M.桑扎·雷奥达布尔函数操作的数据并行算法。FMPSC，第28 -36页，1995年[12] S. 格拉夫湾 Steen，and G. Luéttgen. 使用接口规范的财务系统的组