用Maude验证重写理论的VLRL属性

理论计算机科学电子笔记137（2005）133-150www.elsevier.com/locate/entcs用Maude元级方法证明重写理论的模态性质Isabel Pita1，Miguel Palomino2DepartamentodeSistemasInforicosUniversidad Complutense de Madrid，Spain摘要重写逻辑是并发和分布式系统规范的一种非常有表现力的形式主义;更一般地说，它是一种变化逻辑。相比之下，VLRL是一种模态逻辑，它建立在重写逻辑之上，以精确地推理这种变化。在这里，我们提出了一种技术，机械地证明重写理论的VLRL属性使用重写逻辑的响应能力，通过其Maude实现。保留字：重写逻辑，Maude，模态逻辑，VLRL，反射，机械验证。1介绍重写逻辑[9]提供了一个形式化的框架，用于根据状态和状态转换对并发系统进行建模，这在Maude系统[5]中得到了有效的实现。它是一种变化的逻辑，演绎与变化直接对应。与此相反，重写逻辑的验证逻辑（VLRL）[7]是一种行动模态逻辑，以更间接和全局的方式谈论变化，就像其他模态和时态逻辑一样。VLRL是为了证明重写逻辑中特定系统的抽象属性而开发的。*研究得到西班牙项目MELODIAS TIC 2002 -01167和MIDAS TIC 2003 -01000的支持。1电子邮件地址：ipandreu@sip.ucm.es2 电子邮件地址：miguelpt@sip.ucm.es1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.042134I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）133在VLRL中，重写规则被捕获为动作，转换由动作模态表示，状态的结构由空间模态表示。通过这种方式，动作模态允许在特定的重写序列之后定义状态的属性，而空间模态允许定义状态组件的属性。这类公式可以在Maude的LTL模型检查器的帮助下在对象级别上得到证明，但一般来说，对于重写理论R，指定这样的谓词可能非常困难（甚至不可能）在[10]中，我们通过展示如何获得语义等价的理论RJ来解决这个问题，在这个理论中，这些谓词可以被直接定义。在本文中，我们开发了另一种方法来证明VLRL公式在给定状态下成立，这在很大程度上依赖于反射的使用[6]。重写允许系统访问自己的元级，并将重写作为普通对象进行操作，从而为控制重写过程提供了一种Maude一个国家，以及看看国家的内部结构。这种方法比以前探索的方法更简单，因为它既不需要理论转换，也不需要将VLRL公式转换为线性时序逻辑，也不需要使用Maude为了具体起见，我们用一个具体的例子来说明我们的技术，其完整的代码可以在maude.sip.ucm.es/vlrl/metalevelprover/上找到，但该方法是通用的，它可以很容易地适应任何系统。2重写逻辑分布式系统在重写逻辑[9]中通过重写理论R=（E，E，R）公理化，其中（E，E）是一个方程理论，将其状态集描述为与初始代数（E，E）相关联的代数数据类型TE/E系统在对E和R的合理假设下，重写理论是可执行的，并且有几种重写逻辑语言实现，包括ELAN[1]，CafeOBJ [8]，Maude [4，5]。特别是，Maude o编译器支持多种排序、子排序关系、运算符重载，并且在I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）133135其他实施例、反射。我们通过借用Maude手册[5]中的分布式银行系统示例来说明重写逻辑规范这样的系统是一个对象的mod BANK-ACCONDUIS保护INT。包括配置。op Account：-> Cid.op bal：_：Int-> Attribute。操作贷方借方：Oid Nat -> Msg。操作from_to_transfer_：Oid OidNat ->Msg.varsAB：Oid.vars M N N'：Nat.rl [credit]： credit（A，M）=>< 答：账户|bal：N + M>。crl[借方]： debit（A，M）=>< 答：账户|如果N >= M，则bal：N-M>。crl [transfer]：（从A到B transferM） =>< 答：账户|bal：N - M >< B：帐户|如果N >=M，则bal：N '+M>。恩德姆整数在第二行以受保护的形式导入，而对象的语法从模块CONFIGURATION导入。一个对象的形式<为A：C|Ats>，其中A是对象的名称，C是对象的类，而At是对象属性的列表。在模块BANK-ACTRONT中，只有一个类Account用属性bal声明。 我们也有三条留言，借记和转账，每个都有一个相关的重写规则（后两个是有条件的），这些规则将系统在收到消息时的行为公理化。请注意，对象和消息与运算符组合在一起在CONFIGURATION中声明为关联的、可交换的，tive，并且标识为none，它返回一个排序为Configuration的术语。最后，我们可以声明一个新的模块，它用一个新的类Manager扩展了前一个模块，其对象将负责创建新帐户。mod BANK-BERKER是incBANK-Accounts.操作管理器：-> Cid.op new-account：Oid Oid Nat -> Msg[ctor].varsOC：Oid.var N：Nat.rl[new]：< O：经理|无>< C：账户|bal：N>。恩德姆136I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）1333VLRL逻辑VLRL允许在选择一个特殊的状态后定义系统上的观测。 通过这种方式，用户定义了他想要谈论系统行为的方式;参见[7]以获得完整的演示。例如，在银行账户系统中，我们可以选择Configuration作为区分排序。那么，我们可以借助一个账号来观察系统中是否有账号？观察，以及具有观察余额的账户的当前余额？.操作帐户？：Oid ->VLRLBool。操作平衡？：Oid-> VLRLInt.对于每个对象的名称，这定义了两个它们的实际意义是通过解释I给出的，解释I取一个State类的项和一个s类的观察，并返回一个s类的项。例如，对于I（，余额？（A-002））= 300，其中A-002是帐户名称。行动我们首先定义预作用α。这些对应于通过以下演绎规则获得的证明项集合• 鉴别：每个[t]3个、[t]：[t]→[t]• 替换：对于每个重写规则r：t（x1，...，x）−→tJ（x1，.，x）和项w1，.，wn，和n nr（w）：[t（w/x）]→[tJ（w/x）]，• f-结构：对于每个f∈f，α1：[t1] → [tJ].α ：[t]→[tJ]1n nn，f（α1， . . . ， α）：[f（t1， . . ， t）]→[f（t，J， . . ，tJ）]n模以下等式：n1n• Idntit . ，[tn]）=[f（t1， . . ，tn）]，[3]我们使用[t]来表示状态的等价类和该状态的身份转移。I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）133137• E中的公理：t（α）= TJ（α），对于E中的每个方程t = TJ.操作是重写排序状态项的预操作。4直观地说，动作（或者更一般地说，预动作）对应于没有发生替换规则的顺序组合或嵌套应用的过渡。文[9]证明了重写理论初始模型中的任何转移都可以分解为预作用的交错序列。模态语言模态语言中的公式由下式给出：：：=true|t1=t2|¬ϕ|ϕ⊃ϕ|⟨α⟩ϕ|⟨⟨α⟩⟩ϕ|fd1， . . . ，其中t1和t2是可能包含观测的项，α是动作，f：s1. sm→State∈n，d是对应于f的非State类变元的数据项序列，ni与f的State类变元一一对应. 我们也有对偶运算符[]和d[]]，以及对偶空间运算符fd[1， . . . ] 。 . ，J. VLRL公式在给定状态[t]、观测解释I和基替换σ下的满足性由结构归纳法以通常的方式定义。若对t1和t2的解释相同，则方程t1=t2在[ t ]中成立;如果存在一个状态[tJ]，满足从[t]通过在[t]的顶部应用动作α，resp可以到达的条件，则在[ t ]中为真。 A nywhereein[t];并且fdin1， . . ，则满足，如果存在形式为fw（t1，.，tn），其中w是观测解释I和地面替换σ在状态[ t ]处的d的值，这样每一个人，都有自己的幸福。 我们在[7]中给出了一个正式的定义。4VLRL在Maude我们现在开始在Maude中指定VLRL，旨在使用它来自动检查给定的VLRL公式是否在给定的状态下成立。语法第一步是在Maude模块中定义VLRLfmod VLRL-公式是[4]上述对动作的定义假定R中的规则是无条件的。对条件规则的扩展是直接的（参见[2]）。138I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）133排序操作VLRLFormula。ops True False：-> VLRL公式。op_->_：VLRLFormula VLRLFormula->VLRLFormula。op ~_：VLRL公式-> VLRL公式。op<_>_：操作VLRLFormula -> VLRLFormula。op<<_>>_：操作VLRLFormula->VLRLFormula。op [_]_：操作VLRLFormula -> VLRLFormula。op [[_]]_：操作VLRLFormula ->VLRLFormula。op_/\_：VLRLFormula VLRLFormula->VLRLFormula。op_\/_：VLRLFormulaVLRLFormula-> VLRLFormula。变量X Y：VLRL公式。varA：Action。eq[A]X=~（~X）.eq[[A]]X=~（<>~X）。等式X1/Y = ~ X-> Y。eqX/|Y=~（X->~Y）。endfm上面的模块VLRL-FORMULAE定义了命题和模态动作公式的语法，它是独立于系统的。 ba sicfor mulaet1=t2，spatialfor mulaefd1， . . . ，而动作依赖于手头的特定系统，并且在超模块中定义。对于银行系统，我们在一个导入BANK-FORMULAE和VLRL-FORMULAE的模块VLRL-SAT中声明操作符op _=_：VLRLInt VLRLInt-> VLRLFormula. op_=_：VLRLBool VLRLBool-> VLRLFormula.原子公式（每个观察排序一个）。然后我们定义了mula的空间。 Forea chfd：S ta te. . . State−→状态，我们必须声明一个运算符fd.. . 产品：VLRLFORORMULA.. . VLRLFormula→VLRLFormula，及其对偶fd[. . . ]：VLRLFormula. . . VLRLFormula→VLRLFormula。在我们的例子中，唯一这样的运算符是，我们得到：op<>：VLRLFormula VLRLFormula ->VLRLFormula。op []：VLRLFormula VLRLFormula -> VLRLFormula。变量X Y：VLRL公式。eq[XY]=~<（~X）（~Y）>。最后，为了捕获预动作，我们为原始签名中的每个排序s声明一个排序Prestress-s。注意，在没有条件规则的情况下，我们只需要为那些在定义I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）133139国家建设者。然后，对应于被选择为系统状态的排序的预操作被设置为Action的子排序。排序首选配置。subsort优先级配置<操作。对于每个排序s，由恒等式规则产生的动作用运算符[ ]表示：s-→Predict-s。为了捕获应用替换规则所产生的动作，我们为每个重写规则添加：tJ（x），其中我们假设x =（x1：s1，.，X：sn），运营商l：s1. sn−→ RPredict-s。RPredict-s是使用的Predict-s的子排序以精确地识别通过替换规则获得的那些预动作。最后，通过允许签名的运算符也应用于动作来表示使用签名结构规则获得的动作：对于每个运算符f：s1.sn−→s，我们声明f：Predict-s1. Pre-s n−→Pre-s。此外，为了考虑第4页所述的商，规范中的所有公式都被复制，因此现在它们也适用和相应的等式的身份转移。 (Note新的操作符是用与配置上相同的属性声明的。对RPreview Configuration进行排序。子排序RPreview Configuration< Preview Configuration。op [_]：配置->预配置。opnone：->优先配置。op：预置配置预置配置->首选配置[aslogid：none]。RPre_Configuration操作符依赖于我们正在观察的特定系统的重写规则;在银行系统中操作贷方借方：Oid Int Int -> R优先配置。op transfer：Oid Oid Int Int Int -> R优先配置。op new：Oid Oid Int -> R优先配置。配方满意度为了研究VLRL公式的可满足性，我们首先必须为观测值定义一个有效的解释，然后将其扩展到任意项。例如，为了平衡？ 观察和“ 标 准 ” 解释，我们将宣布：op interp：Configuration VLRLInt-> Int.操作平衡？：Oid-> VLRLInt.op balance-aux：Configuration Oid -> Int.var C：配置。vars O O1 O2：Oid.变量N N1 N2：Int.var M：Msg.eq balance-aux（none，O）= 0。n140I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）133eq balance-aux（ C，0）= N。ceq balance-aux（ C，O2）= balance-aux（C，O2）。eq balance-aux（M C，O）= balance-aux（C，O）。eq interp（C，平衡？(O))= balance-aux（C，O）。eq interp（C，0）= 0。等式interp（C，s（N））= s（interp（C，N））。现在让我们做两个假设。第一，我们有两个行动，op nextState：State Action -> State。op nextStateinContext：State Action -> StateList.给定一个状态和一个动作，分别返回在顶部应用该动作后的状态的唯一（如果有的话）后继者，以及在上下文应用该动作可以获得的所有后继者的集合。 结论是，对于ea chfd：S ta te。 . State−→Statewehave ann可分解操作？：状态VLRL公式. VLRL公式−→布尔你 有没有 什么可分 享 的 ？（ S ， F1 ， . . . ， Fn ） 是 真 的 ， 如 果 S 是 f∈fd（t1， . . ，tn），其中每个ti满足Fi，其中i = 1. n;对于银行系统：操作可分解？：状态VLRLFormula VLRLFormula -> Bool。现在，任意VLRL公式的可满足性可以通过结构归纳法直接定义。可区分的排序Configuration被声明为State的子排序，还向其添加了错误常量，以在操作无法应用于给定状态时发出信号。子排序配置<状态。操作错误：->状态。操作_|=_：状态VLRL公式->布尔值。var S：State。var I1 I2：VLRLInt. varB1 B2：VLRLBool.变量F1 F2：VLRL公式。var A：Action。ceq（S| = I1 = I2）= true if interp（S，I1）== interp（S，I2）. ceq（S| = I1 = N2）=假，如果interp（S，I1）=/=interp（S，I2）。ceq（S| = B1 = B2）= true if interp（S，B1）== interp（S，B2）. ceq（S| = B1 = B2）= falseif interp（S，B1）=/= interp（S，B2）. eq（S| = True）=true.eq（S| = False）= false.eq（S |=（F1-> F2））=（S |= F2）或不（S |= F1）。eq（S |=（~ F1））=非（S |= F1）。- 行动ceq（S|=F1）=nextState（S，A）|=F1ifnextState（S，A）=/=error.eq（S|=F1）=false[owise]。ceq（S| = <> F1）= nextStateinContext（S，A）|= F1if nextStateinContext（S，A）=/= nil.eq（S| =<< A >> F1）= false [owise].I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）133141---空间ceq（S| = ）= true if decomposable？（S，F1，F2）。eq（S| = ）= false [owise].在Maude中，只有在没有其他方程适用的情况下，才尝试使用owise方程;它的语义可以纯粹根据方程来定义[5，第4章]。现在只需要详细说明我们认为理所当然的三种操作，而这正是本文的主要创新之处。请注意，在它们的本质上，它们应该使用指定银行系统本身的模块作为输入，例如在nextState的情况下选择一个特定的规则应用于状态。 为了定义它们，我们需要使用Maude5META-LEVEL模块Maude这个模块包含的操作符（Meta）表示的术语和模块分别为术语排序术语和模块。s类的变量X和常数C分别由引用的标识符“X：s”和“C.s”表示;项f（t1，...，tn）是“f [ t 1，. ，tn]，其中t 1，. . ，tn是t1和tn的表示。类似的约定也适用于模块。此外，Maude将元级计算减少到对象级计算。我们现在对我们所需要的那些做一个简要的总结;为了得到一个完整和更准确的描述，我们请读者参考[5，第10章]。• 操作metaApply有五个参数：模块M的元表示、项它尝试使用替换将项与规则的左侧匹配，丢弃前n个匹配项，并将规则应用于具有n+1的项的顶部匹配.它返回一个由约简项的元表示、其对应的排序或种类以及所使用的替换构成的三元组;我们可以通过操作getTerm获得三元组的第一个分量。• 操作metaXapply类似于metaApply，但规则可以应用于术语中的任何地方。• 操作metaMatch（R，t，最后一个参数用于枚举可能的匹配。如果成功，则返回一个排序Substitution项，否则返回noMatch项。有一个相应的泛化称为MetaXmatch。142I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）133• upModule将Maude数据库中已有的一个模块的名称作为第一个参数还有第二个论点，我们可以有把握地假设它总是正确的。• 函数upTerm接受一个术语并返回它的元表示;操作downTerm作为它的逆操作。6函数nextState、nextStateinContext和可分解的可分解所需的功能？由MetaMatch免费提供。因此，空间公式的语义可以定义为：ceq（S| = ）= true如果metaMatch（upMod_le（“V_L_R_L_S_A_T +，tr_e’'_|=_'S1：State，upTerm（F1）] = 'true.Bool /\ '_|=_'S2：State，upTerm（F2）]='true.Bool，0)=/=不匹配。ceq（S| = ）= false [owise].我们简单地将状态分解为两个子状态S1和S2，并通过元条件要求它们中的每一个满足相应的性质F1或F2'_|=_'S1：State，upTerm（F1）] = 'true.Bool /\'_|=_'S2：State，upTerm（F2）] = 'true. Bool然而，nextState和nextStateinContext函数的具体化要复杂得多，尽管其思想非常简单：从动作中提取标签，并使用MetaApply和MetaXapply应用相应的规则。为此，我们需要两个RPreviewConfiguration上的辅助操作：upAction，用于获取与操作关联的规则opupAction：RPrevent Configuration-> Qid.opgetSubs：RPrestitution Configuration-> Substitution.vars O O1 O2：Oid.变量N M N1 N2 N3：Int.eq upAction（credit（O，N，M））='credit. eq upAction（debit（O，N，M））='debit.等式upAction（transfer（O1，O2，N1，N2，N3））= 'transfer. eq upAction（new（O1，O2，N））='new.EQgetSubs（credit（O，N，M））='<<State。ceq nextState-aux（S，A1A2，i） =nextState（downTe rm（ge tF ir stT er m（R：S ub sti tu tion？），e rr orr），A 1）nextState（downTerm（getSecondTerm（R：Substitution？），错误），A2）如果A1 =/=无/\A2 =/=无/\R：替代品？：=metaMatch（upMo_dul_e（’R：替代品？=/= noMatch/\nextState（downTe rm（ge tFi rs tT er m（R：Su bs ti tut io n？），e r ro r），A 1）=/= error/\nextState（downTe rm（getSe co nd Ter m（R：S ub st itu ti on？），err orr），A2）=/= error.ceq nextState-aux（S，A1A2，i）=error144I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）133如果A1 =/=无/\A2 =/=无/\MetaMatch（upModule（’nil，i）== noMatch.ceq nextState-aux（S，A1A2，i）=nextState-aux（S，A1A2，s（i））ifA1=/= none/\A2 =/= none/\R：替代品？：=metaMatch（upModule（’无，i）/\R：替代？=/= noMatch/\（nextState（down Te rm（getFi rs tT er m（R：Su bs ti t u t ion？），e r ro r），A 1）== error or nextState（downT er m（g et Sec on dT er m（R：Su bs ti t u t io n？），e r ro r），A 2）== error）。最后，我们也有常数actionnone：eq nextState（none，none）= none。eq nextState（S，none）= error [owise].指定nextState背后的思想也适用于nextStateinContext操作。现在，由于动作可以发生在状态中的任何地方，而不仅仅是在顶部，所以我们使用MetaXmatch和MetaXapply来代替MetaMatch和MetaApply。因为同一个动作可以重写状态的不同部分，所以应用nextStateinContext的结果不会是一种一般来说，它是一个状态集合（实际上，在我们的实现中是一个列表）。为了不陷入太多的技术细节，我们推迟到附录的规格。7一些属性我们举例说明银行系统的一些性质，初始银行确认S有三个帐户，A-001，A-002和A-003，三个借记消息，一个从A-003到A-002的转账指令，以及一个我们在模块VLRL-SAT+中定义的新帐户消息。我们想决定，对于给定的公式F，F是否在S操作A-001 A-002 A-003 A-004经理：->Oid。op bankConf：-> Configuration.eq bankConf =<管理员：管理员|无>借方（A-001，150）借方（A-001，150）借方（A-002，400）（从A-003到A-002转移300）新帐户（管理器，A-004，1000）。让我们证明一个借记操作并不排除存在一个I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）133145账户余额减少，账户余额减少。请注意，该操作是在上下文中完成的，因为它只引用A-001帐户，而我们在状态中有更多的术语在VLRL-SAT+中减少：银行会议|=<<借方（A-001，150，300）>>（帐户？（A-001）=true/\平衡？（A-001）= 150）。结果Bool：true我们可以在A-001账户上同时执行借记操作并创建新账户A-004，在VLRL-SAT+中减少：银行会议|=<<借方（A-001，150，300）新（经理，A-004，1000）>>True。结果Bool：true但我们不能同时创建一个新帐户并对其进行操作：在VLRL-SAT+中减少：银行会议|=<<借方（A-004，150，300）新（经理，A-004，1000）>>True。结果Bool：false我们不能把超过活期余额的钱记入借方在VLRL-SAT+中减少：bankConf |=<>True。结果Bool：false除非我们先把钱转过去在VLRL-SAT+中减少：银行会议|=<<传输（A-003，A-002，300，1250，250）>><<借方（A-002，400，250）>> True。rewrites：71 in 120ms cpu（120ms real）（591rewrites/second）结果Bool：true但请注意，这两个操作不能同时执行在VLRL-SAT+中减少：银行会议|=<<借方（A-002、400、250）transfer（A-003，A-002，300，1250，250）>> True.结果Bool：false我们也可以用空间算子定义并发动作发生的状态部分来表示并发动作。例如，我们可以借记A-001账户，并从账户A-003转账到账户A-002：在VLRL-SAT+中减少：银行会议|=<（<借方（A-001，150，300）>余额？（A-001）= 150）（转移（A-003，A-002，300，1250，250）>>平衡？（A-002）= 550）>。结果Bool：true第一个动作是在顶部完成的，而第二个动作是在上下文中完成的。如果我们想在顶部表达所有的动作，我们可以使用恒等动作146I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）133去修复州的其他部分例如，在下面的属性中，我们将状态分为三个子状态：在VLRL-SAT+中减少：银行会议|=<（<借方（A-001，150，300）> True）<（new（manager，A-004，1000）> True）（<[（从A-003到A-002转账300）借方（A-002，400）））debit（A-001，150）] > True）> >.结果Bool：true8最后发言VLRL逻辑是一种强大的逻辑，用于证明重写逻辑中指定的系统的模态和时间属性。它允许对动作和空间属性进行具体化，这些属性探索了一个系统的结构，类似于Cardelli和Gordon [3]的移动环境模态逻辑所定义的系统结构在本文中，我们已经提出了一种方法来检查，如果一个给定的VLRL公式持有在一个给定的状态，使用Maude我们的技术可以应用于任意系统，只需稍微适应本文描述 尽管如此，这种描述应该已经被广泛应用，因为分布式系统倾向于在重写逻辑时指定一个结合和交换运算符，如这里;不同类型的例子可以在www.example.com上maude.sip.ucm.es/vlrl/metalevelprover/。事实上，虽然没有提出的一般性，定义，nextState和nextStateinContext操作的定义可以简化为关联和交换结构;在这种情况下，足以区分以下两种情况：该规则适用于通过替换获得的诉讼的情况。这个定义更有效，因为它没有得到所有可能的状态分解，但它通过将状态的某个部分与某个动作相匹配并证明状态的其余部分完全满足动作的其余部分来进行。通过直接在元级编程，可以提高实现的性能。也就是说，我们不需要使用upTerm和downTerm操作来不断改变级别，而是可以编写直接处理表示相应状态的项的元表示的方程。这种替代方案的缺点是，由于效率并非我们的主要关注点，我们已选择尽量保持规格清晰I. Pita，M.Palomino/Electronic Notes in Theoretical Computer Science 137（2005）133147与借助LTL Maude模型检查器在对象级别证明VLRL公式的技术相比，该方法不需要对原始理论进行转换，而只需为原始签名的每个函数定义nextState和nextStateinContext 从计算的角度来看，使用 元级极大地减少了证明公式，因为避免了在变换理论中模拟动作执行所需的重写步骤尽管如此，在示例中，我们已经运行了证明公式在两种情况下几乎相同的时间，这是由于元级别的计算效率低于对象级别的计算，以及LTL Maude模型检查器的高性能此外，LTL模型检查器在属性未填充时返回一个反例，而本文中解释的方法的当前实现则没有;尽管如此，我们计划在未来的版本中支持它确认我们感谢Narciso Mart-Oliet对之前的草稿提出的有益意见，感谢Franci的同事Dur'an在论文发表期间提出的引用[1] Borova n sky'，P. 、C. K irchn er，H. K ir ch n e r andP. - E. M〇r e au，ELANfromarit itinglgi c pointof view，Theoretical Computer Science 285（2002），pp. 155-185[2] 布鲁尼河和j.Meseguer，Generalized rewrite theories，in：J.C. M. Baeten，J.K. 伦斯特拉，Parrow和G. J. Woeginger，编辑，自动机，语言和编程。2003年6月30日至7月4日在荷兰埃因霍温 举 行 的 第 30 届 国 际 学 术 讨 论 会 Proceedings ， Lecture Notes in Computer Science 2719（2003），pp. 252-266。[3] 卡尔代利湖和A. D. Gordon，Anytime，anywhere：Modal logics for mobile ambients，in：Proceedi