π-演算活动名称等价性的重写规则和双模拟检验技术研究

理论计算机科学电子笔记130（2005）169-185www.elsevier.com/locate/entcs从活动名称到π-演算重写规则安娜角V. de Melo圣保罗大学计算机科学系RuadoMatao，1010-CidadeUniversita'ria0550 8090-SaoPaulo-SP-Brazil摘要检验π-主体的等价性的问题并不简单，在过去的十年中得到了广泛的研究。可以采用句法和语义方法来形式化地验证π演算等价性。句法方法主要依赖于结构一致性。 另一方面，语义检查方法可以验证更广泛的等价性，但不能检查无限个π-代理。双相似代理具有相同的活动名称集。这一结果和一种考虑活动名称的双模拟检验技术在[7]中给出。在那里，代理活动名称是从其对应的标记转换系统（LTS）计算的，因此不能直接应用于重写系统。在[2]中，给出了π-主体主动名的句法特征。 在这里，提出了新的重写规则（基于活动名称的句法特征），以识别和丢弃一类表达式（包括组合）的π表达式的无用代码。 有了这些新规则，π-表达式被更好地减少（更多无用的代码被丢弃），丰富了代理的等价类关键词：移动代理，π演算，形式验证，重写系统1介绍在过去的十年中，π演算代理的形式验证问题得到了广泛的研究。关于等价性检查，我们可以粗略地将验证技术分为使用重写系统在语法级别解决问题的技术，例如[3];以及基于标记转换系统（LTS）的行为等价性。在这两种情况下，检查π-代理的等价性的问题并不是微不足道的，每种技术都有局限性。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.010170A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169为了检查行为等价性，状态爆炸是一个问题，因为当代理名称集是有限的时，输入动作会引起无限数量的转换。Montanari和Pistore [7，8]证明了有限自动机可以在没有匹配的情况下有效地为有限个1π-演算构建（选择代表性输入）。从这些有限分支自动机中，活动名称是计算和自动机被进一步减少，以检查等价性（bisimilarπ-代理具有相同的活动名称集对于这种方法，代理活动名称的计算依赖于标记的转换系统（自动机被构建），并且仅限于没有匹配的有限π演算类在句法方法中，π-表达式被改写为规范形式，如果它们的表达式被规范为相同的表达式，则代理是等价的，模到α转换，并行组合的交换性和结合性这种方法中的大多数验证系统都与结构一致性有关。一些效果已经被用来改进句法验证技术，以检查比结构全等更广泛的等价。例如，Hirschko [3，4]开发了一种技术，将检查结构一致性的想法扩展到Sangiorgi[11，12]的双模拟。在[2]中，提出了一个关于潜在的主动名的句法特征的研究。这项研究确定了某些类别的表达式，可以从语法上计算出活动名称，而其他表达式则需要内部通信来计算活动名称。尽管该研究给出了如何计算活动名称及其对应的非活动名称的指导，但该研究并没有给出使用后者来消除π表达式的无用代码的见解。消除π表达式的无用代码对切片技术，特别是重写验证技术很有意义。本文提出了一种应用活动名的句法特征化来约简π-表达式和增强π-演算重写验证技术的方法这是通过开发新的重写规则来实现的，以在规范化阶段从π表达式中消除无用的代码。一般来说，主动名称的句法计算是不可能的，对于某些类别的表达式，内部通信是必要的这里给出的重写规则仅限于有效名计算仍然可判定的π首先介绍了π演算的基本概念：语言片段及其语义。第三部分总结了对主动名的研究第4节介绍1.....................................................一个句法上但限制性更强的概念是finite控制剂，即， 在递归中没有并行组合的代理。”[7]的文件。A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169171一个重写系统，然后提出新的重写规则。最后一部分分析了本研究的局限性。2π-演算矩阵本工作中使用的π-演算片段（一元π-演算）与[6]中的类似，但复制的代理人由一个prefixing action2保护：Q：：= 0|α。P|（v→x）P|P1+P2|P1|P2|！ α。P语言元素具有通常的含义。0表示停止，不能进行。（v→x）P是n→x中的所有元素，它们都受主体P的约束。P1+P2表示代理人P1或P2的选择，而P1|P2代表药剂成分. 终于，！ α.P复制α.P作为只要有需要，就有无限多的α。代理动作α定义如下：α：：= τ |a（b）|AB |a（b）τ是无声的（内部的）动作：没有可观察行为的动作。a（b）表示沿着端口a接收b的动作，ab表示沿着端口a发送b的动作，并且a（b）沿着端口a将内部名称b发送到其上下文（范围扩展）。I和O分别表示输入和输出操作的集合。ch（α）表示操作端口名，而obj（α）表示沿端口传递的信息。限制（νb）P与输入作用a（b）.P都将名字b绑定到P的作用域。b在这两种情况下都是绑定名称（bn），否则是自由名称（fn）。2.1语义定义π演算语义的一种方法是首先捕获结构一致性的概念，然后通过转换方法定义行为。结构全等（Structural Congruence，缩写为STW）被定义为满足表1- 3[9]中的定律的最小全等（复制主体的定律已被添加到原始定义中，以处理Hirschko的重写系统[3，4]）。结构同余不足以定义进程代数中的行为等价。除了结构一致性之外，2在重写系统中，需要保护的复制代理来寻找范式。此外，在后面的重写系统中也没有考虑求和;这里引入求和是因为对活动名称的研究。[3]定义结构一致性的方法有很多，我们选择了其中一种来帮助找到重写规则。172A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169P→P，P →Q，Q →QJαJ结构的PrefixP→QJαJα.P→PαP→PαJP→P，bn（α）<$fn（Q）={}αJ总和ParP+Q→PαJP|Q → P| QαJP→P，Q →Qa（x）日欧JP→P， x∈/ααJ网ResαP|Q → P {u/x}|QτJ J（νx）P→（νx）PJP→P，a/=xaxJP→P，P→P， a=/ua（x）Ja（νu）J开放密切（νx）P→Pa（νx）JP|Q→（νu）（P| Q)τJ J(i) 如果P和Q是α转换的变体，则P<$Q。(ii) 平行和求和的阿贝尔幺半群定律：(a) 交换性：P|QQ|P，P + Q<$Q + P;(b) 关联性：（P|Q）|RP|（Q|（P + Q）+R=P+（Q + R））;和(c) 0为单位：P|0P和P +0P。(iii) 范围扩展法：(a)（v x）00(b) （νx）P<$P，ifx∈/fn（P）(c) （vx）（P|Q）（P|（νx）Q），ifx∈/fn（P）(d) （νx）（P+Q）<$（P+（νx）Q），ifx∈/fn（P）(e) （νx）（νy）P（νy）（νx）P(iv) 复制定律：(a) ！α.P| A.P！α.P(b) ！α.P|！A.P！α.P表1结构一致性规则每个组合子都是必需的。在这里，π演算的语义由基于后期语义的标记转换系统给出（表2）[9]。表2π-演算的迁移语义（后期）引入规则Struc以考虑结构一致性。这也简化了过渡系统规则。由于交换律是为结构同余中的求和和平行合成定义的，因此不需要定义Sum和Par的对偶规则。A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169173有一组定义为π演算的等价物[9]。在这里，只定义了早期互模拟。定义2.1具有后期语义的早期互模拟（英语：early bisimulation）是一个对称的年龄上的二元关系R满足PRQ和P→α PJ，当他在bn（α）是新鲜的，意味着1.如果α=a（x），则<$u：<$QJ：a（x） JJJ，及;Q→Q2.如果αi不是一个n输入，则n<$QJ：Q→αP{u/x}RQ{u/x}QJPJRQJ.P和Q是（强）早期双相似的，记作P<$Q，如果它们通过早期双模拟相关。3活动名称Montanari和Pistore在[7]中基于用于值传递CCS [5]的使用名称的思想研究了π-演算代理（简称π-代理）的活动名称。Pistore和Sangiorgi [10，11，12]提出了一种分区细化算法，使用从LTS计算的活动名称来检查早期和开放互模拟。在[2]中，进行了一项研究，以识别来自π-代理表达式的活动名称，而不是LTS。如果一个名称是自由名称，并且可以由P执行，则称该名称在施事P中是语义上活跃的。一个重要的结果，从这取决于具有相同的一组活动名称的bisiliminary代理：这在[7]中正式声明如下：定义3.1名称a对于施事PiP/（νa）P是有效的;an（P）={a|P/ε（νa）P}是年龄P的一个具体名字的集合。命题3.2如果P<$PJ，则an（P）= an（P J）。如果从外部上下文的角度来看，一个名称对于一个代理来说是语义上不活动的。绑定名称可以在代理的内部操作中发挥作用（因此它们无法干扰外部上下文）。除此之外，由于名称限制，某些操作永远不会执行。因此，专门参与内部动作或从未参与的动作（无用动作）的代理名称是所谓的非活动名称。某些π表达式可以在不参与内部动作的情况下识别活动名称。表3总结了这类表达式的活动名称的句法特征。例3.3Q1def= a（x）.x（y）|ab.bc.c（z）174A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169剂活动名称10- -2α.Pfn（α）<$（ an（P）− bn（α））3P1+ P2一个（小一）一个（小二）84（v→x）α.P>{}，ch（α）∈→xfn（α）<$（an（（ν→x−{b}）P）−bn（α））， α=a（b）<$a∈/→x>：fn（α）<$（an（（ν→x）P）−bn（α）），otherwise5（v→x）（P1+P2）ann（（v→x）P1）n（（v→x） P2）6α. P1 |β. P2α-葡聚糖（α. P1）7！α.Pan（α.P）8！α. P1|！β. P2α-葡聚糖（α. P1）表3没有反应的an（Q1）=an（a（x）.x（y））→an（ab.bc.c（z））an（a（x）.x（y））=fn（a（x））<$（an（x（y））−bn（a（x）={a}<$（fn（x（y））<$（{}−bn（x（y）−{x}）={a}（{x}（{} − {y}）− {x}）={a}（{x}− {y}− {x}）={a}− {y}={a}an（ab.bc.c（z））=fn（ab）<$（an（bc.c（z））−bn（ab））={a，b}<$（fn（bc）<$（an（c（z））−bn（bc）−{}）={a，b} <$（{b，c} <$（{c} <$（{}−{z}）− {}）− {}）={a，b，c}an（Q1）={a}<${a，b，c}={a，b，c}复合代理可以使用相同的动作参与内部通信并与外部环境通信，因为在表达式的顶部没有限制。因此，不会进行范围挤压，并且表达式中的所有操作都可以参与。对于没有限制名称的代理，可以直接从表达式计算活动名称。在一般情况下，如果不进行内部通信，就无法计算代理活动名称对于可以独占地参与内部操作的代理，必须执行内部步骤来检查接下来要执行哪些操作，然后计算它们的活动名称。表4总结了A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169175在需要内部通信时，计算潜在代理的活动名称为了获得所有可能的内部通信复制过程，我们必须考虑最多的后续行动的数量代理可以执行。这对应于表达式的大小（expsize（E）由运算符的数量给出，第3项），只考虑前缀和复合运算符。剂活动名称81（v→x）α。P|β。Q>（a n（（v→x）β. Q））<$（an（（ν→x）α.P）），>>（a n（（v→x）（P{c/b} |Q））−b n（α）），α=a（b）<$>>>β=ac>（a n（（v→x<${c}）（P{c/b} |Q））>>−bn（α）−bn（β）），α=a（b）>>>β= a（ c）>：a∈→x2（v→x Pnα。P|）的情况下（i=1iPmα .Q）j= n+1j jS{an（（v→x）（αi. Pi|αj。Qj））|1≤i≤n，n+ 1≤j≤m}Q3（v→x）！α.Pan（（v→x）nα。P）， n =expsize（α. P） + 1（Si=14Qn（v→x） i=1！ αi。PiS{an（（v→x）（！ αi。Pi））|1≤i≤n}S{an（（v→x）（αi. Pi|αj。Pj））|1≤i，j≤n<$i/=j}表4反应下的活动名称下面的示例显示了如何计算活动名称，因为需要内部通信。例3.4假设代理人Q2和Q3定义如下：defQ2 =cd.a（x）.xydef年q3 =a（b）.b（z）.ywCD（νa）Q2→（νa）（a（x）.xy）<$0（νa）Q30（νa）（Q2|Q3）→cd（νa）（a（x）.X y|Q3）→ττ（v a，b）（由|b（z）.yw）ywan（（νa）Q2）={c，d}an（（νa）Q3）={}→（νa，b）（0 |yw）→（νa，b）（0 |0个）an（（νa）（Q 2 |Q 3））={c，d，y，w}176A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169上面的例子展示了一种情况，在这种情况下，执行范围扩展，然后由于这样的名称挤出而可以进行操作，否则代理将停止。例如，Agent（νa）Q2不能执行动作a（x），因为名字a是受限制的。 由于同样的原因，（νa）Q3有与代理停止的行为类似。虽然由于名称受限，两个代理都无法单独进行，但当它们组成时，它们可以进行内部通信，并且在整个代理范围。结果，（νa）（Q2 |Q3）可以执行所有Q2和Q3动作和活动名称集包括所有这些动作名称.注意由于内部操作，名称b的作用域挤出首先被执行，这使得第二个内部操作成为可能。4一个π-演算检查互模拟可以通过重写与结构一致性有关的系统来执行[12]：使用π表达式的范式，并且如果可以将代理重写为相同的表达式模到alpha转换，并行组合的交换性和结合性以及连续限制的置换，则代理是双相似的。除此之外，Hirschko [4]开发了一种技术，将检查结构一致性的想法扩展到互模拟-直到Sangiorgi [11]。本节总结了Hirschko [3，4]开发的用于检查双向模拟的重写系统。新的重写规则的基础上的研究活动的名称描述后（第5节）。4.1通过重写Hirschko的验证技术可以处理π演算的一个片段，而不需要求和、匹配或不匹配。为此，定义了一个标准形式，并证明了它是唯一的[3]：（1） P=0|（v→x）α1.P1|α2.P2|... . . . 你 好 。 .|αm.Pm|！ αm+1.Pm+1|... . . . 你好 。 . |！ αn.Pn|注意，在这个范式中没有考虑求和，代理人是预先确定的代理人的产物。此外，使用字母转换是为了避免自由名称和绑定名称冲突。在第5节中，这个范式也被用来定义新的重写规则。为了检查代理的等价性，首先应用术语规范化算法，然后比较规范化的标准化如下：定义4.1规范化算法可以定义为基于以下规则的重写系统：A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169177[R1] P| 0→P[R2]（νx）P→P，若x∈/fn（P）[R3]P|（νx）Q→（νx）（P|Q），如果x∈/fn（P）[R4]！α.P| α.P→！α.P【R5】！α.P|！α.P→！α.P[R6]（v→x）α。P→0，若ch（α）∈→x除了规则[R3]之外，重写系统由归约规则组成，因此它们对表达式的应用导致新的表达式在大小上更短。定义4.1中的绝大多数规则都来自结构一致性规则（表1）。结果表明，约简后的表达式与原表达式结构一致，并且可以找到一种算法将表达式约简为相应的范式。这个系统（包括规则[R1]规则[R1]到[R5]都来自结构一致性定义。规则[R1]将与停止代理组合的任何代理还原为自身。规则[R2]消除了限制组合子，只要受限制的名称在代理4中不自由出现。规则[R3]是关于范围扩展的。与前面的规则不同，它的应用程序保持表达式的大小，而不是尽管如此，所有的限制都尽可能地被取消，当规则不再适用时，减少程序停止规则[R4]和[R5]是关于复制代理的。在[R4]中，如果代理与其自身的复制副本组成，则会删除该代理。在[R5]中，复制的代理在与自身组合时被删除。请注意，这些规则是可能的，因为所有复制的代理都由一个动作保护;这对于任意复制的代理来说不是真的，正如Milner在[6]中指出的那样。所有来自结构一致性定义的其他规则都不能减少表达式。[R6]不是从同余规则中捕捉到的。它被进一步创建[4]以消除表达式中未使用的部分，并且基于删除不能参与其prefixing操作的代理的想法。请注意，这条规则与结构一致性无关，因为它具有语义（行为）而不是几何意义。然而，这是作为一个“一致性”规则，使更容易应用到互模拟技术。4规则[R2]和[R3]由关于名称自由度的条件保护。 尽管如此，该系统被认为是一个普通的术语重写系统，因为如果使用De Bruijn表示法，则可以将这样的条件嵌入到代理表示178A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169剂（v y）（y（b）.bc.c（z））→简化代理规则0[R6]例4.2考虑以下代理：def年q4 =a（x）.x（w）defQ5 =（νy）（a（x）.x（w）.y（b）.bc.c（z））尽管有不同的自由名称集，但两个代理都只能执行前两个动作，因为y是受限制的。为了检查这些代理是双相似的，上面的重写系统首先应用于两个代理，使得Q5被减少到a（x）.x（w）：以来整个施事体Q5被简化为a（x）.x（w）剂（νy）（a（x）.x（w）.y（b）.bc.c（z））（νy）（a（x）.x（w））简化代理规则→（νy）（a（x）.x（w））[R6]→a（x）.x（w）[R2]还原后Q4和Q5的除了结构一致性，赫希科还检查了双向模拟，直到内射替换、限制和合成。为了检查最多替换和最多限制，使用了规范化代理，并应用了一种对自由名称进行单射替换的算法（实际上，它是阿尔法转换检查方法的扩展）。然而，为了检查合成，必须执行标准化表达式的转换：减少导致无声动作的通信。这些减少有两个主要后果：第一，在内部通信之后，原始的代理不能恢复;第二，当执行内部通信时，可能会产生一组新的表达式。然而，它仍然控制即使使用新规则（[R6]），重写系统也无法从表达式中删除所有不活动的动作（双相似代理具有相同的活动动作集[7]）。由于端口名限制，具有无法与其上下文通信的prefixing操作的代理已被规则[R6]捕获。然而，除了prefixing操作之外，其他情况也可能导致代理无法与其上下文进行通信，如以下示例所示例4.3考虑代理商Q6和Q7：def问6 = （v a）（a（x）.x（w）|（公元前）defQ7 =BCA.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169179动作a（x）（代理Q6）既不能与外部环境（a是受限制的）通信，也不能与另一个复合代理（bc）通信。因此，a（x）.x（w）可以从Q6中移除，而无需检查其行为。如果是这样的话，Q6将变成与代理Q7相同的写入（它们是双相似的）。Q6和Q7的双相似性不被上面的重写系统识别：没有规则可以应用于将Q6重写为Q7。为了扩展寻找π表达式的非活动动作的想法，下面的部分基于对活动名称的研究，提出了从π表达式中消除非活动动作的新规则。新的规则集并不涵盖具有复制代理的π演算片段的后期或早期互模拟，但它在稍微丰富[4]中使用的组合项约简的意义上向前迈出了一步。5从非活动名称到新重写规则通过对主动名的句法表征，我们可以找到代理人的潜在主动名和非主动名。非活动名称是绑定名称集与自由名称的联合，这些自由名称只出现在代理从未参与的操作（即非活动操作）中。分析表达式及其相应的活动名称集，我们可能会发现子表达式在前面有非活动动作时从未使用过。这些不可接合的子表达式可以代替保持互模拟的停止代理为了通过去除不使用的子表达式，对活动名特征化的研究为π-表达式的约简提供了基础，从而丰富了基于项重写的π-演算验证技术本节介绍了基于该研究的新重写规则5.1非活动操作：案例从主动名称的句法特征中，我们还可以发现某些由于名称限制而从未参与的行为。此外，之前从未参与的动作（非活动动作）变得不活动。事实上，受限制的名称是不可参与的动作的关键点。这一节总结了一些情况，在这些情况下，受限制的名称会导致使用前缀和并行组合的π演算非活动名称可以分为自由名称和绑定名称。所有非活动的自由名称仅出现在非活动的操作中。另一方面，非活动绑定名称可以参与可参与和不可参与的动作。可接合绑定名称的集合由在活动名称的计算中出现的所有绑定名称组成。未出现在此类计算中的绑定名称属于从未参与的操作（非活动操作）。一180A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169可以从活动/非活动名称计算中识别不可参与操作的候选者。在这里，我们分析了导致潜在的不可参与的动作的情况，以获得涉及受限的前缀和合成代理的表达式：前置：前置动作的端口名称受到限制-组合：代理是两个进程的组合，它们具有受限制的端口名称，因此其中一个进程不能与上下文或另一个进程通信。我们必须首先分析一个受限制的行动如何与其他行动交流，以便发现相反的情况。 设α是年龄P的一个预赋限制算子，其中Q（（v→x）（α））是P的一个预赋限制算子。P|Q）andch（α）∈→x）。αcan通过以下方式之一与Q(i) Q中存在作用量α。由于绑定名与表达式中所有其他绑定名或自由名不同，因此端口名不能被重构。只要α在Q中，它就可以与α通信（例如：（v a）（a（x）.A |ab.B））;(ii) 代理Q中存在动作β，它将α端口名挤出到并且β端口名称是自由的（β是可参与的动作）。(ex.：（v a）（a（x）.A|b（a）.B））;或(iii) 在该限制内存在第三代理。例如，（v→x）（α. P|Q|R）andch（α）∈→x而β（在代理Q中）可以由于内部comm而被重构为α与第三代理（R）通信。一个特殊的例子：（νa，b）（a（x）.A|b（y）.yc.B|ba.C）。如果发现其中一种情况，受限制的代理人能够从事通讯然而，对于相反的情况，代理不能通信，无用的子表达式可以被删除。所有这些潜在沟通均与表4第1项有关）。下面的部分将对上述情况进行形式化，以在重写规则中表示无用的子表达式。5.2初步定义为了定义新规则，我们首先给出基本定义。以下定义都与代理表达式（语法）有关，而不是动作本身-mantics。设I是输入动作的集合（β∈I意味着β是输入动作），O是输出动作的集合。定义5.1直到通信和阿尔法转换的行动平等被定义为：α等于β（表示为αβ），如果A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169181=ch（α）=ch（β）<$（（α∈I <$β∈I）<$（α∈O <$β∈ O））请注意，要具有相同的通信能力，操作必须具有相同的端口名称，并且都是输入或输出操作。只要操作具有相同的端口名，并且其中一个是输入操作，另一个是输出操作，它们就可以相互通信。以下定义将在沟通理念下采取互补行动的想法形式化。定义5.2一个动作α与动作β互补，如果它们能相互沟通：ch（α）=ch（β）<$（（α∈I <$β∈ O）<$（α∈O <$β∈I））注意，输入动作可以与输出动作或输出绑定动作通信。如果一个动作被写在一个施事表达式中，那么它就被称为出现或属于一个施事表达式。定义5.3一个动作α在施事P中（记作α∈P），如果它或它的α转换，出现在P的... 阿尔法...如果一个动作的前面有一个输入动作，并且它的通道名称与该输入动作的对象名称一致，则该动作可以被重构。这种行动重组的概念定义如下：定义5.4施事P中的动作β与动作α相互作用（记为如果：defP=...β.P1.α.. <$β∈I <$ch（α）=obj（β）一旦一个动作可以被重构，它就可以演变成一个特定的动作。 事实上，它可以改变它的名字，使之与另一个动作相同，直到阿尔法转换。定义5.5在年龄t（ν→x）P中的作用βc可以vevoα（denotedasβ\α：（ν→x）P）ifβ∈（ν→x）P（β=α β/β γ）。γ<$→β：（ν→xP））（注：γ<$→β：（ν→xP）<$β{ch（α）/ch（β）}α）如果操作β的端口名被重命名为α端口名，则操作β等于（直到通信）α。请注意，这种平等是在定义的意义上。5.1[5]这是为了使进一步的定义更容易而滥用符号。182A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）1695.3新规则在这里，创建新的重写规则来减少π表达式，因为代理无法参与某些操作。先验地，我们可以考虑减少代理表达式，只要要执行的如果我们既没有通过合成进行交流，也没有通过重组进行交流，也没有通过π-施事中的在[4]中，Hirschko开发了一个基于结构一致性的重写系统，该系统丰富了一个规则，以减少代理表达式，因为限制是对前缀操作端口名称的限制（规则[R6]）。然而，这条规则并不涵盖子表达式可以在没有删除代理行为的情况下被删除的所有情况（已经在4.1节中讨论过）。在这里，找到了将代理表达式减少为受限动作的规则，并且定义了代理无法与其上下文通信的情况（第5.1节-合成中显示的情况）。事实上，这扩展了重写系统，也可以处理组合代理中无用的子表达式。定义5.6并行代理的重写规则定义如下：[R7]（v→x）（α. P|Q）→（ν→x）Q，ifch（α）∈→x<$/α∈Q/nβ ∈ O.β ∈ Q n obj（β）= ch（α）[R8]（v→x）（α. P|Q|R）→（ν→x）（Q|R），if（ch（α）∈→x<$β ∈ O. （β∈Robj（β）=ch（α）<$ch（β）∈→x）<$/γ∈Q.γ\α：Q）对于规则[R7]，agentα.P被降为0，因为它不能与Q通信;Q没有α动作。同时，Q无法将α端口名称挤出到上下文。该规则将第5.1节中的组成1和组成2项形式化。例5.7考虑例4.3中的代理人Q6和Q7：def问6 = （v a）（a（x）.x（w）|（公元前）defQ7 =BC将规则[R7]应用于AgentQ 6，我们得到一个新的Agent，可以进一步A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169183AgentReduced AgentRule（νa）（a（x）.x（w）|bc）→（νa）bc[R7]（νa）bc→bc[R2]剂简化代理规则（v a，d）（a（x）.x（w）|d（y）.bc |da）→（νa，d）（d（y）.bc |da）[R8]简化为代理Q7：Q6和Q7被检查为双相似，因为应用了归一化。另一方面，规则[R8]显示了如何减少一个agent表达式，即使α端口名称明显被挤出，但Q中没有动作可以进化到α。乍一看，这看起来与规则[R7]不一致，其中α通道名称被挤出。然而，如果挤压通道名称的动作也受到限制，则与α进行通信的唯一方法是将其作为Q的输入（从R）给出，并且Q规则[R8]给出了一种句法情况，在这种情况下，这样的通信是不可能的，并将第5.1节的组合3项形式化。例5.8考虑代理商Q8和Q9：defQ 8 =（νa，d）（a（x）.x（w）|d（y）.bc |da）defQ 9 =（νa，d）（d（y）.bc|da）将规则[R8]应用于AgentQ 8，我们得到AgentQ 9：规则[R6]、[R7]和[R8]捕获了基于非活动动作消除无代码π表达式的想法。[R6]捕获了在prefixing上下文中的受限代理的想法，而[R7]和[R8]捕获了受限组合代理的想法，其中一个代理停止，因为它的prefixing动作具有受限通道，无法与其他代理通信。然而，这些规则并不涵盖合成代理可能停止的所有情况。 例如，我们可以从规则[R8]中删除条件ch（β）∈→x和s直到haveαchannele挤出。但是，这将需要一种语义方法来进行检查，我们避免了这种方法，以保留重写技术（为了检测到这种情况，由于代理重新配置，必须执行某些通信）。6结论基于π-agent主动名的句法特征，提出了新的重写规则.主要结果是对这些应用184A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169重写系统的规则，丰富了通过规范化检查的等价类：在代理规范化之后，现在可以检查某些组合代理的双相似性。这是向[3，4]前进的一步，其中只有未使用的前缀代理可以从表达式中删除。互模拟检验可以通过重写与结构同余有关的规则来实现在那里，使用π-表达式的范式，如果代理可以被重写为相同的范式模到alpha转换，并行组合的可交换性和结合性以及连续限制的置换，则代理是双相似的。除此之外，Hirschko [3，4]开发了一种技术，将检查结构一致性的想法扩展到Sangiorgi[11，12]的互模拟。通过对主动名的句法表征，我们还可以发现代理人的潜在非主动名。从中，我们可能会发现部分的ex-currency从来没有使用过，因为它前面的名称语义上是不活动的（即不活动的动作）。以非活动操作开始的表达式可以代替停止代理而不改变行为。换句话说，我们可以利用主动名的特征化来减少π-表达式并增强π-表达式。演算重写验证技术。在目前的工作中，我们调查了如何在不影响其行为的情况下去除某些不可接合的合成试剂。但是，这并不包括组合代理可能停止的所有情况。为了检测到这种情况，由于代理重新配置，必须执行某些通信，并且必须应用语义方法。新的规则组成的代理人已被调查考虑的语义方法，但仍在进行中，以及复制代理人的规则。已经开发了一个原型来实现Hirschko的重写系统和新规则。从[R1]到[R7]的规则已实施，[R8]正在进行中。该系统已成功地应用于玩具的例子，但没有准确的数据性能已采取至今。引用[1] W.兰斯·克里夫兰编辑Proceedings of the Second International Conference on Foundationsof Tools and Algorithms for the Construction and Analysis of Systems（TACASSpringer，1999年。[2] 安娜角梅洛。关于π-主体的潜在活性名的研究。ENTCS（Electronic Notes in TheoreticalComputer Science），95（C）：269[3] D. 赫 什 科 自 动 证 明 互 模 拟 。在 Petr Jancar 和 Mojmir Kretinsky ， 编 辑 ， Proceedings ofMFCSElsevier Science Publishers，1998.A.C. V De Melo/Electronic Notes in Theoretical Computer Science 130（2005）169185[4] D.赫什科使用up-to技术进行互模拟验证的好处。在Cleaveland [1]，第286[5] B. Jonsson和J. Parrow。一类非有限状态程序互模拟等价性的判定。信息与计算，107（2）：272[6] R.米尔纳通信和移动系统：π-演算。剑桥大学出版社，1999年5月。[7] 联合Montanari和M.皮斯托雷检查有限个π演算的双相似性。Insup Lee和Scott A. Smolka，编辑，Proceedings of CONCURSpringer，1995年。[8] 乌戈·蒙塔纳里和马可·皮斯托雷 异步π演算的有限状态验证。 在Cleaveland [1]，第255[9] J·帕罗 π-演算简介 在Bergstra，Ponse和Smolka，编辑，过程代数手册，第479Elsevier，2001年。[10] M. Pistore和D.桑吉奥吉π-演算的一个分区精化算法。 在Rajeev Mür，编辑，Proceedings ofCAV 完整版本将出现在信息与计算上。[11] D.桑吉奥吉互模拟证明方法。Mathematical Structures in Computer Science，8（5）：447-479，1998.一个扩展的摘要出现在MFCS '95的会议记录[12] D. Sangiorgi和R.米尔纳弱互模拟问题。In W. R. Cleaveland，编辑，CONCUR史普林格出版社