状态空间的分布偏序约化

理论计算机科学电子笔记128（2005）63-74www.elsevier.com/locate/entcs状态空间的分布偏序约化1L. 布里姆岛切埃纳山口Moravec，J.圣门沙捷克共和国布尔诺马萨里克大学信息学院摘要状态空间爆炸是并发系统形式化验证的一个根本障碍。在过去的几年里，出现了一些解决这个问题的技术，其中我们感兴趣的两个是：偏序约简和分布式存储器状态探索。第一种方法试图将问题缩小到一个更小的问题，而另一种方法则试图扩展计算能力来解决同一问题。在本文中，我们考虑这两种方法的组合，并提出了一个分布式存储算法的偏序约简。保留字：分布式模型检测，偏序约简，LTL模型检测1介绍并发系统是由能够并发协作并相互通信的系统组成的。由于组件之间所有可能的相互作用以及它们之间可能出现的许多竞争条件导致的组合爆炸，并发系统通常表现出非常大量的不同行为。基于状态空间探索的模型检测是一种常见的技术，用于确定系统的所有可能行为都与给定属性兼容。它包括探索表示所有系统组件的组合行为的状态图（状态空间）对于有限状态系统，可以详尽地探索该图。该技术的主要限制是状态1 捷克共和国资助机构资助的研究。201/03/05092Email：{brim，cerna，xmo ra vec，x si msa}@ fi. 穆尼岛cz1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.10.01964L. Brim等人理论计算机科学电子笔记128（2005）63可以随着系统描述的大小呈指数增长的图（状态空间爆炸）。几种方法被用来克服状态空间爆炸。本文研究了其中两种方法的结合：半降阶方法和分布式方法。部分降阶方法的目的是减少需要搜索的状态空间的大小。它利用了这样一个事实，即探索并发事件的所有交织可能不是检查属性所必需的，因此它最适合于异步系统。该方法包括构造一个简化的状态空间;完整的状态空间，这可能是太大，以适应一个内存，从来没有构造。这加快了状态空间的构建，使用更少的内存，并导致更有效的模型检查。以缩减状态空间为例的行为形成完整状态空间的行为的子集，然而，它们的口吃不变性质仍然有效。非正式地，口吃不变性意味着如果序列中的状态重复有限次，则无限状态序列上的属性的真值不会改变。我们考虑线性时间时态逻辑LTL的公式表示的属性。将可以用LTL表示的属性限制为断续不变属性的一种简单方法是不允许使用next运算符（LTLX）。该方法有几个成就，更多细节见[12，19，21]。我们的算法所基于的方法在第2节中进行了总结。分布式方法通过将状态空间分布在网络中的多个工作站之间来应对状态爆炸，目的是通过将强大的并行计算机构建为工作站网络（集群）来增加计算能力（特别是随机存取存储器）工作站通过消息传递接口进行通信，并在相互合作中探索整个状态空间。人们对构建分布式验证工具（例如，[1、2、3、5、6、10、22]）。在[4，13，14]中，已经考虑了符号模型检查和分布的组合一个自然的问题是如何结合偏序方法与enumerative分布，从而允许在分布式设置中构造简化的状态空间。在[15]和[17]中提出了两种结合方法的方法我们在论文中提出的方法可以理解为两者的推广并行化背后的基本思想是将缩减状态空间的生成划分为可以以任意顺序并行执行的独立子任务。这是通过将搜索堆栈分割成由完全扩展的状态确定的部分来实现的。该方法在第3节中描述。第4节总结了我们所做的实验L. Brim等人理论计算机科学电子笔记128（2005）63652部分降阶方法在这一节中，我们主要根据[9]的介绍，对部分降阶方法作一个简要的回顾。我们所使用的并发系统分析被建模为状态转换系统（标记转换系统）。如果S是状态的集合，则跃迁是关系α<$S×S，即， 它可以在不同的状态对之间进行。一个状态转移系统被定义为一个元组M=（S，s0，n，L），其中s0∈S是一个初始状态，n是一个转移集合α<$S×S，L：S→2AP是一个标记函数，它为每个状态分配一个原子命题集合AP的子集。在状态si中允许转移α∈ {\displaystyle\alpha}，并且存在状态sJ使得α（s，sJ）。在状态s中启用的所有转换的集合被表示为启用（s）。我们假定过渡是确定性的，即，对于每个α和s，至多有一个SJ满足α（s，SJ），记为α（s）=SJ。如果α（s，SJ），我们说SJ是s的后继。正如在介绍中所提到的，偏序方法开发了可以同时执行并以任意顺序交错的转换。这可以通过定义可以并发执行的转换对的独立关系来形式化。定义2.1独立关系I×是一个对称的反自相关关系，对于每个状态s∈S和每个（α，β）∈I，满足以下两个条件：(i) Enabledness – If(ii) 交换性依赖关系是I的补语。找出异步系统的给定模型的最小可能依赖关系的问题与可达性问题一样困难因此，启发式方法被用于根据上述条件高效地计算依赖关系独立关系表明，通过从源自状态s的独立转移中仅选择一个，可以对状态转移系统进行潜在的还原。然而，这不能保证简化状态转换系统是完整状态转换系统的正确替代，因为它没有考虑要检查的属性。此外，消除中间状态α（s）或β（s）之一可能会导致其某些后继状态（对验证很重要）无法探索。还需要用于还原的正确性的附加条件，并且它们将在下文中描述首先，我们通过定义过渡的可见性66L. Brim等人理论计算机科学电子笔记128（2005）63定义2.2如果对于每一对状态s，sJ∈S使得α（s，sJ），L（s）<$APJ=L（sJ）<$APJ成立，则跃迁α∈ <$对于一组命题APJ <$AP j是不可见的。如果变换不是不可见的，则它是可见的集合APJ通常由包含在已验证公式中的原子命题的集合导出。简化的状态转换系统，由MR表示，由修改的生成算法生成，该算法仅探索转换的子集，称为样本集，在生成期间遇到的每个状态下启用。样本集可以用一种不依赖于状态转移系统由一组与完整状态转移系统和相应的简化状态转移系统相关的条件生成的注意，对于一个给定的状态，可能有不止一个样本集满足条件。 我们说，只要empty（s）=enabled（s），状态s就完全展开定义2.3设APJ是一组原子命题。 充足的条件相对于集合APJ的是：C0样本（s）= C0 i启用（s）= C0。C1沿着完整状态图M中从s开始的每条路径，以下条件成立：如果没有首先发生的样本转换，则不能执行依赖于样本转换的转换。C2如果enabled（s）/=ample（s），则每个α∈ample（s）对于w.r.t.是不可见的。 到APJ.C3（循环关闭条件）如果简化状态图MR中的循环包含某个转换α被启用的状态，则该循环是不允许的，但该状态从不包含在该循环上的任何状态s的样本这些条件刻画了生成满足安全性和活性检验要求的简化状态转移系统所需的充分集。特别地，所生成的所得到的简化的状态转换系统被保证为与完整的系统是断续的等价的，并且因此所有的LTLX性质被保留。定理2.4设M=（S，s0，ε R，L）是一个状态转移系统，MR=（SR，s0，ε R，L）是一个约化的状态转移系统，满足关于一组原子命题AP j的充分条件C0，C1，C2和C3.设λ是LTL X在AP J上的公式。 则M满足，当且仅当MR满足。因此，给定的LTLX公式在给定的系统M中是否满足的问题可以归结为在简化的系统MR中是否满足的问题。L. Brim等人理论计算机科学电子笔记128（2005）63673约简状态空间对于分布式计算，我们假设一个没有全局内存的协作节点（工作站，计算机）节点之间的通信在分布式计算中，状态转移系统被划分为多个部分，每个节点一个部分我们的目标是设计一个分布式内存算法来计算减少的状态转移系统。简化系统由生成算法计算，该算法系统地探索状态，每个状态S，它选择一组样本（S），该样本（S）被启用（S），并且仅遵循来自样本（S）的这种算法的关键部分是没有任何怀疑充分条件的分布式检查。虽然检查条件C0和C2很容易，可以在本地完成，但检查条件C1和C3与解决可达性问题一样困难。条件C1可以使用与序列情况相同的近似解析法进行局部检查（参见[9]）。循环关闭条件C3是在分布式环境中唯一难以检查的条件。在使用深度优先搜索探索状态图时的顺序情况下，使用搜索堆栈在恒定时间检查条件C3。事实上，下面的更强的条件被用来代替C3。如果状态s未完全展开，则样本中没有转换导致搜索堆栈上的状态。我们的目标是开发条件C3J的对应部分，用于基于深度优先搜索生成分布在多个节点之间的状态转移系统在分布式设置中以相同的效率检查原始条件C3J因此，我们建议使用一个更合适的条件.新条件的动机是观察到在深度优先搜索期间，仅需要搜索堆栈的一部分以确保条件C3J。特别是，搜索堆栈的重要部分是堆栈顶部和已完全展开的最顶部状态之间的部分。这是因为在一个状态被完全展开后，通过搜索堆栈到达该状态的所有循环都将该状态作为一个完全展开的状态。基于这个简单的观察，我们可以将约简（生成）过程拆分为独立的子任务。每次一个状态被完全展开时，我们就用一个空的搜索堆栈开始一个新的搜索。这特别适合于分布式，因为我们不需要关心在节点之间传输搜索堆栈。多个子任务可以在不同的节点上并行为了处理总而言之，我们使用以下循环关闭条件。68L. Brim等人理论计算机科学电子笔记128（2005）63如果状态s未完全扩展，则样本中没有转变导致 本地搜索堆栈上的状态也不属于不同节点所拥有的状态如上所述，我们假设状态转换系统（实际上只有状态）被划分到几个节点上。分区函数表示为owner（）。初始状态s0的所有者表示为manager。分布式算法的主要思想如下。每个节点保持一组等待状态，从该等待状态开始生成简化状态转移系统。管理器通过从初始状态开始第一个深度优先搜索过程来启动整个计算。每当访问一个新的状态s时，计算一组转换的可扩展性。我们总是试图选择一个满足充分条件的集合;特别是在C3JJ的情况下，它不包括通向搜索堆栈或另一个节点的过渡。如果我们不成功，当前状态将完全扩展。有两种可能的情况。在状态s被完全扩展的情况下，状态s的每个后继sJ都被插入到等待集合中。如果所有者（sJ）与所有者（s）不一致，则向sJ的所有者发送消息以这样做。深度优先搜索然后从状态s回溯。否则，深度优先搜索在仅从样本深度优先搜索结束后，所有传入的消息都将被处理。然后从等待集合中挑选一个状态，并从它开始一个新的深度优先搜索。重复这个步骤，直到等待集合为空。 一旦集合等待为空并且没有传入消息，节点就开始空闲。如果所有节点都空闲并且没有未决消息，则算法终止。注意，状态s在没有样本时完全展开，使得没有从样本指向不同节点的转换。一般来说，这并不是真正必要的。当穿越到另一个节点时完全扩展的主要原因是处理然而，这样的循环至少两次通过同一个节点在下文中，我们描述了两个简单的算法，以减少完全展开的次数，同时确保满足条件C3J。第一个启发式算法对所涉及的节点进行排序。如果不可能选择一个样本，使得没有从样本指向严格大于所有者的不同节点的转换，则状态被完全扩展。第二个启发式算法涉及更多，可以给出更好的约简。它在每次深度优先搜索期间跟踪访问过的节点。为此，我们将每个深度优先搜索与布尔值的数组历史相关联。的L. Brim等人理论计算机科学电子笔记128（2005）6369数组的长度是固定的，等于所涉及的节点数。数组历史的第i个元素为真当且仅当搜索访问了节点i所拥有的某个状态。当根据以下条件计算状态s的集合样本时，考虑阵列历史如果状态s未完全展开，则样本中没有转换导致本地搜索堆栈上的状态，也没有转换导致不同节点所拥有的状态，使得当前搜索已经访问了该节点。同样，有两种可能的情况。在样本是使能样本的真子集的情况下，深度优先搜索在从样本的转换之后在状态转换系统生成中继续，如下所示：• 对于指向状态sJ的每个转换，使得所有者（sJ）与所有者（s）不同，我们创建数组历史的复制历史J，其中我们设置历史J[所有者（s）] =true，并向sJ的所有者发送包含元组（sJ，historyJ）的消息。• 然后，深度优先搜索从s开始，只考虑指向状态sJ的转换，使得s和sJ具有相同的所有者。 如果状态sJ已被访问，并且对于其历史sJhistory和对于所有索引i，隐含history[i]和sJhistory[i]都是有效的，则状态被认为是已访问的。否则，深度优先搜索进入状态sJ，并且sJ与历史（如果之前没有访问过）或与历史历史sJhistory一起存储。第二种情况是充足=启用，即， s已完全扩展。 在这种情况下，状态s的每个后继sJ都被插入到集合中，等待与数组空历史一起（对于每个节点i，空历史[i]=false）。如果所有者（sJ）与所有者（s）不一致，则向sJ的所有者发送消息以这样做。深度优先搜索然后从状态s回溯。该算法的伪代码（包括所描述的函数visited（s，history）返回true当且仅当状态s已经被访问，并且数组history没有关于在状态s之前被搜索访问的节点的新信息（对于所有索引i，隐含history[i]和history[i]是有效的）。命题3.1算法终止，简化的状态转移系统满足条件C0、C1、C2和C3。这个命题是从上述论点得出的。正确性的形式证明在技术上是相当复杂的，我们跳过它。至于时间和空间的复杂性，我们评估的复杂性相对于一个单独的节点。设n是分配给节点的状态数，e out是来自分配给节点的状态的边数，70L. Brim等人理论计算机科学电子笔记128（2005）63procMain（）/* 对于节点i */ifi=managerthenwaiting.push（s0，emptyhistory）;finally<$finisheddoreturn（）;whilewaiting/=dopublicintfindDuplicate（）;如果<$visited（state，history），则Dfs（state，history）;return（）;od奥德恩德procDfs（state，history）/* 对于节点i */if（state）=enabled（state）然后foreacht∈sample（state）do如果所有者（t（状态））=ithen if<$visited（t（state），history）push（t（state），emptyhistory）;filelsesend（owner（t（state）），（t（state），empty history））;其他菲奥德foreacht∈ample（state）doifowner（t（state））=ithen if<$visited（t（state），history）然后Dfs（state，history）;elsesend（owner（t（state）），（t（state），historyJ））;菲奥德芬恩德Fig. 1. 分布式算法并且e是边的数量，使得它们的端点是分配给节点的状态。时间复杂度是O（n + e out + e in），而时间复杂度是O（n + e out + e in）。使用“历史”启发式的计算复杂度为O（P）。（n + e_out + e_in）），其中P是参与简化状态转换系统生成的节点的数量。空间复杂度分别为O（n）和O（P.n）。证据没有启发式的计算只探索一次每个状态及其所有出来的边。此外，传入的消息必须保持，这需要时间O（e in）。在这种情况下，启发式是em-每一次探索一个国家的历史，已经改变了。由于历史单调增加，重新探索的次数最多为P。在这两个版本中，访问状态的数量（以及它们的历史）决定了空间复杂度。L. Brim等人理论计算机科学电子笔记128（2005）63714实验我们已经实现了分布式算法与实现已经完成了在C++和实验已经进行了13个英特尔奔腾4 2.6 GHz的工作站与1 GB的RAM每个与一个快速的100 Mbps以太网互连的在实现中，状态转换系统使用随机散列函数在工作站之间划分，因为这保证了均匀分布。一旦系统被分区，就不执行重新平衡。我们进行了几次测试，以评估减少的潜力和可扩展性的算法。我们考虑了四组模型。第一组由对应于Peterson算法的模型组成，互斥问题由进程的数目n（表示为PA（n））参数化第二组由对应于由进程数n（TRA（n））参数化的令牌环算法的模型组成。的第三组由对应于交替比特协议的模型组成，该协议由在一行中可能丢失的比特数n（ABP（n））参数化。最后，第四组由对应于简单发送器-接收器协议的模型组成，该简单发送器-接收器协议由一行中可能丢失的比特数n（SRP（n））参数化。对LTL X公式GF（P）中的原子命题进行了状态转移系统的约化。cs）表示进程P将无限次进入其临界区（对于PA（n）和TRA（n））和GF（Receiver. 接收器。（1）表达接收器将无限次接收某个值（对于ABP（n））和SRP（n））。模型充分自旋比FDFS比美国（4）2239099147058865.7百分比（%）144939764.8百分比（%）中国（15）14745591167· 10− 5%1167· 10− 5%中文（简体）31457271243 .第三章。9· 10− 5%1243 .第三章。9· 10− 5%ABP（11）1965620122648362.4百分比（%）107380354.7百分比（%）ABP（12）2302468143330162.3百分比（%）125698754.6百分比（%）中文（简体）1687102133250379.0百分比（%）124669373.9百分比（%）中文（简体）1814110143794979.3百分比（%）134636574.2百分比（%）图二. 减少连续实验的结果如图2所示。我们比较了完全状态转移系统（Full）的可达状态数与缩减状态转移系统的大小。使用深度优先搜索过程生成减少的状态转换系统，其中状态72L. Brim等人理论计算机科学电子笔记128（2005）63每当从样本点到搜索堆栈的转换时，s该算法被广泛使用，由于它是在SPIN模型检查器中实现的，因此我们将其称为SPIN。然后使用我们的算法FDFS（碎片深度优先搜索的缩写）生成约简状态转移系统。性能比较1601401201008060402004 6 8 10 12多个工作站图三. 分布式环境我们的算法在分布式环境中使用“历史”启发式的实际性能它的性能进行了比较与分布式算法产生的完整的状态转移系统。为了生成ABP（20）和SRP（50）（分别为5954564和6007102个状态）的完整状态转换系统，至少需要三个工作站。减少率（分别为54.5%和73.8%）与节点数无关，图中仅显示了节点数与计算时间的关系。实验结果表明，该算法的降阶比确实优于采用保守的循环闭合条件得到的降阶比。同时，分布式计算中的算法具有很好的可扩展性，并且比分布式可达性算法需要更少的时间。ABP（20）满ABP（20）还原SRP（50）全SRP（50）还原时间L. Brim等人理论计算机科学电子笔记128（2005）63735相关工作和结论Lerda和Sisto（[15]）首次尝试将这些方法结合起来，他们用部分降阶来增强分布式SPIN模型检查器。该算法只允许可达性检查，并使用保守的循环关闭条件（在计算它们的节点之外保持的后继总是假设当前在搜索堆栈中在[17，18]中，提出了分布式算法TwoPhase。与SPIN的算法相比只要没有满足充分条件的单例，状态就完全扩展。在生成单例样本集时，计算不跨越不同的节点，从而可以局部地检查循环闭合条件。在并行环境中，该算法只实现了可达性检查。与这两种方法相比，我们提出的算法不仅考虑了单例充分集，而且使用了保守性较小的循环闭合条件，从而提高了约简同时，当生成缩减状态空间时，用于生成缩减状态空间的算法可以容易地与分布式LTL模型检查算法[7，8，1]结合，同时检查关于给定LTL属性的正确性。然而，到目前为止，我们只实验测试了我们的算法的可扩展性和约简效率，并测试其效率在完整的LTL模型检测是一个未来的工作。引用[1] 巴纳特湖Brim，and J. Chaloupka.并行广度-第一搜索LTL模型检查。第18届IEEE自动化软件工程国际会议（ASEIEEE计算机协会，10月。2003年。[2] G. Behrmann，T. S. Hune和F. W. 凡德拉格 分布式定时模型检查-搜索顺序如何重要。第12届计算机辅助验证国际会议（CAVSpringer-Verlag，2000.[3] A. Bell和B. R.哈弗科特Petri网规范的顺序和分布式模型检验。在Proceedings of the 1stInternational Workshop on Parallel and Distributed Model-Checking （ PDMCElsevierScience Publishers，2002.[4] S. Ben-David，T. Heyman，O. Grumberg和A.舒斯特可扩展的分布式在线符号模型检查。在Warren A. 小 亨 特 和 史 蒂 芬 D 。 Johnson ， editors ， Proceedings of the 3rd InternationalConference on Formal Methods in Computer-Aided Design（FMCADSpringer-Verlag，2000.[5] S. Blom和S.奥赞状态空间强互模拟约简的分布式算法。国际软工具技术转让杂志，2004年。[6] B. Bollig，M. Leucker和M.韦伯无交替μ-演算的并行模型检验。在第七届国际会议的工具和算法，74L. Brim等人理论计算机科学电子笔记128（2005）63系统的构造和分析（TACASSpringer-Verlag，2001.[7] L. 布林岛 Cern'a，P. 克雷奇阿尔河。 Pel'an ek.基于负循环检测的分布式LTL模块化第21届软件技术和理论计算机科学基础会议论文集Springer-Verlag，2001.[8] I.Cern'aandR.Pel'an ek.Distributedexplicitfai r cydete 在 Proceedings of the 10thInternational SPIN Workshop on Model Checking of Software（SPINSpringer-Verlag，2003.[9] E. M. Clarke，O. Grumberg和D.佩尔德。模型检查。MIT Press，1999.[10] H.加拉韦尔河Mateescu和I.M Smarandache。用于模型检测的并行状态空间构造。在Proceedingsof the 8th International SPIN Workshop on Model Checking of Software（SPINSpringer-Verlag，2001.[11] P. Godefroid和P. Wolper。模型检查的部分方法。计算机科学中的逻辑，第406 - 415页[12] P. Godefroid和P. Wolper。模型检查的部分方法。信息与计算，110（2）：305[13] T. Heyman，D.盖斯特岛Grumberg和A.舒斯特在超大型电路的并行可达性分析第12届计算机辅助验证国际Springer-Verlag，2000.[14] T. Heyman，O. Grumberg和A.舒斯特可达性分析的一种高效分布式算法。在第15届计算机辅助验证国际会议（CAV'03）的会议记录Springer-Verlag，2003.[15] F. Lerda 和 R. 西 斯 托 使 用 SPIN 进 行 分 布 式 内 存 模 型 检 查 。 在 Proceedings of the 6thInternational SPIN Workshop on Model Checking of Software（SPINSpringer-Verlag，1999.[16] R. Nalumasu和G. 哥帕拉克里希南 PV：用于验证LTL-X属性的模型检查器。第四届NASA兰利正式方法研讨会，第153 - 161页。NASA会议出版物3356，1997年。[17] R. Palmer和G.哥帕拉克里希南一种分布式偏序约简算法。在Proceedings of Formal Techniquesfor Networked and Distributed Systems-FORTE 2002 ， 22ndIFIP WG 6.1 InternationalConference Houston，Volume 2529 ofLNCS，第370页。Springer-Verlag，2002.[18] R. Palmer和G.哥帕拉克里希南部分降阶辅助并行模型检测（完整版）。技术报告，犹他大学，2002年8[19] D.佩尔德。All from one，one from all：on model checking using representatives. 第五届计算机辅助验证国际会议（CAVSpringer-Verlag，1993.[20] D.佩尔德。将部分降阶与在线模型检测相结合。系统设计中的形式化方法，8（1）：39[21] D.佩尔德。十年的部分订单减少。在第10届计算机辅助验证国际会议（CAV'98）的会议记录Springer-Verlag，1998.[22] 联合Stern和D. L.迪尔使穆尔河的水化。在Proceedings of the 9th International Conference onComputer Aided Verification（CAVSpringer-Verlag，1997.