Maude实施CCS操作语义的新实现及其逻辑描述的过程的论文总结

282S−→理论计算机科学电子笔记71（2003）网址：http://www.elsevier.nl/locate/entcs/volume71.html19页在Maude实施CCS 2*Alberto Verdejo1和Narciso Mart-Oliet1Dpto. deSistemasInform'ati c osyProg ramaci'on，Universidad Complutense de Madrid，Spain.摘要本文详细介绍了如何弥合理论与实践之间的差距，在Maude的CCS操作语义的新实现，其中转换成为重写和推理规则成为条件重写规则的重写的条件，Maude 2.0的新功能成为可能。我们实现了通常的过渡语义和弱过渡语义的内部行动没有观察到，并在他们之上，我们还实现了Hennessy-米尔纳模态逻辑描述的过程。我们比较这种实现与以前的过渡成为判断和推理规则成为重写，并评论扩展LOTOS语言。关键词：可执行语义框架，操作语义，CCS，模态逻辑1介绍在提出重写逻辑作为逻辑和语义框架的背景论文[10]说明了将推理系统映射到重写逻辑的几种不同方式一个非常普遍的可能性是映射一个推理规则，形式S1... Sn0转换成S1形式的重写规则S n−→S0重写多个判断集Si.这种映射从抽象的角度来看是正确的但是考虑到重写规则的可执行性，考虑S0S1... S n仍然重写多个判断集，但是从结论到前提，所以用这些重写规则重写对应于以自下而上的方式搜索证明。同样，这种映射是正确的，在这两种情况下，直观的想法是重写关系对应于水平条*研究 支持 通过 CICYT 项目 正式制度发展 巴萨多斯恩AgentesM'oviles（TIC2000-0701-C02-01）。1电子邮件：{alberto，narciso}@ sip.ucm.es2003年3月，出版社dbyElsevierScienceB。 V. 操作访问和C CB Y-NC-N D链接。VERDEJO和 MARTI-OLIET283→在典型的教科书推理规则的表述中将结论与前提这些映射可以应用于各种各样的推理系统，如[10]中所详细描述的，包括逻辑的推理系统以及语言的结构操作语义定义然而，在操作语义学的情况下，判断Si通常具有状态之间的某种转移PiQi的形式，使得考虑将状态之间的这种转移关系映射到表示状态的项之间的重写关系当以这种方式思考时，P1→ Q1.. 。P n→ Q nP0→Q0成为一个条件重写规则的P0−→ Q0如果P1−→ Q1. Pn −→ Q n，其中条件包括重写。这种形式的规则已经被Meseguer在关于重写逻辑的开创性论文[11]中考虑过。在逻辑层次上，这种映射也是正确的，但是在映射中必须小心地考虑操作语义的转换中出现的附加信息。例如，在进程代数的结构化操作语义中，转换必须具有提供同步机制 如何解决这些细节在米尔纳的CCS[12]的特殊情况下已经显示在[10]。此外，文献[4，8]显示了这种用于CCS的语义映射的良好性质。随着1999年Maude系统的第一个版本的可用性[6]，我们开始了一个项目，以完全可执行的方式仔细实现CCS操作语义，以实际评估上面总结的理论上优雅和正确的想法。我们遇到的第一个问题是，Maude的第一个版本不允许重写条件的条件规则这不允许我们当时考虑基于转换的方法作为重写，并且我们被限制为基于推理规则的方法作为重写（在这种情况下也称为转换作为判断即使在这种情况下，也有一些问题需要解决，即规则右侧新变量的出现，以及如何控制规则应用中的不确定性这些问题是通过Maude的响应能力解决的在第3节。莫德在CCS操作语义的完全可执行的实现中，以及后来在更复杂语言的一些更大的实现中，理论和实践之间存在着巨大的差距2在CCS的另一个实施中，这些相应能力的不同用途，以及在实施瓦片系统中也已经在[5，2]中进行了研究。VERDEJO和 MARTI-OLIET284现在，Maude 2.0[7]的最新实现使得重新考虑基于转换的重写方法成为可能，因为Maude 2.0确实允许在条件中重写的条件规则，其中这些重写在执行时通过内置的搜索机制解决3.因此，我们能够继续进行我们以前的项目，通过仔细重新实施在一个完全可执行的方式，CCS操作语义将转换视为重写，并在条件中使用重写的连接规则。本文详细介绍了在这第二个实现中获得的结果，并比较两个implementations。我们在这里提出，第二个实现是有点简单，因为它更接近数学教科书的操作语义表示然而，仍然需要弥合理论和实践之间的一些差距，在这种情况下，Maude 2.0中可用的新冻结属性也发挥了重要作用，如第4.2节中详细描述的那样。将运算符声明为frozen禁止重写其参数，从而提供了另一种控制重写过程的方法。虽然在本文中，我们描述了CCS操作语义的实现作为一个具体的案例研究，所提出的技术是相当普遍的，适用于不同语言的操作语义具体来说，我们已经成功地使用它们来实现LOTOS的符号语义[18]，以及Hennessy在[9]中为命令式和函数式编程语言提出的所有求值（大步）和计算（小步）语义本文的组织结构如下。 在第2节中快速回顾了CCS语法和操作语义之后，我们在第3节中总结了第一个可执行实现的主要思想。第4节回顾了我们在实现中需要的新的Maude 2.0特性，并详细描述了如何以完全可执行的方式通过条件规则重写条件来指定语义。该机制被扩展到一个弱的过渡语义的内部行动没有观察到，然后实现的Hennessy-Milner模态逻辑描述的过程，这是我们的实施项目的一个重要组成部分第5节比较了这两种实现，第6节结束时描述了一些相关的工作，包括对LOTOS的扩展和Isabelle中语义的实现3BragaMaude本身的tures也允许条件规则在条件中重写，并且已用于在Mosses的模块化结构操作语义的上下文中构建MSOS规范的解释器[13]。Maude 2.0的显著优点是通用性和高效性。关于我们在本文中的工作，我们不知道MSOS解释器是否被用于执行CCS操作语义的规范。VERDEJO和 MARTI-OLIET285L|L→L → L{|∈}L{}2CCS我们给一个非常简短的介绍米尔纳的通信系统的演算，CCS [12]。我们假设一个名称集合A;集合A=a aA的元素称为共同名称，（不相交的）联合=A A的成员是命名普通动作的标签函数aa通过定义a=a扩展为。有一种特殊的动作叫做无声动作，记作τ，用来表示系统的内部行为，特别是通过互补动作a和a来实现两个过程的同步。 而行动的集合就是τ。这组过程直观地定义如下：• 0是不执行任何操作的非活动进程• 如果α是一个动作，P是一个过程，则α.P是执行α并随后表现为P的过程。• 如果P和Q是过程，那么P+Q是可能表现为P或Q。• 如果P和Q是进程，则P Q表示P和Q通过一对普通动作a和a的同步而同时运行，并且可能进行通信。• 如果P是一个过程，f：是一个（有限的）重新标记函数，使得f（a）=f（a），则P[f]是行为与P相同但动作根据f重新标记的过程，假设f（τ）= τ。• 如果P是一个过程，而L是一个（有限的）普通函数集，那么P\L是行为像P但在L\L中的动作被禁止的过程。• 如果P是一个过程，X是一个过程标识符，X=defP是一个定义方程，其中P可以递归地涉及X，那么X是一个行为与P相同的过程。这种直观的解释可以根据图1所示的结构化操作语义来精确地进行，该语义定义了CCS过程的标记转换系统为了简化演示，我们已经假设求和和并行合成的运算符是交换和结合的，因此使用了更抽象的语法，并消除了相应规则中对对称情况的我们在Maude中定义了CCS语法，这对于下面几节中描述的语义的两种实现几乎是通用的。唯一的区别是，所有用于构建过程的非常数运算符都被定义为冻结，这是Maude 2.0的一个新特性，只在我们的第二个实现中使用。 我们将在第4.2节中解释其原因。fmodCCS-SYNTAX包含QID。排序标签动作进程ID进程。子分类Qid<标签<法。子排序Qid Label。VERDEJO和 MARTI-OLIET286f（α）一α.P−α→PP−α→PJP|Q−α→PJ|QP−α→PJP−α→PJP+Q−α→PJP−α→PJP[f]−→PJ[f]P−a→ P JQ−a→QJP |Q −τ→ P J|QJP−α→PJP\L−α→PJ\Lα/∈L<$LαX=defPX−→PJFig. 1. CCS操作语义规则EQ~~ L：标签= L：标签。op tau：-> Act.op 0：->进程。op _._ ：Act Process -> Process [frozen prec 25]。op _+_：流程流程->流程[冻结为零]35]。op _|_：工艺流程->工艺流程[冻存]30]。op _[_/_]：Process Label Label -> Process [frozen prec20]。op_\_：Process Label-> Process [frozen prec 20].endfm我们表示完整的CCS，包括（可能是递归的）通过上下文的过程定义。我们已经定义了这些上下文以及在模块CCS-CONTEXT中与它们一起工作的操作（参见附录A）。 它包括一个恒定的上下文，用于保持每个CCS规范中使用的流程标识符的 定义。3作为判决我们在这里总结了CCS操作语义的第一个实现中使用的主要思想，其中转换成为判断，推理规则成为重写[20]。CCS转换判断P−→PJ在Maude中表示为：项P--a->PJ的排序判断，以及CCS的操作语义规则被翻译成重写规则，其中结论被重写为前提的表示集，如以下示例所示：crl [res]： P\ L-- A-> P=>>最大值如果（A =/= L）且（A =/= ~ L），则P-A-> P '。rl[n]：A. P--A->P=>>最大值emptyJS.通过这种方式，我们从一个要被证明有效的转换开始，然后使用重写过程向后工作，维护必须填充的转换集，以证明初始转换的正确性初始转换可以重写为空集，当且仅当它是VERDEJO和 MARTI-OLIET287CCS操作语义中的有效转换然而，我们在使用这种方法时发现了两个问题[4]第一个是，有时候新的变量出现在前提中，而这些变量在结论中并不存在。Maude默认解释器不能直接使用这种规则;它们只能在元级别使用一种策略来实例化额外的变量。第二个问题是，有时可以应用几个规则来重写一个判决，但一般来说因此，我们必须处理整个可能重写判断的计算树，搜索其中一个分支是否导致emptyJS。在[20]中，我们通过修改语义表示（在对象级别）和通过元级别的策略控制重写过程新变量的存在通过使用显式元变量[15]来解决，这使得重写规则右侧的新变量表示的知识的缺乏变得显式显式元变量的语义必须在这些值已知时将它们绑定到具体值因此，我们引入了语义表示机制来处理这些绑定，并将它们传播到可能存在绑定元变量的其余判断修改后的表示也有规则，在右边有新的变量，但现在它们被本地化了。控制重写过程的策略（见下文）负责实例化这些变量以构建新的元变量。重写规则的非确定性应用问题通过在元级定义的一般搜索策略该策略遍历一个术语的所有可能重写的概念树，通过使用表示语义的重写规则来构建，搜索表示空判断集如果找到，则在此树的根处表示的转换是有效的CCS转换。我们还扩展了语义实现，将元变量作为进程（在此之前，我们只需要元变量作为动作）。 如果我们开始搜索策略时，判断CCS转换右侧的过程是一个元变量，如P--a-->？P，并且搜索到达空集，那么元变量？在执行动作a之后，P必须被绑定到左边过程的一步后继者P中的一个。通过扩展搜索策略，不仅可以找到到达空集的第一种方法，而且可以找到所有可能的方法，我们实现了一个函数，该函数在执行给定操作后返回进程的所有后继。这个函数随后被用于实现CCS过程的Hennessy-Milner模态逻辑[16]，通过遵循与CCS语义中相同的处理新变量和非确定性的技术，即通过定义重写4这些问题本质上与方法本身有关，而不是与Maude在实现中使用。VERDEJO和 MARTI-OLIET288|将模态逻辑判断P = Φ重写为必须满足的判断集的规则（由逻辑语义指定）[20]。必须再次使用搜索策略，现在检查模态逻辑判断是否为真。每次使用该策略时，具有定义搜索树的重写规则的模块因此，我们得到了三个层次的代表性。CCS语义规则位于第一级。它们由第二层的搜索策略控制，在第二层定义了返回进程所有后继的函数和模态逻辑语义。最后，模态逻辑语义由第三层的搜索策略控制4转换为重写在回顾了Maude 2.0的一些新功能之后，我们描述了CCS操作语义的新实现，其中转换成为重写，推理规则成为条件重写规则。4.1Maude 2.0Maude2.0是Maude的新版本，其主要特征是：更大的通用性和表现力;对更广泛的编程应用程序的有效支持;以及作为开发互联网编程和移动计算系统的关键组件的可用性[7]。 我们在这里简单地总结了以下几节中使用的新特性。重写规则可以采取最一般的形式，在重写逻辑的变体中，重写逻辑建立在隶属关系等式逻辑之上。即可以是以下形式如果t=0，则（我i=i（J2016 -05 -2200：01：01Kpk→qk）而不限制哪些新变量可以出现在右侧或条件中。规则中的条件由关联连接符f 1形成，允许方程（普通方程t = t在完全的一般性中，系统模块的执行将需要在元级控制条件和右侧中的外部变量的实例化的策略。然而，一个非常通用的系统模块类，称为可接受模块，可由Maude 2.0的默认解释器执行。本质上，容许性要求确保所有额外的变量都将通过匹配实例化[7]。当执行条件规则时，从左到右顺序地尝试满足其所有条件;但是注意，除了由于等式公理的存在而可能有许多等式条件的匹配之外，我们还必须处理这样一个事实：VERDEJO和 MARTI-OLIET289一联系我们重写条件需要搜索，包括在先前的解不能满足后续条件时搜索新的解。因此，默认的解释器支持搜索计算.search命令查找与满足某些条件的给定模式匹配的给定术语的所有重写（我们将在下面的部分中看到一些示例 搜索是通过函数metaSearch（在4.4节中使用）在元层上进行的，它接收要工作的元表示模块作为参数，搜索的起始项，要搜索的模式，边条件，搜索的类型（对于零次或多次重写，可以是'*'，对于一次或多次重写，可以是'+'，以及'！仅用于匹配范式）、搜索深度和所需的解数。它返回与模式匹配的术语、其类型以及由匹配产生的替换。Maude 2.0的另一个特性是冻结属性。当一个操作符被声明为frozen时，它的参数不能被规则重写（我们将在下一节解释为什么使用这个操作符）。请注意，使用此属性会通过不允许全等证明规则来有效地更改冻结运算符的语义4.2CCS操作语义的实现为了在Maude中实现CCS语义，将转换作为重写，我们希望将CCS转换P−→PJ解释为重写逻辑重写。然而，重写没有标签，这在CCS语义中是必不可少的因此，我们将使标签成为结果项的一部分，以这种方式获得形式P a PJ的重写，其中a PJ是一个排序为ActProcess的值，它是Process的超级排序（参见下面在本例中的确切含义）。下面的模块是一个可接受的模块[7]，因此可以直接执行，包括CCS语义实现。modCCS-SEMANTICS正在 保护CCS-CONTEXT。对ActProcess进行排序。subsort进程 ActProcess [frozen].vars L M：标签.var A：Act.vars P P ' Q Q'：过程。var X：ProcessId。* 前缀rl [n]：A. P => {A}P。* 求和crl[sum]：如果P =>{A} P '，则P + Q =>{A} P'。* 组成crl[par]：P |Q =>{A}（P '|Q）如果P =>{A}P' 。crl[par]：P |Q =>{τ}（P '|Q' ） ， 如 果 P = > { L } P ' / | Q = > { ~ L } Q ' 。* 重新标记如果P =>{L}P'，则crl [rel]：P[M/L]=> {M}（P'[M / L]）。crl [rel]：P[M/L]=>{~ M}（P' [ M / L] ） ， 如 果 P => { ~ L}P'。crl [rel]：P[M/L]=> {A}（P'[M / L]），如果P =>{A} P'/\ A =/= L /\ A =/= ~ L。* 限制crl[res]：P\L =>{A}（P ' \ L ） ， 如 果 P = > { A } P ' / \ A = / = L / \ A = / = ~L。* 定义VERDEJO和 MARTI-OLIET290−→−→−→crl [def]：X => {A}Pif（X definedIn context）/\def（X，context）=>{A}P.恩德姆在该语义表示中，重写规则具有排序递增的属性，即， 在重写t tJ时，最小类tJ大于最小类t。如果我们把我们自己限制在在可以为它们分配排序（而不仅仅是种类）的意义上，一个规则不能被应用，除非所得到的项是格式良好的，也就是说，它具有排序。例如，虽然A.P {A}P是一个正确的转移，我们不能导出（A。P）|Q（{A}P）|因为右边的项不是很好的形式。通过这种方式，重写只允许发生在过程项的顶部，而不是在项内但是在当前的Maude 2.0系统中，如果我们有重写条件和无限进程（具有无限数量的后继进程），则排序增加机制是不够的如果我们有重写条件P=>{A}Q，则尝试以任何可能的方式重写P，并将结果与模式{A}Q匹配。例如，如果P是形式（A. P '）|Q'，也重写为（{A} P'）|Q'，但结果被拒绝。当我们有递归过程时，问题就出现了，因为试图满足重写条件的内置搜索可能会变得无限而不会终止。例如，如果上面的P '是递归的，则P'=A。P'，则P被重写为（{A} P'）|Q'，（{A}{A} P'）|Q'等，尽管所有这些结果都将被拒绝，因为它们不是良好形成的。我们对这个问题的解决方案是将所有的语法操作符声明为frozen，这可以防止相应操作符的参数被规则重写;参见第2节中的模块CCS-SYNTAX。然而，当我们想知道上述过程P'的所有可能重写形式为{A}Q时，问题仍然 出 现 在 这 种 情 况 下 ， P' 被 重 写 为 {A}P' ， 而 且 被 重 写 为 {A}{A}P'、{A}{A}{A}P'等， 只有第一次重写匹配模式{A}Q。因此，我们还必须将操作符{_}_声明为冻结。总之，当我们知道搜索将不成功时，我们使用frozen属性来避免搜索过程中的无限循环，尽管搜索可能由于两个不同的原因而不成功：要么是因为构建的术语格式不好，如（{A} P '）|Q'，这就是语法运算符被冻结的原因;或者因为术语不匹配给定的模式，如{A}{A}P'，这就是{_}_被冻结的原因。一个缺点是，由于CCS-SEMANTICS中重写规则的形状和所有构造函数操作符都被声明为冻结，我们已经失去了证明流程可以执行一系列操作或跟踪的能力，因为规则只能用于获得单步后继。重写逻辑的同余规则不能使用，因为运算符被冻结，传递性规则不能使用，因为所有规则都重写为{A}Q形式的某个-事物，并且左手中没有这种模式的规则VERDEJO和 MARTI-OLIET291−→1一个k的方面想如果我们只想在模态逻辑语义的定义中使用语义，这不是问题，因为只需要一步后继然而，我们可以通过使用生成CCS转换的传递闭包的规则来扩展语义来解决这个问题，如下所示：对TProcess进行排序。子排序TProcess TProcess [frozen]. crl[refl]：[P]=>{A}Q，如果P =>{A} Q。crl[tran]：[P]=>{A}AP，如果P =>{A}Q/\[Q]=> AP。注意我们是如何使用伪操作符[_]的。如果我们在上述规则的左边不使用它，规则头部的左边和条件中的重写都将是匹配任何项的变量，然后规则本身可以用于解决其第一个条件，从而产生无限循环。此外，为了避免无用的重写，dummy操作符也被声明为frozen，例如[ A。P]的范围[ {A}P]。具有这最后两个规则的CCS的所获得的表示在给定CCS过程P的意义上是语义正确的，存在过程P1，.，P k，使得P−a→1 P−a→2··· −→Pk当且仅当[P]可以重写为{a1}{a2}... {ak}Pk（参见[10]）。通过使用Maude 2.0搜索命令，我们可以找到一个过程的所有可能的单步后继。Maude> search 'a. 'b. 0 |~ a. 0 => AP：ActProcess。溶液1（状态1）AP：ActProcess --> {~ 'a} 0|'a. 'b. 0解决方案2（状态2）AP：ActProcess -->处理。0 |~ a. 0溶液3（状态3）AP：ActProcess --> {tau}0|'b. 0没有更多的解决方案。如果我们将下面的等式添加到模块CCS-SEMANTICS中，在CCS上下文中定义递归过程eqcontext ='Proc =def 'a. 'b. 过程Maude>search [1]['Proc]=>'a}'b}'a}X：Process. 溶液1（状态5）X：过程-->“b. '过程我们已经要求Maude搜索是否有一种方法可以将术语['Proc ]重写为模式<$' a}<$'b}<$' a}X：Process。 search命令在概念树中执行广度优先搜索term [ 'Proc ]的所有可能重写，并且由于存在解决方案，因此它会找到它。VERDEJO和 MARTI-OLIET292−→−→一然而，如果我们要求搜索更多的解，搜索不会终止，因为搜索树是无限的。[联系我们✏✏✏✏✏✏✏✏✮✏//联系我们❅❅❅❅❘...{'a } 'b.' Proc{'a }{ 'b } 'Pro c { 'a }{ 'b }{ 'a }'b.'产品展 示 。4.3弱变迁语义的扩展CCS中定义的另一个重要的过渡关系，P观察τ跃迁[12]。 其定义如下：=aPJ，不P−τ→<$Q Q−→aP=aQJQJ−τ→PJPJ其中，τ表示τ的自反传递闭包，对于一般作用a，其定义如下：P−→aPJPJ−→aPJJP−→aP−P−→a PJJ在[19]中，我们按照第3节中解释的方法实现了这种语义，定义了新的判断类型，并重写了将结论重写为前提的规则。 我们必须添加元变量作为过程，因为新的过程变量出现在前提中。现在，我们想按照4.2节中描述的替代方法来实现它，将新的转换也表示为重写，即，转换P-→P将被表示为重写P-→ {a}PJ和跃迁P={a} PJ将表示为重写的P−→{{a}}PJ。我们有一个再次引入伪操作符，以防止使用新的重写规则以错误的方式验证重写条件。建议的实施方式如下：sortAct*Process ObsActProcess。op{_}*_ ：Act Process -> Act*Process [frozen].op {{_}}_：Act Process -> ObsActProcess[frozen]。排序WProcess。子排序WProcess WProcess[frozen]。op<_>：Process -> WProcess [frozen].rl[refl*]：|P |=> {tau}* P.crl [transl *]：|P| =>{tau}*R，如果P => {tau}Q/\|Q|=>{tau}*R。crl [weak]：

=> {{A}}P'if |P| =>{tau}* Q/\Q=>{A}Q' /\|Q'|=> {tau}* P'。请注意，新的语义运算符{_}*_和{{_}}_以及伪运算符，|_|和<_>被宣布为冻结，其原因已在第4.2节中解释。✏VERDEJO和 MARTI-OLIET293一P|= TTP|= Φ1Φ2i P |= Φ1和P |= Φ2P|= Φ1Φ2i P |= Φ1或P |= Φ2P|=[K]Φ iQ ∈ {PJ|P −a→ PJ<$a ∈ K}.Q |= ΦP|=Q∈ {P J|P −a→ P J<$a ∈ K}.Q |= ΦP |=[[K]]Φ i Q∈ {P J|P =a<$P J<$a ∈ K}.Q |= ΦP |= KΦ i Q ∈ {PJ|P =a<$P J<$a ∈ K}.Q |= Φ图二. 模态逻辑满足关系我们可以使用search命令来查找给定进程在执行操作“a”之后的所有弱后继进程Maude> search< tau. 'a. τ的'b. 0 > => {{'a }}AP：ActProcess. 溶液1（状态2）AP：ActProcess --> tau。'b.0溶液2（状态3）AP：ActProcess -->'b. 0没有更多的 解决方案。4.4Hennessy-Milner模态逻辑我们现在想实现Hennessy-Milner模态逻辑来描述CCS过程的本地能力[16]。公式如下：Φ：：= tt |FF |Φ 1∧ Φ 2|Φ 1∨ Φ 2|[K]Φ|联系我们|[[K]]Φ|联系我们其中，K是一组（有限）动作。描述过程P何时满足性质Φ的满足关系，P |=Φ，在图2中归纳定义。由于满意度关系的定义使用了CCS的转换我们可以尝试在同一级别上实现它，使用如下规则：rl [和]：P| = Phi/\Psi=>true if P| = Phi=>true/\P| = Psi=>true.rl[直径]：P |= Phi => true，如果P =>{A}Q/\Q |= Phi => true。这些规则是正确的，它们准确地代表了模态逻辑的满足关系所表达的内容。例如，第二个条件规则表示存在一个过程Q，使得P −→ Q且Q |= Φ，这是钻石模态算子的定义。这是因为变量Q在规则条件下是存在量化的。但是我们发现框模态算子的定义存在问题，因为它在过程的可能转换上使用了一个泛量化器。如果我们想处理所有可能的一步重写项，我们需要上升到元级别。通过使用操作元搜索，我们定义了一个操作succ，它在给定的有限集合中执行操作后返回进程的所有（元表示的）后继VERDEJO和 MARTI-OLIET294下面SUCC模块中的操作成功定义使用了两个辅助函数。allOneStep（T，N，X）的求值通过使用模块MOD（CCS-SEMANTICS的元表示）中的规则返回与模式X匹配的项T的所有单步重写（跳过前N个解决方案）。filter（F，TS，AS）的求值返回元表示进程P，使得项F[A，P]在TS中，而A在AS中。为了在项集合AS中查找项A，我们比较模块MOD中的项。 这是因为不同的元表示术语，如“a.Qid”和“a.Act”，可以在模块CCS-SEMANTICS中表示相同的动作。操作过滤器用于succ（T，TS）的定义中，以从进程T的所有后继进程中删除那些通过执行不在集合TS中的操作而到达的进程。在以一般形式定义了这些操作之后，我们可以实现wsucc操作，它返回所有具有相同操作的弱后继fmod SUCC包含META-LEVEL。op MOD：-> Module.等式MOD =对TermSet进行排序。子排序术语TermSet。op_U_：TermSet TermSet -> TermSet [aslogid：mt]. op_isIn_：Term TermSet -> Bool。op allOneStep：Term MachineInt Term ->TermSet。操作过滤器：Qid TermSetTermSet -> TermSet。op succ：Term TermSet -> TermSet.op wsucc：Term TermSet -> TermSet.var M：Module.var F：Qid.变量T T ' X：术语。var N：MachineInt.var TS AS：TermSet.等式T isInmt=false。等式Tis In（T（getTerm（MetaReduce（MOD，'_==_[T，T']））=='true.Bool）或（TisInTS）。eq filter（F，mt，AS）= mt.ceqfilter（F， X U TS，AS）=（如果T是In AS，则T ' e l s e m t f i ） U 过 滤 器（ F ， T S ， A S ） 如 果 F [ T ， T ' ] ： = X。EQallOneStep（T，N，X）=如果元搜索（MOD，T，X，nil，allOneStep（T，N +1，X）fi. eq succ（T，TS）=filter（（''{_'}_），allOneStep（T，0，'AP：ActProcess），TS）。等式wsucc（T，TS）= filter（allOneStep（<'_>[T]，0，'OAP：ObsActProcess），TS）。endfm使用操作succ和wsucc，我们等式实现了模态逻辑的满足关系注意模态运算符的语义是如何通过展开为合取或析取来定义的，其中使用了给定过程的后继者VERDEJO和 MARTI-OLIET295fmodMODAL-LOGIC保护SUCC。对HM公式进行排序。op ttff：-> HM公式。ops_/\__\/_：HM公式HM公式-> HM公式。ops<_>_'[_']_：TermSet HM公式-> HM公式。ops<<_>>_'选项'[_']']_：TermSet HMFormula -> HMFormula。opsforall exists：TermSet HM公式->布尔值。操作_|=_：项HM公式->布尔值。var P：术语。 vars K PS：TermSet.Phi Psi：HM公式。方程式P|= tt=true。方程式P|= ff= false。方程式P| = Phi/\Psi =P| = Phi和P| = Psi。方程式P| = Phi\/Psi =P| = Phi或P| = Psi。方程式P| =[K] Phi=forall（succ（P，K），Phi）. 方程式P| = Phi=exists（succ（P，K），Phi）.方程式P| =[[K]] Phi = forall（wsucc（P，K），Phi）.方程式P| = <> Phi = exists（wsucc（ P ， K ） ， Phi）. eq for all （ mt ， Phi） =true。eq for all（P U PS，Phi）= P| = Phi和forall（PS，Phi）。eq exists（mt，Phi）= false。eq 存 在 （ P U PS ， Phi ） = P| = Phi 或 存 在 （ PS ，Phi）。endfm使用[16]中的两个例子，我们展示了如何在Maude中证明模态公式被CCS过程满足。第一个示例涉及在CCS上下文中定义的自动售货机eq context =（'Ven =def '2p. 'VenB + ' 1页。’VenL)= def'big.'collectB.'&Ven ） （ 'VenL=def'little.'collectL.'V e n ）。进程如果投入2便士的硬币，可以按下大按钮，收集大物品如果投入一枚1便士的硬币，可以按下小按钮，收集一件小在物品被收集之后，自动售货机返回到初始状态。它满足了在存入硬币并按下按钮后，可以收集物品（或大或小）。Maude> red“Ven.Qid |= [''1p.Act + ''2p.Act ] [ ''big.Act + ''little.Act]<''collectB.Act+''collectL.Act>tt.结果Bool：true第二个例子涉及铁路道口系统，具体如下：eqcontext= （ 'Road =def 'car. “ 起 来。 ~ cross. ~' 下 来。 '&Road ） （ ' Rail=def“ 火 车 。 “ 绿 色 。 ~'tcross.~' 红 色 。 '&Rail）（' Signal =def ~ '绿色。“红色。“信号+ ~”上升。“放下。'&Signal）（' Crossing =def（（'Road|（'铁路|' 信 号 ） ）"该系统由三个部分组成：道路、铁路和信号。Action- tionscarandtrain表示汽车和火车的接近，向上打开VERDEJO和 MARTI-OLIET296门为汽车，ccross是汽车通过，关闭门，绿色是火车收到绿色信号，tcross是火车通过，红色设置红灯。“穿越”过程Maude>red“Crossing. Qid| =[[''car.Act]][[''train.Act]]（（<<<<'~_''ccross.Act]>>tt）\/（'~_''tcross.Act]>>tt））。结果Bool：trueMaude>red“Crossing. Qid| =[[''car.Act]][[''train.Act]]（（<<<<'~_''ccross.Act]>>tt）/\（'~_''tcross.Act]>>tt））. 结果Bool：falseMaude 2.0在解决最后一个命令时需要0.5秒在Maude的第一次实施，需要10分钟。利润是相当可观的。我们将在下一节中比较这两种实现。5两种方法我们认为第二种实施方式有几个优点。 这种实现更接近于语义的数学、逻辑表示。一个操作语义规则建立了如果前提中的转换是可能的，则结论中的转换是可能的，并且这正是具有重写条件的条件重写规则的解释第一种方法需要辅助结构，如要证明有效的判断的多集，以及生成新元变量和当它们的具体值已知时传播它们这迫使我们在元级实现一种搜索策略，检查给定的多集是否可以归约为空集，并在每次需要时生成新的元变量正是新的元变量的必要性使得策略不可避免。即使我们在前面的语义实现中使用Maude 2.0，我们也不能使用Maude2.0的search命令，因为它不能处理在右侧有新变量的重写规则，只要它们不受任何条件的约束，这就是第一个实现中发生的事情[20]。在第二种实现中，搜索的必要性出现在重写条件中，但Maude 2.0系统解决了这个问题，因为它能够处理这些条件以及在某些条件下绑定的新变量。在对象级（语义表示的级别）和元级（通过使用反射）完成的事情中也存在差异在第一个实现中，搜索策略遍历概念树，其中包含术语的所有可能重写，在对象层和元层之间连续移动。在本文描述的实现中，搜索完全发生在对象级别，这使得它更快，更简单。VERDEJO和 MARTI-OLIET2976相关工作遵循本文中描述的两种方法，我们还实现了Full LOTOS的符号语义[3]，它比CCS复杂得多在第一个实现中，转换被表示为判断，我们在几个方向上改进了第3节中提出的想法为了避免模交换的多重匹配，我们将判断集改为判断序列。这意味着判决将被排序，他们将被证明从左到右。我们还改变了搜索策略，以便每次只重写第一个判断。由于它必须检查所有的判断都可以重写为空序列，如果第一个判断不能重写，它不需要重写其余的判断，它可以丢弃所有的序列。当然，这可能与语义规则中前提的书写方式不同;判断的归约不应该要求由后面（右边）的判断产生的绑定第二个实现[18]，其中转换表示为重写，不需要关于效率的改进。在LOTOS符号语义中，使用了语法替换的概念，其中LOTOS变量或数据表达式被替换为过程表达式中的- other变量当我们实现语义时，我们不能完全用等式定义这