π-演算代理活性名的形式验证技术研究

理论计算机科学电子笔记95（2004）269-286www.elsevier.com/locate/entcsπ-主体的潜在活性名研究安娜角V. de Melo圣保罗大学计算机科学系（USP）RuadoMatao，1010-CidadeUniversita'ria0550 8090-SaoPaulo-SP-Brazil电子邮件地址：acvm@ime.usp.br摘要CCS [5]的验证技术不能直接用于验证π演算[6，7，10]代理。Montanari和Pistore [8]指出，在某些限制下，如果只考虑活动名称，则可以构建π-agent的标记迁移系统（LTS），以便CCS的工具和算法也用于检查π-演算中的一些等价性。在那里，他们提出了一种基于语义模型计算代理活动名称的方法-首先建立整个LTS，然后计算活动名。本文给出了π -agent的活动名的句法特征。通过这种方式，可以为代理表达式而不是其相应的LTS计算活动名称。这项研究的结果可以应用于在基于重写和行为模型的验证技术中减小π-代理的大小。关键词：移动代理，π演算，形式验证，活动名称。1介绍在过去的十年中，π演算代理的形式验证问题得到了广泛的研究。关于等价性检查，我们可以大致将验证技术分为使用重写系统在语法级别解决问题的技术，例如[2];以及基于标记转换系统（LTS）的行为等价性。在这两种情况下，检查π-代理的等价性的问题并不是微不足道的，并且每种技术都有局限性。对于行为等价性检查，状态爆炸仍然是一个问题，因为输入动作可能会生成无限数量的转换，1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.016270A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-代理人有无限多个名字。Montanari和Pistore [8，9]已经证明，如果选择代表作为输入，则可以有效地为有限π演算因此，可以找到无穷个π-agent的最小实化自动机（无冗余展开），并且可以将检查CCS等价的技术和工具应用于这样的自动机。 然而，为了构建无冗余的展开自动机，主动必须发现名称和具有代表性的新名称（它们用于构建有限分支自动机）。活动名称的概念与使用名称为CCS代理构造有限状态转换的想法有关，并传递值[4]。Mota- nari和Pistore为π-演算重新定义了这一思想：如果（νx）P不与P双相似，则名称x在P中是活动的。这意味着活动名称是自由名称的子集，对代理的行为起作用他们还提出了一种算法来计算给定代理标记的转换系统的活动名称：（i）首先用整个自由名称集构造压缩自动机;（ii）在此压缩自动机上计算活动名称;（iii）从压缩自动机中删除非活动名称（无冗余展开）。一旦构建了紧凑的自动机，就可以使用CCS工具来检查这些代理的互模拟。使用活动名称而不是自由名称对使用语义方法的验证技术具有重要意义这对重写验证技术也很有意义，因为代理表达式可以通过消除从未参与的动作（即不活动的动作）来减小大小。与[8，9]一样，使用活动名称来检查等价性的成本在于可以应用于语义方法的压缩自动机的计算另一方面，如果潜在的活动名称被calculu- lated代理表达式，非活动名称可以从表达式中删除因此，主动名称可以应用于语法（重写）和语义验证技术。本文提出了一种潜在的主动名称的句法特征，以计算他们对代理人的表达式的研究。这在一般情况下是不可识别的，并且需要执行内部通信来计算某些表达式的活动名称这项研究致力于识别类的表达式，可以在语法上计算，那些需要内部的行动。它首先解决了π演算的片段，其中活动名称是从语法中计算出来的。内部通信是必要的，以找到潜在的活动名称的片段是A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-271事后提出首先，给出了π演算的基本概念：语言片段及其语义.下面的部分专门研究这个语言片段的活动名称。第四节在前人研究的基础上，给出了计算π最后一节分析了该研究的局限性，并就如何将其应用于核查技术给出了指导。2π-演算矩阵在本工作1中使用的π演算片段（一元π演算）与[8]中使用的π演算片段以及防护复制代理2有关：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发送到其上下文（作用域挤出）。限制（νb）和输入动作a（b）都绑定了名字b。b在这两种情况下都是绑定名称（bn），否则是自由名称（fn）。此外，如果一个名称在其任何行为中表现为受约束，而在其他行为中表现为自由，则该名称与一个施动者受约束。2.1结构同余定义π演算语义的一种方法是首先捕获结构一致性的概念;代理直观地具有相同的行为，并且可以从它们的结构中识别。结构同余式定义为满足表1[10]中定律的最小同余式。1 在这个语言片段中不考虑匹配和不匹配。[2]复制在这里被包括进来是为了关注π演算的一些重写技术。272A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-(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|0 P和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.2转换规则结构同余不足以定义进程代数中的行为等价。除了结构上的一致性，每个组合子的操作语义也是必要的。在这里，π演算的语义由基于后期语义的标记转换系统给出（表2）[10]。引入规则Struc，将结构一致性考虑到语义中。这也简化了过渡系统规则。由于交换律是为结构同余中的求和和平行合成定义的，因此不需要定义和与配的对偶规则。这里没有必要定义封闭转换规则，因为它是从结构一致性和开放规则得出的结论;这里定义两者都明确地具有范围侵入和挤出的概念2.3互模拟实际应用中需要π-代理的行为等价性。 现在有一组定义为π演算的等价物[10]。为了研究的目的，这里只考虑了早期的互模拟。定义2.1具有后期语义的早期互模拟（early bisimulation，缩写为BSE）是一个对称的，αAgent上的Ric二元关系R满足：PR Q和P→P其中bn（α）是新鲜的意味着，JA.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-273Q→QP{u/x}RQ{u/x}Q→QRQP→P，P →Q，Q →QJαJ结构的前缀P→QJαJαα.P→PαP→PJαP→P，bn（α） <$fn（Q）={}J金额αP+Q→PJαP|Q → P| QJP→P，Q →Qa（x）日 欧JαP→P， x∈/αJ网ResτP|Q → P {u/x}|QJ JαJ（νx）P→（νx）PaxP→P， a=/xJP→P，P→P， a=/ua（x）a（v u）JJ开放密切（νx）P→Pa（νx）JτP|Q →（νu）（P|Q)J J表2π-演算的迁移语义（后期）1.如果α=a（x），则<$u：<$QJ：a（x） JJJ，及;2.如果α不是输入，则<$QJ：αJJJ.P和Q是（强）早期双相似的，记作PEQ，如果它们通过早期双模拟相关。3主动名Montanari和Pistore在[8]中基于值传递CCS的使用名称的思想研究了π-演算主体的活动名称（简称π-主体）。Pistore和Sangiorgi [11，12，13]提出了一种分区细化算法-rithm检查早期和开放基于活动名称的互模拟。 这是Montanari工作的一个进步事实上，具有非活动名称的动作，即非活动动作，可以从代理中删除而不改变其行为。由于π-演算中允许的代理重构，查找活动名称与检查互模拟一样困难，并且在这两项工作中都遵循语义方法。本文研究了从π-agent表达式中识别主动名的问题，给出了一个句法特征，而不是像以前的工作那样遵循语义方法。如果一个名称是自由名称，并且可以由P执行，则称该名称在施事P中是语义上活跃的。显然，端口名受限的操作不能单独执行（除非发生内部通信），274A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-α一个（α）一个（α）联系我们ab{a，b}{}a（b）{a}{b}所涉及的所有名称与代理行为无关。一个重要的结果，这取决于这样一个事实，即bisiliminary代理有相同的一组活动名称：一个代理的活动名称是最小的子集的自由名称，其中一个executes代理的行为。这在[8]中正式声明如下：定义3.1一个名字a对于一个施事PiP/（νa）P是有效的;an（P）={a|P/ε（νa）P}是年龄P的一个类型名的集合。命题3.2如果P<$PJ，则an（P）= an（P J）。基本上，如果从外部上下文的角度来看，一个名字在代理中是不活动的，那么它不能改变这样的代理。某些名称可能只对主体的内部行为起作用;因此它们无法干扰外部环境。除此之外，由于名称限制，某些操作永远不会执行。因此，只参与内部动作或从未参与该动作的动作的代理名称是非活动名称。为了识别代理的活动和非活动名称，必须首先定义单个动作的活动名称：定义3.3单个动作的主动名称如下[8]：动作α的活动名（an（α））是它的自由名的集合。这对应于输入和输出操作以及输出信息的端口名称。另一方面，输入和输出边界信息由非活动名称（an（α））表示。静默操作既没有活动名称也没有非活动名称。尽管对识别代理非活动名称至关重要，但由于代理重新配置，动作的活动和非活动名称的定义不足以计算代理的整个活动名称为了研究施事活动名的特征，我们必须考虑一个标准形式：这里使用Milner [6]的施事标准形式，但限制是所有复制的施事都有一个前缀动作3。π-agent的标准形式包括并行和复制agent，所有名称限制都在表达式的顶部。3这也是对π演算重写系统的限制（以保证规范形式的唯一性），并已被采用以使分析更短。A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-275定义3.4[6]过程表达式（1）（ν→x）M1|... . . . 你 好 。 . |Mm|！ α1。Q1. . . |！ αn. Qn是标准形式的，如果每个Mi都是非空和，并且每个Qj本身是一个标准形式。对于该标准形式，阿尔法转换被认为是所有绑定名称都是新的（自由名称和绑定名称在代理中不冲突）。因此，可以在不检查表达式中的后续名称的情况下对代理名称集进行操作。接下来的部分总结了基于π-agent的表达结构（语法）对agent的活动名称的分析这是一种主动名称的句法特征，而不是Montanari和Pistore定义的转换（语义）特征。该研究已经进行了有关的结构归纳法：单一的π演算算子的治疗，其次是他们的组合。首先分析了可以直接从表达式计算活动名称的π演算片段，然后分析了必须进行内部通信才能计算活动名称的片段。3.1没有反应的某些活动名称可以从代理表达式中计算出来，而无需执行内部操作。这在prefixing actions中尤其如此。前置动作，即使它们是输入动作，也可以在不执行转换的情况下，通过查看代理表达式来计算它们的活动名称。代理活动名称的集合主要是它们的自由名称的集合，除了那些专门出现在代理从未执行的动作中的名称。 从π-演算表达式出发，对每个算子分别分析了代理活动名称的计算.3.1.1停止defQ=0，然后an（Q）=fn（Q）={}0代理的自由名称由空集给出;它既没有绑定名称也没有自由名称。3.1.2前缀defQ=α.P，则an（Q）=fn（α）<$（an（P）−bn（α））276A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-对于具有前缀动作的代理，首先计算前缀动作的活动名称，然后计算后续代理的活动名称。请注意，绑定名称将从活动名称集中删除3.1.3求和defQ=P1+P2，则an（Q）=an（P1）an（P2）求和代理的活动名称由每个被加数的并集分别计算。没有必要从另一个主体中消除一个主体的绑定名称（从 P2中消除bn（ P1），反之亦然），因为在标准形式的主体中没有绑定名称与自由名称冲突3.1.4限制(i) 预处理：defQ=（v→x）α。P：x{}，ch（α）∈→xan（Q）=fn（α）<$（an（（ν→x−{b}）P）−bn（α）， α=a（b）<$a∈/→xfn（α）（an（（ν→x）P）−bn（α）），则rw是在上述情况下，输出绑定操作已被视为特殊情况，因为从该点开始必须将其从受限制名称列表中删除。输出绑定名称不活动，因为它们是系统创建的新名称。然而，它们的挤出极大地扩展了代理范围，并可能改变新的活动操作，被计算。如果这样的绑定输出成为剩余代理表达式中的通道名称，则代理有机会不会因为范围挤压而死锁。考虑以下单个示例4：defP=（νb）a（x）.cb.ba.d（y）an（P）={a}<$（an（（νb）cb.ba.d（y））−{x}）={a} （{c} （a n（ba. d（y））−{b}））−{x}={a} <$（{c} <$（{a，b} <$（an（d（y）−{b}））−{x}={a} <$（{c} <$（{a，b} <$（{d} −{y}）−{b}））−{x}={a，b，c，d}− {y，b，x}={a，c，d}4.停止（0）剂从剂的末端省略。A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-277α .P|j=n+1jj如果不考虑范围外推，则不能执行动作ba和d（y）因为B是限制性的。因此，通过b作用域挤出（从actioncb on），以下动作变为活动，它们的自由名称也变为活动。(ii) 总计：defQ=（v→x）（P1+P2），则an（Q）=an（（ν→x）P1）<$an（（ν→x）P2）对于带限制的求和，由于两个代理之间不能执行通信，因此被加数被单独处理。因此，来自两个受限代理的所有活动名称在整个代理中也是活动的（考虑单个联合）。3.1.5组合物(i) 预处理：defQ=α.P1|β.P2，则an（Q）=an（α.P1）an（β.P2）对于异步合成，代理被隔离地评估，因为没有观察到任何限制，并且代理处于标准形式：没有P1的绑定名称可以与P2的自由名称相一致（反之亦然）。因此，来自两个代理的所有活动名称在整个代理中也是活动的，并且可以考虑单个并集。即使应用了范围挤出，由于通信涉及绑定的输出操作，每个代理的活动名称在复合代理中仍然是活动的。考虑到π-演算中的合成是异步的，合成中两个主体的活动名称的集合由于它们的内部通信而不能减少。 另一方面，由于没有受限制的名称，因此不会有新的活动名称出现在内部通信中。(ii) 总计：defQ=卢恩i=1我我n+mP，则a n（Q）= {a n（αi.Pi）|1≤i≤n+m}这是求和和合成的一个推广，这里介绍它是为了涵盖标准形式。3.1.6复制(i) 预处理：278A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-defQ= ！P，则an（Q）=an（α.P）当一个代理被重新定义时，只有它的绑定名称可以改变。然后，由于重新配置，没有新的活动名称可以从代理中出现（活动名称是自由名称的子集此外，如果没有应用限制，则无法到达死锁的代理。因此，不会从活动名称集中删除任何自由名称。每次进行通信时，都必须适用范围限制。然而，该代理是标准化的，并且没有先验地应用限制。因此，即使找到绑定操作并应用了作用域挤压，所有自由名称都是活动的，因为在顶部没有找到限制。事实上，这是一种特殊的合成情况。(ii) 成分：defQ=！α.P1|！β.P2，则an（Q）=an（α.P1）an（β.P2）由于没有限制被先验地应用于施事，所有的自由名都是主动的，并且可以在没有反应的情况下计算主动名（判断与上面类似）。上面讨论的案例展示了π演算语言的片段，其中表达式的这个结果是Pistore和Sangiorgi [11]的结论的一个进步，他们认为对于没有平行合成和匹配活动名的π演算片段，可以在句法上计算，因为它们与自由名的集合一致。在这里，我们已经证明了这可以扩展到没有限制名称的并行组合（这也包括复制代理）。下一节将展示活动名称的计算，包括限制、并行组合和复制。3.2反应下的活动名称在一般情况下，不可能在不参与内部通信的情况下计算所有代理的活动名称。对于包括并行的子代理而没有受限制的名称的代理，可以计算活动名称而不参与内部动作，如前一节所示。然而，对于可以专门参与内部动作的代理，必须执行这些内部步骤，以检查接下来会发生什么动作，然后计算它们的活动名称。本节总结了在需要反应时计算潜在试剂活性名称的方法。A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-2793.2.1限制(i) Compositon：Qdef=（v→x）α。P1|β。P2，thenn（（v→x）β. P2））<$（an（（ν→x）α. P1）），n（（v→x）（P1{c/b} |P2））−bn（α）），α =a（b），β=ac，an（Q）=a∈→xn（（v→x <${c}）（P1{c/b} |P2））−bn（α）−bn（β）），α=a（b），αβ=a（c），n ∈a→x如果只有内部通信，则需要反应来计算活动名称可以进行通信。这导致了新表达式的爆炸，因为代理人对这种内部行为很熟悉。 即便如此，这也受到内部行动数量的限制。对于这种计算，必须处理三种主要的特殊情况。在第一种情况下，活动名称计算是由每个代理的活动名称孤立组成的 最后两个处理所有潜在的活动名称，可以在执行内部操作时出现。它们捕捉到了这样一种想法，即让代理孤立地陷入僵局，但随着内部通信的进行而进展。第二个定义将活跃名称的计算视为由于内部通信而引起的代理人的重新确认。最后一个概念抓住了范围挤压的概念，因为内部操作正在进行。请注意，无法先验地进展的代理可能会随着范围挤出的执行而进展。因此，在这样的挤压之后，动作中的名称可能会由于内部通信而变得活跃。(ii) 组成-总和：民主党Q =（v→x）（i=1αi.Pi| j=n+1αj.Pj），则an（Q）={an（（ν→x）（αi.Pi|αj.Pj））|1≤i≤n，n+ 1≤j≤m}在这种情况下，必须进行组合物中试剂的组合。这是必要的，以涵盖所有可能的内部通信对代理之间。(iii) 复制：defQ=（ν→x）！ α。P，Tennan（Q）=an（（v→x）α. P）， n=expsize（α. P） +1i=1280A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-主动名称不能从重构中出现;它们是自由名称的子集然后，复制的代理可以通过组成有限数量的代理副本来计算其活动名称，而不是复制操作员建议的无限副本所考虑的副本数量基于涉及前缀和复合运算符的表达式的大小。原则上，我们可以考虑单个代理来计算其活动名称。然而，对于受限制的复合代理（即复制代理的情况），某些组合可能会由于重新配置和范围挤压而扩大活性名称的集合为了获得所有可能的内部通信，我们必须考虑代理最多可以执行的后续操作的数量这对应于表达式的大小（expsize（E）），只考虑前缀和复合运算符。(iv) 复制成分：defQ=（ν→x） 你好！P，则i=1iin（（v→x）（！ αi.Pi））|1≤i≤n}an（Q）={a n（（ν→x）（αi.Pi|αj.Pj））|1≤i，j≤n<$ij}这与上面的情况类似。在这里，每个单独的复制代理被认为是与所有对复制代理的组合在一起正如可以注意到的，π演算的片段必须参与内部动作才能计算出活动名称，它涉及到与一种组合相结合的限制运算符。这导致了限制与合成的结合（以及覆盖正常形式的合成求和），以及限制与复制的结合，复制是一种合成（无限多个合成）。考虑到上面的定义，我们可以注意到，许多情况下甚至在反应实际进行之前就导致了新试剂的爆炸。计算活动名称的算法必须考虑到某些个体代理可能出现在不同的地方，并在计算中统一起来。通过这种方式，可以减少新表达式的数量，并且可以唯一地计算它们的活动名称。4计算活动名称：示例本节提供了一组示例来展示如何从π-agents表达式计算活动首先，代理，可以有他们的活动名称计算，而不参与内部行动的一些例子。具有内反应的A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-281将在下一节介绍。在这里，通过直接应用第3节中的活动名称定义（在代理表达式上）来计算代理活动名称。这种计算的递归算法可以从定义中推导出来，因为它们是基于π表达式的结构归纳。然而，这不是最好的算法（如上所述），特别是对于那些需要内部反应的计算。在这种情况下，一个更好的算法可以被定义为识别代理一致性直到阿尔法转换。这种算法的研究超出了本文的范围4.1无反应这一节首先展示了一些只涉及前缀和求和的π-演算片段的例子对于具有这种特征的代理，在整个表达式拼写中计算活动名称;不执行内部操作。例4.1Q1def=a（x）.x（y）.yban（Q1）=fn（a（x））<$（an（x（y）.yb）−bn（a（x）={a}<$（fn（x（y））<$（an（yb）−bn（x（y）−{x}）={a}<$（{x}<$（fn（yb）<$（an（0）−bn（yb））−{y}）−{x}）={a}<$（{x}<$（{y，b}<$（{}−{}）−{y}）−{x}）={a，b}在上面的例子中，agent表达式是一个prefixing action序列。为了计算它的活动名称，我们只需要从左到右读取每个动作，并从整个代理活动名称集中添加自由名称并删除所有绑定名称。这是一个简单的应用程序的代理活动名称定义的prefixing行动。def例4.2Q2 =a（x）.x（y）.yb+bc.c（z）an（Q2）=an（a（x）.x（y）.yb）|an（bc.c（z））a n（a（x）. x（y）。yb）=an（Q1）={a，b}an（bc.c（z）） =fn（bc）<$（an（c（z））−bn（bc））={b，c} <$（{c} <$（{}−{z}）− {}）={b，c}an（Q2）={a，b} <${b，c}={a，b，c}282A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-在求和的情况下，如上所述，计算被分成两个单独的情况：每个被加数一个情况。整个代理的活动名称由两个被加数代理活动名称的并集给出。请注意，这个单一的联合是唯一可能的，因为代理是在一个正常的形式：没有自由和绑定名称冲突。对于名称受限制的代理，必须考虑范围挤压。如果一个动作的端口名受到限制，它就不能被先验地参与。然而，在两种情况下，这种受限的动作可以被参与：它的端口名称先前被挤出到更宽的范围，或者这个动作能够与受限范围内的另一个第一种情况在下面的例子中说明。例4.3Q3def=（νb）（a（x）.x（w）+y（b）. bc.c（z））an（Q3）=an（（νb）a（x）.x（w））→an（（νb）y（b）.bc.c（z））an（（νb）a（x）.x（y））={a}an（（νb）y（b）.bc.c（z））=fn（y（b））<$（an（bc.c（z））−bn（y（b）={y} <$fn（bc）<$（（an（c（z））−bn（bc）−{b}））={y} <$（{b，c} <$（{c} <$（{}−{z}）− {}）−{b}）={y，c}an（Q3）={a}<${y，c}={a，y，c}如果在上面的代理中没有考虑作用域挤压，那么只有第二个被加数的第一个动作会参与，因此，名称c将从代理活动名称的集合中丢失。然而，考虑到作用域挤出，名称b被挤出，使得c在该代理中被视为活动名称。请注意，b一旦被挤出到环境中，就不再受表达式限制没有限制的复合剂的活性名称也可以在表达式上计算，而无需进行内部操作。复合代理是否可以进行通信并不重要，因为重新配置并不影响不受限制的代理的活动名称集。下面的示例说明了一个复合代理：例4.4Q4def=a（x）.x（y）|ab.bc.c（z）A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-283an（Q4）=an（a（x）.x（y））an（ab.bc.c（z））an（a（x）.x（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（Q4）={a}<${a，b，c}={a，b，c}观察到复合代理可以参与内部通信。即便如此，能够在内部沟通的动作，也能够与外部环境沟通，因为在表达上面没有限制。因此，不会进行范围挤出，表达式中的所有操作都可以参与（独立于输入名称）。对于没有限制名称的代理，输入名称不会限制其活动名称集4.2有反应正如我们在这项研究中所看到的，必须执行内部通信来计算某些表达式的活动名称。特别是，当表达式中出现限制和组合时，由于内部通信，必须进行重新配置。这是必要的，因为某些重新配置可能会增强代理人的通信能力。本节介绍如何计算活动名称，因为内部通信是必要的。例4.5假设代理人Q5和Q6定义如下：284A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-ywdefQ5 =cd.a（x）.xydefQ6=a（b）.b（z）.ywCD（νa）Q5→（νa）（a（x）.xy<$0（v a）Q60cd τ（νa）（Q5 |Q 6）→（νa）（a（x）.xy|Q）→（νa，b）（由|b（z）.yw）→τ （νa，b）（0|yw）→（νa，b）（0|0个）an（（νa）Q5）={c，d}an（（νa）Q6）={}an（（νa）（Q 5 |Q 6））={c，d，y，w}上面的示例显示了一种情况，其中执行了范围挤出，然后由于这样的名称挤出而可以进行操作，否则代理将停止。例如，Agent（νa）Q5无法执行动作a（x），因为名称a在表达式的顶部受到限制。出于同样的原因（νa）Q6具有与agent stop类似的行为（不能执行任何操作）。虽然由于这些受限的动作，两个代理都不能孤立地进行，但如果它们是组合的，并且限制在整个代理范围的顶部，作为a结果，（νa）（Q 5 |Q6）可以执行所有Q5和Q6的 动作，名称集必须包括所有这些行动。 请注意，由于内部操作，名称b的作用域挤出首先被执行，这使得第二个内部操作成为可能。5最后的考虑本文研究了π-施事表达式的主动名的句法特征。由于双相似主体具有相同的活动名称集，因此该名称集的计算对π演算验证技术特别感兴趣。本研究的主要结果可以应用于语义和句法两种验证方法。互模拟检验可以通过重写与结构同余有关的规则来实现在那里，使用π-表达式的范式，如果可以重写为相同的（相同的）范式，则代理是双相似的。除此之外，Hirschko等人[2，3]开发了一种技术，将检查结构一致性的想法扩展到由Sangiorgi [12，13]开发的互模拟A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-285通过对主动名的句法表征，我们还可以发现代理人的潜在非主动名从中，我们可能会发现一部分从未使用过的表达式，因为它前面有语义上不活跃的名称（即不活跃的动作）。这种情况导致停止代理。换句话说，我们可以使用活动名称的表征来减少π表达式，然后增强π演算重写验证技术。这项关于开发新重写规则的工作正在进行中，这些规则消除了进展到停止代理的部分表达式（新规则已经创建，但其证明仍在开发中）。对于语义方法，活动名称的预先计算可以减少状态爆炸。如果在表达式中计算活动名称，则不需要参与不活动的自由名称的转换，从而减少输入转换的空间。例如，在[8]中，转移系统首先考虑整个自由名称集，然后进一步减少到活动名称集对于某些表达式，可能只考虑活动名称来构建转换系统，而不是整个自由名称集。对于包含非活动名称的表达式，状态空间可以先验地减少（不需要用备用的转换和状态来构建自动机并在以后消除它们）。在本文中，计算代理人的活动名称是一个简单的应用程序的活动名称的定义，从研究。然而，必须开发一种有效的算法来进行这种计算。我们已经注意到，当活动名称计算需要内部动作时，recon fixturesexample可以是其他人的alpha转换（主要针对复制代理）。在这种情况下，必须对alpha可转换表达式进行统一，以提高活动名称计算的性能。迄今为止，还没有提出这方面的算法，尽管这对于衡量将有效名称计算应用于现有核查技术（上文提出）的复杂性引用[1] 克里夫兰，W。R.，编辑，[2] Hirschko，D.，自动证明互模拟，在：P. Jancar和M。Kretinsky，editors，Proceedings ofMFCS[3] Hirschko，D.，关于使用最新技术进行互模拟验证的好处，在：Cleaveland [1]，pp.286-299。[4] 琼森湾和j.Parrow，判定一类非有限状态程序的互模拟等价性，信息与计算107（1993），pp.272-302286A.C.V. de Melo / Electronic Notes in Theoretical Computer Science 95（2004）269-[5] 米尔纳河，[6] 米尔纳河，“Communicating and Mobile Systems: the[7] 米尔纳河，Parrow 和D. Walker ，A calculus of mobile processes ，Part I/II ，JournalofInformation and Computation 100（1992），pp. 1-77.[8] 蒙塔纳里湾和M.Pistore，检验有限π-演算的双相似性，在：I。Lee和S.A. Smolka，editors，Proceedings of CONCUR '95，LNCS 962（1995），pp. 42-56.[9] 蒙塔纳里湾和M. Pistore，异步pi演算的有限状态验证，在：Cleaveland [1]，pp. 255-269。[10] Parrow，J.，π-演算的介绍，在：Bergstra，Ponse和Smolka，编辑，过程代数手册，Elsevier，2001页。479-543.[11] Pistore，M.和D. Sangiorgi，A partition refinement algorithm for the - calculus（1996）.[12] Sangiorgi ， D. ， 关 于 互 模 拟 证 明 方 法 ， Mathematical Structures in Computer Science 8（1998），pp. 447URLftp://ftp.dcs.ed.ac.uk/pub/sad/bis-proof.ps.Z[13] Sangiorgi，D.和R. Milner，“弱互模拟问题R. Cleaveland，编辑，CONCUR '92：第三届并发理论国际会议，计算机科学讲义630（1992），pp。32比46