理论计算机科学电子笔记185（2007）63-76www.elsevier.com/locate/entcs将对称性约简技术扩展到一个真实的计算阿拉斯泰尔F. 唐纳森1，2爱丽丝·米勒3格拉斯哥大学计算机科学系苏格兰格拉斯哥摘要大部分关于模型检验的对称性约简的文献假设一个简单的计算模型，其中并发系统中每个组件的局部状态可以用整数表示，并且组件之间不相互引用。用于模型检验的对称性约简技术通常需要解决NP-难构造轨道问题（COP）-计算对称群下给定状态的等价类中的最小元素。多项式的时间策略来解决简单的计算模型下的COP的实例是已知的一大类对称群。我们表明，这些策略是不直接适用的计算模型时，扩展到允许组件相互引用，并提出了一种方法，他们的扩展，从而在一个现实的计算模型，易于处理，内存最佳对称性约简技术使用TopSPIN对称性约简软件包的SPIN模型检测器的实验结果说明了我们的技术的有效性。关键词：模型检测，对称性，计算群论，并发性，Promela/SPIN，分布式系统，GAP1引言在过去的十年里，人们对使用对称约化产生了很大的兴趣。模型检验的状态空间爆炸问题。对称性约简技术利用并发系统通常具有复制结构的事实，在这种情况下，可以在商状态空间上检查系统模型的时间属性，从而避免由复制引起的等效行为的冗余检查。模型的对称性通常由一组分量恒等式置换引起，当提升到状态时，这会引起状态空间的自同构。 标准方法 在显式状态模型检查中利用对称性涉及将每个1 由卡内基信托基金会支持的苏格兰大学。2电子邮件地址：ally@dcs.gla.ac.uk3 电子邮件地址：alice@dcs.gla.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.02964A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）63然后，当达到等效状态时，它将被转换为相同的表示（导致转换到先前达到的状态），并且搜索可以回溯。计算等价类代表的标准方法是，给定状态的全序±，取rep（s）=min±[s]G，其中s是一个状态，[s]G是等价类，或s在对称群G下的轨道在一个简单的计算模型下计算min±[s]G的问题，其中每个分量的局部状态是一个整数值，分量没有引用而±是向量上通常的字典序，称为构造性轨道问题（COP），并且是NP-难的[4]。对于某些类的对称群，包括完全对称群和可以分解为子群的不相交/圈积的群，COP可以在多项式时间内求解[4，8]。然而，诸如Promela [11]的丰富的规范语言允许系统的组件保持彼此的引用，并且软件系统的现实模型依赖于此功能。我们提出了具有参考文献的构造性轨道问题（COPR），并表明在[4，8]中提出的用于COP的多项式时间策略在例如[4，9]中使用的简单计算模型下并不直接扩展到解决COPR。然后，我们提出了一个计算群论的方法，它扩展了任何战略解决COP的解决方案。该扩展基于SymmSpin软件包用于SPIN模型检查器[1]的分段策略，这是我们针对全对称群的方法的特殊情况。虽然我们的扩展导致精确的对称性约简，但代价是丢失多项式时间解，使用TopSPIN包进行SPIN模型检查的实验结果表明，[7]用两个Promela例子的各种配置证明，在实践中，我们的方法比枚举G来计算最小值要有效得多。我们证明了COPR与COP是多项式时间等价的，并讨论了这些问题与计算群论中寻找群下集合的最小像的问题之间的关系[14]。2的计算我们使用组件来表示并发系统中的进程、通道或共享变量 设I ={1，2，. ，n}是用于这样的系统的组件标识符的集合。假设一个组件的局部状态由两部分组成，它的控制状态和参考状态。组件的控制状态由该组件的所有局部变量的值确定，这些局部变量不是对其他组件的引用，例如程序计数器或布尔值标记。不失一般性，我们可以将局部控制状态抽象表示为集合Lc={0，1，2，.，k}，其中k≥ 0。另一方面，组件的引用状态由所有局部变量的值确定，这些局部变量是对其他组件的引用。例如，leader election协议中的组件可能需要一个引用变量，A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）6365CC（最终）保持领导者的身份;电话模型中的用户可以保持对其当前伙伴的引用。因此，参考状态是集合Lr=（I<${0}）m中的元组，其中m≥0。 这里m是组件所拥有的引用数，0用作默认值（例如， 代表领导人未知）。在不失一般性的情况下，我们可以假设所有分量都恰好有m≥0个参考局部变量。因此，全局状态s∈（Lc×Lr）n具有以下形式：S=（l1，（r1，1，r1，2，.，r1，m），l2，（r2，1，r2，2，.，r2，m），.，1n，（rn，1，rn，2，. ， rn，m）），其中li∈Lc表示部件i的控制状态，ri ， j∈I<${0}是部件i的第j个参考变量的值（i∈I，1≤j≤m）。在m= 0的特殊情况下，即当组件之间没有相互引用时，Lr由0元组组成，因此可以忽略。一个状态s∈Ln则具有形式s =（l1，l2，.，ln）。我们将m >0和m= 0的计算模型分别称为有引用和无引用的计算模型一个Kripke结构是一个对M=（S，R），其中S<$（Lc×Lr）n是一个非空的状态集，R<$S×S是一个全跃迁关系。Kripke结构表达了用高级语言（如Promela）编写的并发系统规范的语义规范的语句确定了从Kripke结构的给定状态可以进行哪些转换，并且可以通过从某个初始状态开始遵循所有路径来构造完整的结构3模型检验3.1群论记法我们假设一些基本群论的知识，但在这里重述一些符号 设G是一个群，α1，α2，... ，αn∈ G. G的最小子群包含元素α1，… ，αn表示为α1，α2，… ，αn≠0，称为α1，α2，.，αn.元素αi（1≤i≤n）称为这个子群的生成元。令X ={α1，.，αn}是G的有限子集。然后我们用<$X<$来表示<$α1，.，αn<$，X生成的子群。I的所有置换的集合在映射的合成下形成一个群，记为Sn（n点上的对称群）。若J<$I，α∈Sn，则α（J）={α（i）：i∈J}，J在G中的集合稳定子是子群StabG（J）={α∈G：α（J）= J}. 如果H是子群对于G，我们写H ≤ G（注意，我们也用≤表示向量的字典序）。3.2自同构与商结构在一个无参考的计算模型中，α∈Sn作用于s =（l1，l2，.，ln）∈Ln通过简单地置换控制状态：α（s）=（lα−1（1），lα−1（2），.，lα−1（n））。设s∈（Lc×Lr）n如第2节所述，α∈Sn. α到s的应用可以被认为是一个两阶段的过程。 对于每个i，首先，局部状态（li，（ri，1，ri，2，.，ri，m））被分量i的局部状态替换。66A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）63CCα−1（i）.然后将α应用于分量i的每个参考变量（其中α（0）= 0）。由此可见：α（s）=（lα−1（1），（α（rα−1（1），1），α（rα−1（1），2），. ，α（rα−1（1），m）），lα−1（2），（α（rα−1（2），1），α（rα−1（2），2），. ，α（rα−1（2），m）），. 、lα−1（n），（α（rα−1（n），1），α（rα−1（n），2），. ，α（rα−1（n），m）。例如，考虑由4个组件组成的系统，其中每个组件的状态由其控制状态和一个参考变量组成。在这种情况下，n= 4，m= 1，并且Lr={ 0， 1， 2， 3， 4}，1={ 0， 1， 2， 3， 4}。假设Lc={ 0， 1， 2}。设s=（1，4，2，3，0，0，0，4）∈（Lc×Lr）4（控制态用黑体表示如果α=（3 4），则α（s）=（1，α（4），2，α（3），0，α（4），0，α（0））=（1，3，2， 4，0， 3，0， 0）。置换α∈Sn是Kripke结构M=（S，R）的自同构，如果α保持转移关系R.也就是说，对于每个跃迁（s，t）∈R，（α（s），α（t））∈R。M的所有自同构的集合在映射的合成下形成群，记为Aut（M）。若G是Aut（M）的子群，则G在S上诱导一个等价关系，其中s∈S的等价类或轨道是集合[s]G={α（s）：α∈G}.如果rep是将每个状态映射到其等价类的唯一表示的函数，则M乘G的商Kripke结构可以定义如下：MG=（SG，RG）其中SG={rep（s）：s∈S}，RG={（rep（s），rep（t））：（s，t）∈R}. 一般来说，MG是一个比M小的结构，但MG和M是等价的，因为它们满足在群G下不变的同一组逻辑性质（即关于G“对称”的性质关于下面定理的证明，以及时序逻辑CTL_T的细节，参见[5]。定理3.1设M是Kripke结构，G是Aut（M）的子群，φ是CTL的一个公式.如果φ在G下不变，则M，s| = φi MG，代表|= φ3.3建设性轨道问题设±是S上的全序。 则对任意s ∈ S，rep（s）可以取为min± [s] G，即[s] G中关于序±的最小元素。如果M =（S，R）具有初始状态s0，则算法1（改编自[12]）可以用于探索MG。算法的效率取决于min±[s]G的计算复杂度。 假设一个没有参考的计算模型，使得S<$Ln，我们可以取±≤，向量的通常字典序。4、我们有定义3.2构造性轨道问题（COP）[4]给定一个群G≤Sn和一个状态s∈Ln，求min≤[s]G，G中的字典序最小元s在G下的轨道。4.不存在cho s ingrep（s）=min≤[s]G的情况，这只是一种简单的随机选择方法，但它是一种常用的方法。使用另一个区别元素将是等效的，但不允许我们在没有转换的情况下适应现有的算法。A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）6367C定理3.3 [4] COP是NP-难的。尽管这个令人沮丧的结果，对于一大类常见的对称群，它是可能的解决的COP在多项式时间。我们在4.1节中概述了这些特殊情况。此外，已经提出了COP的近似解决方案，并证明是有效的[8]。现在我们转向允许引用的更现实的计算模型为了在S_n（L_c×L_r）_n上定义一个全序≤，我们定义了两个投影映射，分别把一个状态投影到它的控制部分和参考部分上.对于状态s =（l1，（r1，1，r1，2，.，r1，m），l2，（r2，1，r2，2，.，r2，m），.，1n，（rn，1，rn，2，.，rn，m）），cnc（s）=（l1，l2，.，ln）和ref（s）=（r1，1，r1，2，.，r1，m，. ，rn，m）。定义3.4对于s，t∈S，s≤t，如果s=t;c（s）c（t）;或c（s）=c（t）和ref（s）ref（t）。<<这里ref（s）和ref（t）使用向量上的通常字典排序进行比较（类似于cnc（s）和cnc（t））。很明显，≤是状态的全序如果s≤t且s/=t，我们写st。我们现在将COP扩展到具有参考的计算模型定义3.5带参考的COP（COPR） 给定群G≤Sn和状态s∈（ Lc×Lr） n，求min≤[s]G，S在G下的轨道中的≤-最小元。很明显，COPR是COP的推广由于COP是NP-难的（定理3.3），COPR通过限制也是NP-难的.事实上，这两个问题可以证明是多项式时间等价的。 一个COP的instance平凡地是一个COPR的instance，而一个COPR的instance可以在二次时间内转换成一个COP的instance。后者通过用N个二进制值的向量替换每个分量ID参考Ri，j来实现，除非Ri，j=L >0，否则所有二进制值都是0，在这种情况下，从右边开始的二进制值L例如，如果n= 8且ri，j=5，则ri，j的值被转换为二进制序列0， 0，0， 1， 0， 0， 0， 0。为保存这些值而引入的变量`n−5x`5x被建模为具有二进制值局部状态的组件。如果convert表示执行这种转换的函数，则将值1l放置在右边确保对于状态s和t，s≤ticonvert（s）≤convert（t）。对称群G的元素也必须适当地变换，使得如果s是一个状态且α∈G，则变换后的元素αJ必须满足convert（α（s））=αJ（convert（s））。4对称性约简策略设S ∈ Ln，G ≤ Sn. 群G ≤ Sn 的对称约化策略是函数f：S → S，其性质是f（s）= min≤ [s] G[1]. 这种函数的应用通常涉及重复应用来自G的元素（乘积68A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）63算法1探索商Kripke结构的算法，给定全序在国家。达到：={min±[s0]G};未探测：={min±[s0]G};而未探测/=未探测将状态s从未探索中移除;对于所有的继承国t，如果未达到min±[t]G，则将min±[t]G加至已达到;将min±[t]G加至未探索;结束if结束for结束while是G的一个元素）。我们可以等价地定义关于群G的对称约化策略如下：定义4.1G≤Sn的（精确）COP策略是函数f：S→G，使得对所有s∈S，如果α=f（s），则α（s）=min≤[s]G。换句话说，将f应用于s会产生G中使s最小的元素。由于求解COP的困难性，一些对称约化方法将状态映射到少量代表而不是单个代表[1，4]。这被称为多轨道代表方法。使用多轨道代表的COP策略被称为近似策略[8]。定义4.2G≤Sn的近似COP策略是函数f：S→G使得对所有s∈S，若α=f（s）则α（s）≤s。一个好的近似策略会产生G的元素，这些元素将轨道G映射到少量的代表上。COPR的精确策略和近似策略类似地定义，使用全序≤。4.1多项式时间精确策略枚举If |G|是n中的多项式（例如，当G是由单向/双向环网络拓扑产生的循环或二面体群时），f（s）可以通过枚举G的元素并返回元素α来计算，使得对于所有β ∈G，α（s）≤β（s）[4]。很明显，这种策略是不可行的，|G|是n的指数。当G=Sn时，f（s）可以取为使s按升序排序的任意置换[1，4].比如说，如果G=S4和s =（5，2，4，3）∈ {0，1，.，5}4，对s排序得到min≤ [s] G=（2，3，4，5）。由于排序可以在多项式时间内执行，这导致Sn的多项式时间精确COP策略。算法2给出了一个基于选择排序的策略。 通过排序求解COP的思想在[8]中被推广到一类群，同构于Sm，其中m≤n。如果G是子群H和K的不交积，A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）6369且h和k分别是H和K的COP的多项式时间策略，则定义为f（s）=k（s）h（s）的策略f是G的多项式时间策略[4].换句话说，可以通过应用序列排列来求解G的COP，该序列排列分别使关于H和K的s最小化。在实践中，当系统中的多个组件类型之间完全对称时，经常会出现不相交的产品组。类似的方法可以用来获得多项式时间COP策略，当G是多项式时间策略可用的子群的圈积[4]。当系统具有树形拓扑时，通常会出现环形产品组。算法2基于选择排序的Snα：=id对于所有i∈ [1，.，n− 1] doβ：=id对于所有j∈ [i + 1，...，n]如果（i j）α（s）<βα（s），则β：=（i j）end ifendforα：=βα端返回α4.2参考文献的问题上面总结的策略是针对没有参考文献的计算模型提出的显然，基于枚举的策略立即扩展到具有引用的计算模型，如果|G|是n的多项式。然而，其他战略并不立即适用。我们表明这对于COP策略，其中G=SN和代表通过排序计算。类似的论点也适用于其他策略。G=Sn的COP可以通过对状态s进行排序来求解的证明基于以下引理。引理4.3在简单的计算模型中，不存在i1，j1，i2，j2∈I，其中i1s，（i1j1）（s）=（1，0，0， 3，0， 3）>s。但（i2j2）（i1j1）=（1 3 2），以及（1 3 2）（s）=（0，1，0， 1，1， 0）<$（i2j2）（s）。Q70A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）63这个反例对于n = 3的情形可以被推广为对于任何n ≥ 3给出一个反例--考虑如上的i 1，j 1，i 2和j 2，并且s =（1，0，0，2，0，0，. ，0，0）。将算法2中的≤替换为≤应用于s=（1，0，0， 2，0， 2），得到的元素（1 3）不会最小化s，而枚举S3得到的元素（1 3 2）会最小化s。因此，算法2的这种调整不会产生精确的COPR策略。假设G≤Sn是一个对称群，GJ≤SnJ是一个同构于G的群，它是通过将一个COPR实例转换为一个COP实例而得到的，在3.3节中讨论过（这里nJ≥n是用于表示转换态的分量数G的多项式时间COP策略一般不会产生G j的相应COPR策略，因为GJ对{1，2，.，nJ}的性质与G在{1，2，.，n}。例如，如果G是子群H和K的不交积，则GJ是子群HJ和KJ的直积，但可能不是HJ和KJ不交地作用在{1，2，. ，nJ}。我们现在展示如何将多项式时间精确COP策略扩展为精确COPR策略。结果不是多项式时间策略，但如果G很大，可能比枚举策略更有效5分段：将策略扩展到一个有参考我们的方法来扩展一个策略COP到一个为COPR工程通过构造一个分区的I从一个给定的状态，并枚举这个分区的稳定器。5.1隔板和稳定剂I的划分是集合X ={I1，I2，. ，Id}，其中d> 0，Ij<$ I（1 ≤ j ≤ d），dj=1 Ij，且Ii<$Ij=<$，其中1 ≤ i/= j ≤ d。定义5.1设X是I的一个划分，且G≤Sn。X在G中的（划分）稳定子是子群stabG（X）=J∈XstabG（J）。5.2分割一个国家我们定义了G的一个子集，它的元素具有最小的控制状态。定义5.2令小G（s）={t∈[s]G：cnc（t）≤cnc（u）<$u∈[s]G}。显然min≤[s]G∈smallG（s）.给定一个状态s，向量cnt（s）可以被看作是一个没有引用的计算模型下的状态。以下结果是这一观察和定义5.2的结果：引理5.3对s∈S，t∈smallG（s）惠c（t）= min≤ [c（s）] G.I=A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）6371对于0≤i≤k，令s（i）={j∈I：lj=i}，即s中具有控制状态i的分量的指数集。定义作用于状态的函数seg，seg（s）={s（0），s（1），.，s（k）}。显然，对于任何状态s，seg（s）是I的一个划分。5.3通过分割的引理5.4若t∈小G（s）且α（t）ref（α（t））。< 由于cg（t）=cg（α（t）），对于1≤i≤k，t（i） =α（t）（i），即seg（t）=seg（α（t））。因此，α保持seg（t），即α∈stabG（seg（t））。因此，如果一个状态t∈smallG（s）不是[s]G在≤下的最小元素，那么搜索G的最小元素可以限制在stabG（seg（t））。注意，如果分量索引i，j∈X∈seg（t），则仍然需要考虑G中将i映射到j的元素。因此，我们不能把seg（t）的元素当作序列来处理，并计算它们的逐点稳定子（这在计算上会更容易）。假设我们对G有一个精确的COP策略f。设β=f（c（s）），使得β（c（s））=min≤[c（s）]G.显然，β（c（s））=c（β（s）），因此根据引理5.3，β（s）∈小G（s）。根据引理5.4，群H=stabG（seg（β（s）现在可以枚举找到一个元素α，使得对于所有δ∈H，αβ（s）≤δβ（s）。因此，我们证明了以下几点：定理5.5设s∈S，G≤Aut（M），f是G的精确COP策略. 算法3是G.算法3将群G的精确COP策略f扩展为精确COPR战略β：=f（cnc（s））H：=stabG（seg（β（s）α=id对于所有δ∈H，如果δβ（s）<$αβ（s），则α：=δend ifendforreturnαβ图1用图形说明了[s]G（由外椭圆表示）和它的子集小G（s）（由内椭圆表示）之间的关系，以及计算G中使s最小的元素的过程。我们用一个例子进一步说明了这种方法。设n、m、Lc、Lr和G与4.2节的例子相同。让s=（1，2，0， 1，0， 1，2， 1）。然后，c_（s）=（1， 0， 0， 2），并且应用72A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）63算法2，A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）6373[s]GSβ= f（ cnc（ s））α∈ Hβ（ s）αβ（ s）=min≤[s]G小G（s）=[ β（ s）]Hc（ β（ s））= min≤[ c（ s）]GH=stabG（seg（β（s）Fig. 1.通过分割减少对称性。我们发现β=（1 3）满足β（cnc（s））=min≤[cnc（s）]G. 将β应用于s得到t=（0，3，0， 3，1， 2，2， 3），并且seg（t）={{ 1， 2}，{ 2}，{ 3}}。很容易检验stabG（seg（t））= n（1 2）n，一个2阶群，并且将（1 2）应用于t给出min≤[s]G=（0，3，0， 3，1， 1，2， 3）。对于该示例，算法2需要应用6个群元素，然后枚举2阶群。通过基本枚举计算min≤[s]G需要将G的所有24个元素应用于s。6电子商务假设f可以在多项式时间内计算（使用[4，8]中描述的策略），算法3的效率主要取决于H的计算和计算H=stabG（seg（s））等价于计算群中一个集合的稳定子。计算集合稳定器的最有效算法涉及使用基和强生成集的组的回溯搜索[2，16]。通常，这种搜索可以使用问题独立的算法和基于集合稳定器属性的算法来大量修剪因此，尽管事实上没有多项式时间算法是已知的计算集稳定器，相关的开销并不大。此外，如7.1节的实验结果所示，在搜索过程中必须考虑的I的所有划分的集合{seg（s）：s∈S}通常比I的可能划分的数量小得多。因此，分区稳定器的重新计算可以通过缓存分区稳定器对来避免在最坏的情况下，H可能有大小|G|（例如，|分段|= 1），以及|G|可以5这种划分的数目是Bn，第n个贝尔数，递归地定义为B0= 1，Pn−1`n′Bn=k=0kBkfor n > 0 [15].74A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）63像n一样大！(in其中G=Sn）。但是，如果不同组件控件状态的数量相当大，则许多状态将具有以下属性：|分段|= n，在这种情况下stabG（seg（s））是平凡群。7SPIN模型我们已经实现了本文中提出的方法，作为对TopSPIN [7]的补充，TopS PIN是SPIN模型检查器[11]的对称性简化包。在搜索过程中，分区稳定器的计算通过计算代数系统GAP [10]执行。 给定Promela规范，SPIN为相应的可执行验证程序生成C代码。TopSPIN根据Promela规范自动检测组件对称性，并（使用与SymmSpin [1]类似的方法）根据用户指定的4个选项之一将对称性约简算法添加到验证器如果选择了枚举选项，那么在验证过程中将应用内存最优对称约简，运行时开销与对称群G的大小成比例（因此这只对小的组有用，或者用于与更有效的选项进行比较）。如果选择快速或分段选项，则TopSPIN使用GAP来分析G的结构，试图找到多项式时间精确的COP策略，如[8]所述。对于快速选项，将直接使用这种策略。如果规范的组件不相互引用，这将导致内存最佳验证;否则模型检查可能涉及使用每个轨道的多个代表。选择段选项意味着COP策略将扩展到内存最优的COPR策略，使用本文提出的方法。在这种情况下，验证器当前必须从GAP系统中实例化。最后，可以选择爬山选项，在这种情况下，将应用基于爬山局部搜索的近似对称性降低策略[8]。如果在fast或segment选项中找不到G的多项式时间COP策略，则默认使用此策略。7.1实验结果我们说明了内存需求和验证时间的枚举，快速和段策略的变化使用两个Promela示例的各种配置：电子邮件系统和负载均衡器，它以公平的方式将请求从客户端池转发到服务器池电子邮件示例改编自[3]，并用作[8]中对称性约简的案例研究系统的配置由p个客户端进程组成，它们通过经由网络通道组件向邮件程序进程发送消息来进行 客户端组件是同一个参数化流程因此行为完全相同，因此客户端之间完全对称系统的Promela规范中的组件使用引用变量来跟踪给定消息的发送者和接收者。具有p个客户端的电子邮件示例的配置表示为电子邮件p。负载均衡器配置中的组件A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）6375系统国orig时间orig|G|国红色时间enum时间segptns国快速时间快速电子邮件3232560.1639020.80.2539080.2电子邮件485264192436255647385602电子邮件53.04× 107357612026531525371931532340电子邮件6--7201 .一、7×10613523160011二、3×106576电子邮件7--50409.3×106-50970131 .一、53×1076573磅2/62.37× 10715851440234742652894310665磅2/7--100804413743762662596124516磅3/6--4320125126502427133025620457磅3/7--30240293657-2722451685167213磅4/6--17280527548-23788841.7×106487磅4/7--1209601.2×106-2977912963.7×1061583表1配置电子邮件和负载均衡器（lb）规范的实验结果。示例是具有相关联的通信信道的一组P服务器和Q客户机进程以及负载平衡器进程（具有专用输入信道）。 服务器的负载是在其输入通道上排队的消息数。客户端进程向负载均衡器发送请求，如果某个服务器通道未满，负载均衡器将不确定地将请求转发到负载最小的服务器队列之一。每个请求都包含对其关联的客户端进程，由负载均衡器指定的服务器使用此通道为请求提供服务。具有p个客户端和q的配置表示为p/q。在p个服务器之间以及q个客户端之间存在完全对称性，因此p/q配置具有p阶的不相交乘积对称群！q！对于这两个例子，我们验证了作为断言嵌入在规范中的安全属性表1包含电子邮件和负载均衡器示例的各种配置的实验结果对于每种配置，我们给出了没有对称性约简的模型状态的数量（orig），通过枚举或分段选项（红色）进行记忆最佳对称性约简，以及通过快速选项（快速）进行对称性约简。状态压缩的使用，SPIN提供的一个选项，由斜体的状态数表示。选择此选项用于两种配置，以允许通过更有效地存储状态进行验证，而无需对称性降低，并具有相关的时间开销。对于枚举（enum）、分段（seg）和快速（fast）选项，以及不应用对称约简的情况（orig），给出了验证时间（以秒为单位）。对称群的大小（|G|）和使用段选项（PTNS）产生的分区的数目也被给出。超过可用资源或未在15小时内终止的验证尝试以“-”表示。 所有实验都在具有2.4GHz Intel Xeon处理器、3Gb可用主存储器、运行SPIN版本4.2.3的PC上进行。对于这两个例子，特别是对于负载均衡器，使用对称性约简技术允许验证更大的配置当G很大时，枚举不是一种可行的技术，76A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）63但是通过段选项，可以使用唯一的代表对商结构执行模型检查尽管这比使用fast选项要慢，但是负载均衡器示例的大配置的状态减少是令人鼓舞的。如第6节所述，此时间开销主要是由于最小化状态的最后一步，涉及G的（潜在的大）子群的枚举。8相关工作在[4]中研究了模型检验中对称约简的COP，并提出了某些类别的群的多项式时间策略，在第4.1节中总结。在[1]中研究了在存在组件间参考的情况下执行对称性约简的问题，其中分段策略提供了存储器最优对称性约简。当G=Sn时，该策略适用，并且被非正式地描述为应用对状态的主阵列进行状态s的主数组类似于center（s）。我们已经为malised这种方法使用分区和稳定的想法，并推广的方法适用于任意子群的SN。还提出了一种用于完全对称群的近似策略--安...在SPIN模型检查器中利用对称性的另一种方法是通过向Promela语言添加关键字来处理参考变量[6]。最近的一种方法在约束规划中对称破缺需要解决与COP相关的问题[13]。在搜索过程中，对称破缺是通过确定给定节点处的变量的部分分配是否在对称群G下的其轨道中是字典序最小的来执行的。如果没有，搜索回溯。该方法依赖于一种算法的变体，用于找到置换群下集合的最小图像[14]。这个问题可以被证明是多项式时间等价于COP。9结论和今后的工作我们已经提出了一种方法来扩展对称性约简策略，提供内存最优的减少下一个简单的计算模型，使内存最优性保持在一个现实的计算模型，其中组件保持相互引用。这种方法形式化和generalises的分段策略所采用的SymmSpin模型检查器，并适用于任意对称群的多项式时间COP strategy.We可以找到我们实现了我们的技术在TopSPIN对称约简包SPIN，使用GAP进行群论计算。使用两个Promela实例的实验结果表明，该方法的结果A.F. Donaldson，A.Miller/Electronic Notes in Theoretical Computer Science 185（2007）6377在一个显着的加速超过对称减少枚举，并说明了贸易之间的内存和验证时间与选择一个确切的或近似的对称减少战略。该方法的主要瓶颈是在应用多项式时间COP策略未来的工作包括在TopSPIN中实现[14]中提出的规范化算法，以解决这个问题。确认感谢David Manlove就COP和COPR之间的关系进行了有益的讨论，并感谢EPSRC资助的搜索中的对称网络（SymNet）提供了一个有助于这项工作的讨论论坛引用[1] D. Bosnacki，D. Dams和L.霍兰德斯基对称自旋。International Journal on Software Tools forTechnology Transfer，4（1）：65[2] G.管家基本算法置换群，卷559LNCS。Springer-Verlag，1991.[3] M. Calder和A.米勒在电子邮件中推广功能交互。在FIWIOS Press，2003.[4] E.M. Clarke，E.A. Emerson，S. Jha和A.P. Sistla。 模型检验中的对称性约简 在CAV Springer，1998年。[5] E. M. Clarke，O. Grumberg和D.佩尔德。 模型检查。 MIT Press，1999.[6] F. Derepas和P. Gastin。用Spin对复制进程进行模型检验。 在SPINSpringer-Verlag，2001.[7] A.F. Donaldson和A.米勒用于SPIN模型检验器的计算群论对称性约化包。在AMAST施普林格，2006年。[8] A.F. Donaldson和A.米勒模型检验中对称约化的精确与近似策略。在FM施普林格，2006年。[9] E.A. Emerson和T.哇动态对称约简。在TACAS施普林格，2005年。[10] Gap集团。 亚琛，圣。安德鲁斯，1999年。http：//www-gap.dcs.st-and.ac.uk/[11]G. J. Holzmann。 SPIN模型检查器：入门和参考手册。 艾迪森·韦斯利2003年[12] C.N. IP和D.L.迪尔通过对称更好地验证。 系统设计中的形式化方法，9（1/2）：41[13] C. Je Eschererson，T. Kelsey，S. Linton和K.皮特里GAPLex：结合静态和动态对称破缺。CP Pod技术报告，CPPod-15-2006，2006年。[14] S. 林顿寻找集合中最小的图像在ISSACACM Press 2004.[15] G.C.罗塔集合的分区数。美国数学月刊，71：498[16] A.瑟蕾斯 排列组算法。 剑桥大学出版社，2003年。
我的内容管理
展开
