异步π演算Maude2.0中可执行规范及测试的操作语义、迹和may测试的规范

261--理论计算机科学电子笔记71（2003）网址：http://www.elsevier.nl/locate/entcs/volume71.html21页异步Pi演算语义的可执行规范及Maude2.0Prasanna Thatia，1，Koushik Sena，1和Narciso Mart 's-Olietb，2a美国伊利诺伊大学香槟分校b人口与发展部。deSistemasInform'atic osyProgramaci'on，西班牙马德里康普顿斯大学摘要我们描述了一个可执行的规范的操作语义的异步版本的π演算在Maude的条件重写规则重写的条件。我们还提出了一个可执行的规范，可以测试非递归异步π演算过程的等价性，使用Maude元级。具体地说，我们描述了我们使用元搜索操作来计算非递归过程的所有有限迹的集合，并根据异步π演算中可以测试的特征化的前序关系来比较两个过程的迹集合。因此，在操作语义和may测试的规范中，我们大量使用了Maude语言和系统2.0版本中引入的新功能。关键词：π-演算，可积性，可检验，迹，Maude1介绍自从Milner、Parrow和Walker在开创性的论文[11]中引入π演算以来，π演算已经成为基于名称的进程移动性研究最多的演算之一，其中进程能够通过通道交换名称，以便通信拓扑可以在计算期间改变。π演算的运算语义已经被定义为遵循两种主要风格的几个第一种是根据Plotkin [13]引入的SOS方法的标记转换系统风格。第二种是归约式，首先，1电子邮件：thati，cs.uiuc.edu2 电子邮件地址：narciso@sip.ucm.es2003年3月，出版社dbyElsevierScienceB。 V.操作访问和C CB Y-NC-N D链接。THATI，SEN，ANDMARTI-OLIET262语法过程（通常使语法更加抽象，某些运算符的结合性和/或交换性的性质），然后某些归约或重写规则表示计算如何通过进程之间的通信进行。重写逻辑中的π演算运算语义的第一个规范是由Viry在[19]中开发的，在Elan [6]中使用de Bruijn索引，显式替换和归约策略的归约风格。后来Stehr[14]通过使用显式替换的通用演算（称为CINNI）改进了这种表示，CINNI结合了基于标准变量和de Bruijn指数的最佳方法，并已在Maude中实现。我们的工作以上面描述的工作为起点，以及Verdejo和Mart 's-Oliet[18]最近的工作，展示了如何使用Maude 2.0的新特性来实现CCS的标记转换系统风格中的语义。这项工作主要利用了条件重写规则，在条件中进行重写，使得形式为P1→ Q1.. 。P n→ Q nP0→Q0成为一个条件重写规则的形式P0−→ Q0如果P1−→ Q1. Pn −→ Q n，其中条件包括重写。 这些规则可以在Maude语言和系统的2.0版本中执行[7]。然而，这还不够，因为必须对规则的适用进行某种控制。通常，重写规则可以应用于术语中的任何地方，而CCS或SOS风格中的π演算的操作语义中的转换仅发生在顶部。Maude 2.0中提供的新的frozen属性使这成为可能，因为将操作符声明为frozen禁止重写其参数，从而提供了另一种控制重写过程的方法。应用条件规则时的重写条件通过隐式搜索过程来解决，该过程也可供用户在指挥级和元级。search命令查找与满足某些条件的给定模式匹配的给定项的所有重写。搜索在元级别被具体化为操作元搜索。通过这种方式，我们的第一个贡献是一个完全可执行的规范，在标记的转移系统风格的操作语义的异步版本的π演算（同步情况下的语义是作为一个简单的修改获得）。该规范使用条件重写规则，在条件中重写，以及CINNI演算[14]用于管理π演算中的名称和绑定。然而，这两个要素不足以获得完全可执行的规范。要克服的一个中心问题是，一个项的转换可以无限分支。例如，项x（y）.P可以通过输入动作演化为无限族中的一个：THATI，SEN，ANDMARTI-OLIET263±取决于在通道x处的输入中接收到的名称的术语。我们的解决方案是定义流程相对于执行环境的转换。环境被抽象地表示为一组自由（全局）名称，环境可以使用，同时与过程进行交互，和转换被建模为重写规则对包括一组环境名称连同一个过程。我们的下一个贡献是在有限（非递归）异步π演算过程之间实现may-testing前序[12，3，5]的验证，再次使用[18]中的思想来计算过程的所有有限迹的集合。五月测试是π演算过程行为等价性概念的一个具体实例;在五月测试中，如果两个过程在所有实验中具有相同的成功属性，则称它们是等价的。一个实验由一个并行运行的观察过程组成，并与被测过程相互作用，成功被定义为观察者发出一个特殊事件的信号。将事件的发生视为某种不良事件的发生，可以使用测试来推断安全属性[4]。由于可能检验的定义涉及对所有观察者的普适量化，因此很难直接从定义中建立过程等价。作为一种解决方案，已经找到了等价的替代表征，这些等价不依赖于观察者的量化。众所周知，迹语义是（同步）π -演算中的may测试的替代表征[3]，而迹语义的变体已经被证明可以在异步设置中表征may测试[5]。具体地说，在这两种情况下，根据may-testing前序比较两个过程相当于比较它们展示的所有有限迹的集合。我们已经为有限异步进程实现了[5]中提出的迹集比较。我们强调，我们选择指定异步版本而不是同步π演算，是因为异步情况下的可能测试的特征更有趣和困难。同步版本可以使用类似但更简单的技术以可执行的方式指定。我们获得可执行的测试规范的第一步是求出给定过程的所有有限迹的集合。这是在Maude元级别通过使用元搜索操作来收集重写给定术语的所有结果来完成的。第二步是指定迹之间的一个前序关系，它表征了可能的测试。我们已经将迹前序关系表示为重写关系，即定义迹前序的推理规则再次被建模为条件重写规则。最后第一步是检查两个进程是否通过may前序相关，即形式为P Q的语句是否为真。 这一步涉及计算在跟踪-前序关系下的跟踪的闭包，同样通过元搜索操作。因此，我们的工作证明了Maude 2.0中新的元级设施的实用性。本文的结构遵循上述描述中的步骤。次THATI，SEN，ANDMARTI-OLIET264----第2节描述了我们考虑的异步版本的π演算的语法，以及我们使用的相应CINNI操作。第3节描述了通过条件重写规则指定的操作语义。第4节和第5节定义了迹和迹上的前序，re-order。最后，第6节包含对上述过程的可能测试的规范。第7节总结了本文，并简要讨论了未来的工作。虽然本文包含了一些关于π演算的信息，并可能进行测试以使其尽可能独立，但我们建议读者参考论文[5，3，11]以了解这些主题的完整细节。同样，感兴趣的读者可以在[7]中找到关于Maude 2.0新特性的详细解释，以及在同伴论文[18]中找到关于它们在操作语义实现中的使用的详细解释。2异步π演算下面是对异步π演算的一个版本的简短而非正式的回顾，它配备了一个用于匹配名称的条件构造。假设信道名称的无限集合，并且u、v、w、x、y、z、. 。。 被P，Q，R覆盖的过程集合由以下语法定义：P：= xy| Σi∈Iα i.P i|P1|P2|[x = y ]（P 1，P 2）|！|! P其中α可以是x（y）或τ。输出项xy表示与目标x相同的同步消息，内容y. 求和i∈Iαi.Pi非确定性地选择一个αi，如果αi=τ，则它内部演化为Pi，如果αi=x（y），则它接收一个在通道x处的任意名称z，然后表现得像Pz/y。过程Pz/y是将P中y的自由出现替换为z的结果，通常对绑定名称进行重命名以避免意外捕获（因此替换仅定义为模α等价）。x（y）.P中的自变量y绑定了P中y的所有自由出现。组合物P1|P2是由P1和P2并行作用而成. 组件可以独立工作，也可以相互交互。限制（νx）P的行为类似于P，除了它不能与它的环境交换以x为目标的消息限制约束x在P中的自由出现。条件[x=y]（P1，P2）在x和y相同时表现为P1，否则表现为P2复制！P提供P的无限数量的拷贝。自由名称的函数fn（. ）、绑定名称bn（. ）和名称n（. ），一个过程，被定义为预期的。在随后的π演算语法的Maude规范中，sortChan用于表示通道名称，并且每个非常量syn- tax构造函数都被声明为frozen，因此相应的参数THATI，SEN，ANDMARTI-OLIET265不能被规则重写;这将在第3节结束时得到证明。排序陈。sort Guard GuardedTrm SumTrm Trm.子排序GuardedTrm< SumTrm.Subsort SumTrm< Trm.op_（_）：Chan Qid ->Guard. op tau：-> Guard.opnil ：-> Trm.op_<_> ：Chan Chan-> Trm [frozen].op_._：Guard Trm -> GuardedTrm [冻结]。op_+_ ：SumTrm SumTrm-> SumTrm [frozenasynchronous]. 操作_|_：Trm Trm-> Trm [冷冻冷藏]。opnew[_]_ ：Qid Trm-> Trm [frozen].opif_=_then_else_fi：Chan Chan Trm Trm-> Trm[frozen]. OP！_：Trm-> Trm [冻结]。请注意，Σi∈Iαi.Pi被分为三种情况：(i) nil表示I=0的情况，(ii) 排序为GuardedTrm的项表示I={ 1}的情况，并且(iii) 排序项SumTrm表示I =[1.. n]，n> 1。 由于构造函数+是associative，并且排序GuardedTrm是我们可以表示一个有限和···αn.Pn）。i∈Iα i.P ias（... （α1.P1+ α2.P2）+为了在语言级别上表示π演算过程（和迹，见第4节）上的替换，我们使用CINNI作为显式替换的演算[14]。 这给出了具有绑定和无捕获替换的术语的一阶表示，而不是去元层处理名称和绑定。这种表示的主要思想是保持绑定名称在绑定器中的原样，但将其使用替换为名称后跟索引，该索引是在到达使用位置之前跳转的具有相同名称的绑定器的数量按照这个想法，我们将排序Chan的项定义为索引名称，如下所示。排序陈。op_{_}：Qid Nat -> Chan [prec 1]。我们引入一种替换Subst以及以下操作：操作[_：=_]：Qid Chan->Subst. op [shifting_]：Qid->Subst. op [shiftdown_]：Qid-> Subst.op [lift]：Qid Subst -> Subst.前两个替换是基本替换，代表简单替换和移位替换;第三个替换是简单替换的特殊情况;最后一个表示复杂替换，其中替换可以使用算子提升。这些操作 的直观意义THATI，SEN，ANDMARTI-OLIET266[a：= x][shifa][shiftdown a][lifta S]a{ 0} ›→ xa{ 0} ›→ a{ 1}a{ 0} ›→ a{ 0}a{ 0}›→ [移位a]（Sa{ 0}）a{ 1} ›→ a{ 0}a{ 1} ›→ a{ 2}a{ 1} ›→ a{ 0}a{ 1}›→ [移位a]（Sa{ 1}）············a{ n+1} ›→a{ n}a{ n} ›→a{ n+1}a{ n+1} ›→a{ n}a{ n}›→ [shiftinga]（Sa{ n}）b{m}›→ b{m}b{m}›→ b{m}b{m}›→ b{m}b{m}›→[shiftupa]（Sb{m}）表1CINNI行动如表1所示（更多详细信息请参见[14]）。使用这些，明确的替代π演算过程的定义方程。下面是一些有趣的方程等式S（P + Q）=（S P）+（S Q）。等式S（CX（Y）.P）=（S CX）（Y）。（[lift Y S] P）.等式S（new [X] P）= new [X]（[lift X S] P）。3操作语义一个标号的转移系统（见表2）被用来给出[5]中演算的一个运算性质。转移系统定义为过程的模α-等价，因为α-等价过程具有相同的转移。规则COM、CLOSE和PAR具有表中未显示的对称版本。转换标签，也称为动作，可以有五种形式：τ（无声动作），xy（带有目标x和内容y的消息的自由输出），x（y）（绑定输出），xy（消息的自由输入）和x（y）（绑定输入）。函数fn（. ）、bn（. ）和n（. ）定义为预期的动作。所有可见（非τ）动作的集合由L表示，α被假设为在L. 作为自由动作和束缚动作的统一表示法，采用了以下表示法：（x）xy=xy，（{y}）xy=x（y），输入动作也采用了同样的表示法。 变量z假定为在{z，{z}}范围内。如果z <$={ z }，则项（νz<$）P是（νz）P，否则P是（νz）P。我们定义排序Action和相应的操作如下：排序操作类型。opsio：->对象类型。op f：键入Chan Chan -> Action。opb：键入Chan Qid -> Action。optauAct：-> Action.运算符f和b用于构造自由动作和约束动作re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-THATI，SEN，ANDMARTI-OLIET267re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-re-动作上的名称替换如预期的那样被等式定义表2中的推理规则被建模为条件重写规则THATI，SEN，ANDMARTI-OLIET268表2异步π演算的标号转移系统以前提作为规则的条件。[3]由于重写不像带标签的转换那样有标签，我们将标签作为结果项的一部分;因此，对应于操作语义中转换的重写的形式为P<${α}Q。由于INP和OPEN规则，一个项的转换可以无限分支。具体来说，在INP规则的情况下，对于输入中可以接收的每个可能的名称都有一个分支。在OPEN规则的情况下，每个名称都有一个分支，用于表示正在发出的私有通道（请注意，转换规则仅定义为模α等价）。为了克服这个问题，我们定义了[CS] P形式的转换对，其中CS是一组通道名称，包含与进程交互的环境所知道的所有名称。当进程和它的环境之间交换私有名称时，在绑定的输入和输出交互期间，集合CS会由于INP规则而导致的无限分支通过只允许在自由输入中接收环境集合CS中的名称来避免。由于CS被假定为包含环境中的所有自由名称，因此不在CS中的输入参数将是环境的私有名称。 现在，由于选择用来表示新名称的标识符是不相关的，因此所有绑定的输入3表中缺少的对称版本不需要实现，因为该过程构造函数+和|都是可交换的ΣINP：i∈I α.Pi−→P{X zJ我J z/y}j∈I，α=x（y）J J输出：xy−→0XYXYΣTAU：τi∈I α .P−→我我Pj∈I，α=τJJP−→BINP：P Jx（y）P PJy∈/fn（P）PAR：P1−→P1JP1|P2−→ P1J|P2αααbn（α）<$fn（P）=<$2P1−→COM：−→XY P1JP2−→XYP2JP1|P2−→ P1J|P2Jτ结果：P−→PJα（νy）P−→（νy）PJXYy∈/n（α）打开：x（y）（νy）P PJP−→ PJx=/y−→x（y）关闭：P1−→P1JP2−→XYP2Jατy∈/fn（P）2P|！P−→PJ代表：如果：P1|P2−→（νy）（P1J|P2J）P−→PJα[x=x]（P，Q）−→PJαα！P−→PJα否则：α[x=y]（P，Q）−→QJQ−→QJx/=yTHATI，SEN，ANDMARTI-OLIET269------转换可以被识别为单个输入。通过这些简化，项的输入转换的数量变得有限。类似地，在OPEN规则中，由于选择用来表示发出的私有名称的标识符是不相关的，因此仅在所选名称中使用标识符的规则的实例不会被区分。我们只详细讨论了几个推理规则的实现;读者可以参考附录来获得表2中所有重写规则的完整列表。排序环境跟踪。子排序EnvTrm EnvTrm [frozen].op{_}_：Action TraceTrm-> TraceTrm [frozen].请注意，这两个操作符也在上面用冻结的属性声明，禁止以这种方式重写它们的参数，正如本节末尾所述下面的无条件规则是针对自由输入的。rl [Inp]：[CYCS]（（CX（X）. P）+ SUM）=>{f(i，CX，CY）}（[CY CS]（[X：= CY] P））。我们考虑的下一个规则是约束输入。由于选择用来表示绑定参数的标识符是不相关的，因此我们对所有绑定输入使用常量'U'，因此'U 0表示接收到的新通道。注意，与表2的BINP规则相反，我们不检查“U 0”是否在执行输入的进程的自由名称中，而是在规则的右侧和条件中的环境名称CS和进程P的集合中适当地上移通道索引。这是合理的，因为转换目标在输入操作中的绑定名称的范围内。还要注意，动作中的通道CX没有下移，因为它超出了绑定参数的范围。环境名称集通过添加接收到的通道'U 0来扩展。最后，我们使用一个特殊的常量标志sort Chan来确保终止。我们将flag的实例添加到rewrite in condition的环境集，以便在评估条件时不会再次触发BINP规则。如果没有这个检查，我们将有一个非终止的执行，其中BINP规则被反复触发。crl[BInp]：[CS] P => {b（i，CXif（not flag inCS）/\CS 1：=标志[CS 1][移位'U] P => {f（i，CX，' U {0}）} [CS 1] P1。下面的规则处理绑定输出的情况crl[Open]：[CS]（new [X] P）=> {[shiftdown X] b（o，CY，X）} [X{0} CS1]P1ifCS1：= [shiftdownX] CS/\[CS1] P => {f（o，CY，X{0}）} [CS1] P1/|X{0} =/= CY。与绑定输入的情况一样，我们将所有绑定输出标识为单个THATI，SEN，ANDMARTI-OLIET270----在这种情况下，出现在限制中的标识符X被选择为绑定参数名。注意，在规则的右侧和条件中，CS中的通道的索引向上移动，因为它们被有效地移动穿过限制。 类似地，规则右侧的动作中的通道索引被向下移动，因为动作现在已经被移出了限制范围 另请注意，将添加导出的名称 因为接收此导出名称的环境可以在后续交互中使用它。PAR推理规则由两个重写规则实现，一个用于所执行的动作是自由的情况，另一个用于动作是绑定的情况。后一种情况的重写规则将在下面讨论，而前一种情况的重写规则更简单，并出现在附录中varIO：类型crl[Par]：[CS]（P |Q）=>{b(IO，CX，Y）} [Y{0}（[移位Y] CS）]（P1 |[shiftingy] Q）如果[CS] P =>{b（IO，CX，Y）}（[CS 1] P1）。请注意，表2中PAR规则的附加条件是通过向上移动Q中的通道索引来实现的，它可以避免将发出的绑定名称与Q中的自由名称混淆。这是合理的，因为规则的右侧在绑定输出操作的范围内。类似地，环境中的信道索引也向上移位。此外，通过添加扩展的通道Y{0}来扩展环境名称的集合。最后，我们考虑CLOSE的重写规则。进程P发出一个绑定名Y，它被进程Q接收。由于转换后Y的作用域包括Q，因此在规则的第二个条件中涉及Q的重写是在发出的绑定名称的作用域内执行的。 这通过将通道Y 0添加到环境名称集合中并在重写中向上移动CS和Q中的通道索引来实现。注意，由于正在交换的私有名称没有发送到环境，我们既不扩展规则右侧的集合CS，也不上移其中的信道索引。crl [关闭]：[CS]（P| Q）=> {tauAct} [CS] new [Y]（P1|Q1）如果[CS] P =>{b（o，CX，Y）}[CS1] P1/1，[Y{0}[移位Y] CS][移位 Y] Q =>{f(i，CX，Y{0}）} [CS2] Q1。我们以以下注释结束本节。操作符被声明为冻结，因为对封装的过程项的进一步重写从某种意义上说，TraceTrm是无用的。这是因为转换规则的所有条件只涉及一步重写（这些重写的右侧只能匹配具有单个操作前缀的排序TraceTrm项）。进一步注意，为了防止将一个项重写为非良构项，π演算项的所有构造器（第2节）都被声明为冻结;如果没有这个声明，我们将重写例如formP|Q=>{A}. P1|Qtoanonwell-formed d term.THATI，SEN，ANDMARTI-OLIET271ββ4踪迹语义这是一个很好的选择。 函数f n（. ）、bn（. ）和n（. ）的方法推广到L. 迹线的α-等价关系如预期的那样被定义，并且α-等价迹线不被区分。关系=表示− τ →的自反传递闭包，而= τ表示= τ −→= τ。s l sJ sF或s=1。sJ，我们电感定义P=PJasP==PJ。WeuseP=0对于某些P j，对于P=PJ，一个过程的轨迹集展品是[|P|]={s|P={s}。在实现中，我们引入了一个排序Trace作为Action的超排序来指定痕迹。subsort操作<跟踪。操作符：->Trace。op_._ ：Trace Trace -> Trace [aslogid：]。op[_]：Trace -> TTrace。我们定义运算符[ ]来表示一个完整的迹。这样做的动机是限制方程和重写定义在迹上的规则，使其只对完整的迹而不是其中的一部分进行操作。请注意，在跟踪TR1.b（IO，CX，Y）.TR2中，操作b（IO，CX，Y）绑定TR2中的标识符Y。ceq [TR 1. b（IO，CX，Y）. TR2]=[TR1 。b（IO，CX，'U）. [Y：=如果Y=/='U.因为运算符op{ }：ActionTraceTrm -> TraceTrm被声明为冻结，一个排序EnvTrm的项只能重写一次，所以我们不能通过简单地以所有可能的方式重写多次来获得进程的有限迹集。如[18]中所述，通过使用如下生成一步转换的传递闭包的规则来指定迹语义来解决该问题排序TTrm。op[_]：EnvTrm-> TTrm [frozen].var TT：TraceTrm.如果P => {A} Q，则crl [px]：[P]=>{A}Q。crl [transs]：[P]=> {A} TT如果P =>{A}Q/I[Q]=>TT/I[Q]=/=TT。我们使用运算符[ ]来防止无限循环，同时评估上述规则的条件。如果不使用这个运算符，那么条件中重写的左侧将匹配规则本身的左侧，因此可以使用规则本身来求解其条件。这个操作符也被声明为frozen，以防止在[ ]中进行无用的重写。我们现在可以使用Maude 2.0的搜索命令来查找进程的所有可能的痕迹。迹线作为[[CS] P]形式的TTrm的一步后继的前缀出现。例如，所展示的THATI，SEN，ANDMARTI-OLIET272关于我们⇒通过[mt]new 'y]（'x0 'y0<>|' x0（' u）。nil）（其中mt表示空信道集），可以通过使用下面的搜索命令来获得。Maude> search [ [mt] new 'y]（'x {0} 'y{0}<>|'x{0}（' u）。nil）]=>！X：TraceTrm。在APITRACESET中搜索：[[mt]new <'y]（' x {0} 'y{0}>|'x{0}（' u）。nil）]=>！X：TraceTrm。溶液1（状态1）状态：7次重写：17344在110 ms CPU（150 ms real）（157672重写/秒）X：TraceTrm--> {b（i，'x{0}，'u）}'u {0}]new' y]（nil|“ ）溶液2（状态2）状态：7次重写：17344 in 110 ms cpu（170 ms real）（157672rewrites/second）X：TraceTrm --> {tauAct}[mt]new tau 'y]（nil|无 ）解决方案3（状态3）状态：7次重写：17344次，110 mscpu（170 msreal）（157672次重写/秒）X：TraceTrm--> {b（o，'x{0}，'y）}'y {0}]nil|'x{0}（' u）。 无溶液4（状态4）状态：7次重写：17344次，110 mscpu（170 msreal）（157672次重写/秒）X：TraceTrm-->{b（i，'x{0}，'u）}{b（o，'x{0}，'y）}{b（o，'x{0}，'y）}{y {0} 'u{0}] nil|无溶液5（状态5）状态：7次重写：17344次，110 mscpu（170 msreal）（157672次重写/秒）X：TraceTrm-->{b（o，'x{0}，'y）}{b（i，'x{0}，'u）}{b（i，'x{0}，'u{0}] nil|无溶液6（状态6）状态：7次重写：17344在110 mscpu（170 msreal）（157672次重写/秒）X：TraceTrm--> {b（o，'x{0}，'y）}{f（i，'x{0}，'y{0}）}'y {0}]nil|无没有更多的解决方案。状态：7次重写：17344，110 msCPU（170 ms real）（157672次重写/秒）该命令返回所有可以从给定TTr m到达并且正在终止的TraceTrm（"！“i n =>！ （S表示目标应该终止）。所需的一组轨迹可以通过简单地提取，ING从每个解决方案a1. 一个 TT序列a1...并删除其中的所有tauAct，从而得到了异步π演算迹语义的可执行规范.5一种基于迹线的May测试may测试框架[12]在异步π演算上实例化如下。观察者是可以发出特殊消息µµ的进程。我们说是的。µµ如果O=，则一个观察者verO接受跟踪s，其中s是通过补充s中的动作，即将输入动作转换为输出动作，反之亦然。可预序±过过程被定义为：P±Q，如果对于THATI，SEN，ANDMARTI-OLIET273µµ µµ每个观察者O，P|O =蕴含Q|O= 0。 我们说P和Q可以-THATI，SEN，ANDMARTI-OLIET274±±≤≤≺·（Drop）s1. （y）s2s1。（y）xy。s2 if（y）s2/=（延迟）s1。（y）（α. xy. s2）1. （y）xy。α。s2if（y∈）（α. xy. s2）/=0（Annihilate）s1. （y）s2s1。（y）xy。xy. s2if（y）s2=/表3迹上的前序关系等价，即P = Q，如果PQ和QP。在这个定义中，对上下文的普遍量化使得直接从定义中证明等式非常困难，并且使得机械检查成为不可能。 为了避免这个问题，在[5]中提出了一种基于迹的可能等价的替代表征。我们现在总结这个特征并讨论我们的实现。迹上的前序≤定义为表3中的迹的自反传递闭包，其中不存在（y_n）·被扩展到迹为如下（y）s=sifyx（y）= 0. s2 ify={y}，并且有s1，s2， x，s=s1.xy.s2且y/∈n（s1）<${x}否则，对于迹的集合R和S，我们定义R4S，如果对于每个s∈S，存在r∈R使得r≤s。 在[5]中，may前序被描述为： P±Q当且仅当[|Q|] 4 [|P|].前序背后的主要直觉如果观察者接受一个跟踪s，那么它也接受任何跟踪r s。 前两条定律指出，观察者不能在被测试的过程上强制输入。 由于输出是异步的，观察者展示的跟踪中输出之后的动作不需要因果地依赖于输出。因此，观察者的输出可以被延迟，直到一个因果相关的动作，或下降，如果没有这样的动作。湮灭定律指出，观察者可以消耗自己的输出，除非有后续的行动取决于输出。读者可参考[5]以了解有关此特征的更多详细信息我们将跟踪前序编码为基于排序TTrace的重写规则完整迹的;具体地说，关系r s如果cond，被编码为s=>r ifcond.这种表述形式的理由将在第6节中说明。迹线上的函数（y）由操作bind等式定义。bind操作使用sortTrace的常量bot来发出错误信号。opbind：Qid Trace ->Trace。opbot：->Trace.varTR：Trace.varIO ：变量类型。THATI，SEN，ANDMARTI-OLIET275----关于我们联系我们齐克河如果t =/= 0，则bot =bot。ceq机器人。如果t =/=0， 则 TR = bo t。eqbind（X，n）= n.eqbind（X，f（i，CX，CY）. TR）=如果CX=/=X{0}，则如果CY == X{0}，则（[shiftdownX] b（i，CX，X））。TRelse（[shiftdownX] f（i，CX，CY））. bind（X，TR）fi否则就下图。eqbind（X，b（IO，CX，Y）. TR）= 如果CX =/= X{0}，则如果X=/=Y，则（[shiftdown X] b（i，CX，Y））。bind（X，TR）else（[shiftdown X] b（IO，CX，Y））. bind（X，swap（X，TR））fi否则就下图。对于绑定的第二个参数以自由输出开始的情况，没有显示等式，因为它是类似的。注意，通道索引在动作中，直到第一次出现X 0作为自由输入的参数，当它们移出绑定器X的作用域时，将向下移动。此外，当遇到以X作为绑定参数的绑定操作时，交换操作将应用于跟踪的剩余sunix。交换操作只是简单地改变suprix中的通道索引，即使活页夹X在装订动作中移动，也不会改变。这是通过同时将X 0替换为X 1和将X 1替换为X 0来实现的。最后，请注意，当遇到X 0作为自由输入的参数时，该输入将转换为绑定输入。如果在任何其他地方第一次遇到X 0，则通过返回常量bot来发出错误信号。迹上的前序关系的编码现在是直接的。crl[Drop]：[TR1. b（i，CX，Y）.TR2]=>[TR1. bind（Y，TR2）]如果bind（Y，TR 2）=/= bot.rl[延迟]：[（TR1. f（i，CX，CY）. b（IO，CU，V）。TR2）]=>[（TR1. b（IO，CU，V）。（[shiftv]f（i，CX，CY））.TR2）]。crl [延迟]：[（TR1. b（i，CX，Y）. f（IO，CU，CV）. TR2）]=>[（TR1. bind（Y，f（IO，CU，CV）. f（i，CX，Y{0}）.T R 2 ）]如果bind（Y，f（IO，CU，CV）. f（i，CX，Y{0}）.TR2）=/= bot。crl [歼灭]：[（TR1. b（i，CX，Y）. f（o，CX，Y{0}）.TR2）]=>[TR1. bind（Y，TR2）]如果bind（Y，TR 2）=/= bot.注意，在第一个Delay规则中，当自由输入动作在绑定动作上被延迟时，它的通道索引会上移，因为它进入了绑定参数的作用域。类似地，在第二延迟规则中，当绑定输入动作跨自由输入/输出动作延迟时，自由动作的通道索引通过绑定操作向下移位。延迟规则的其他两个子情况，即，其中自由输入是在自由输入或输出上被延迟的情况下，以及在绑定输入或输出上被延迟的情况下，由于它们是类似的，因此未示出THATI，SEN，ANDMARTI-OLIET276| || || |||类似地，对于Annihilate，没有示出自由输入将与自由输出一起被湮灭的情况。6有限过程之间的May预序我们现在描述我们通过利用第5节中讨论的may测试的基于迹的特征来验证有限进程之间的may前序的实现，即没有复制的进程。过程P的有限性只意味着[P]中迹的长度是有界的，但是[P]中迹的数量可以是无限的（甚至模α等价），因为INP规则是无限分支的。为了避免在有限集合中进行比较的问题，我们观察到，[|Q|]4[|P|[如果且仅如果]|Q|]fn（P，Q）4[|P|]fn（P，Q），其中，对于迹集S和名集ρ，我们定义S ρ={s∈S|fn（s）ρ}。现在，由于[|P|]及[|Q|]是有限长的，则迹s[P]fn（P，Q）与迹s[Q]fn（P，Q）的集合是有限模α-等价的.事实上，通过第3节中描述的我们的实现为[[fn（P，Q）] P]生成的迹集包含[fn（P，Q）]P]的一个代表性的|P|]fn（P，Q）.给定过程P和Q，我们利用Maude 2.0的元级能力生成[[fn（P，Q）] P]和[[fn（P，Q）] Q]的所有迹（模α-等价）的集合如第4节所述，这些术语属于TTrm类，只能重写一次。通过重写获得的排序TraceTrm项包含一个有限迹作为前缀。 为了创建所有轨迹的集合 ， 我 们 计 算 所 有 可 能 的 单 步 重 写 。 该 计 算 在 元 级 由 函 数TTrmtoNormalTraceSet完成，该函数使用两个辅助函数TTrmtoTraceSet和TraceSettoNormalTraceSet。op TTrmtoTraceSet：Term -> TermSet。操作TraceSettoNormalTraceSet：TermSet ->TermSet。opTTrmtoNormalTraceSet：Term ->TermSet。等式TTrmtoNormalTraceSet（T）= TraceSettoNormalTraceSet（TTrmtoTraceSet（T））。函数TTrmTraceSet使用函数allOneStepAux（T，N）返回项T的所有一步 重 写 的 集 合 （ 根 据 第 3 节 和 第 4 节 中 的 规 则 ， 这 些 规 则 在 名 为APISEMANTICS和APITRACE的模块中定义，参见附录中的图A.1），项T是排序TTrm项的元表示，跳过前N个解决方案。在下面的等式中，运算符u代表集合并。注意操作MetaSearch的使用，它接收元表示模块的参数、搜索的起始项、搜索的模式、边条件（在本例中为空）、搜索的类型（对于零次或多次重写，可以是'*'，对于一次或多次重写，可以是'+'，对于一次或多次重写，可以是'！仅用于匹配范式）、搜索深度和所需的解数。它返回与模式匹配的术语、其类型和THATI，SEN，ANDMARTI-OLIET277| |联系我们匹配产生的替换;为了只保留术语，我们使用投影getTerm。opAPITRACE-MOD：->模块。等式APITRACE-MOD = Δ'APITRACE]。var N：MachineInt.vars T X：Term.opallOneStepAux：Term MachineInt Term->TermSet。opTraceTermToTrace：Term -> Term.等式TTrmtoTraceSet（T）= allOneStepAux（T，0，'X：TraceTrm）。等式allOneStepAux（T，N，X）=if metaSearch（APITRACE-MOD，T，X，nil，'else TraceTermToTrace（getTerm（metaSearch（APITRACE-MOD，T，X，nil，