强开同余的检验：基于符号技术的χ-演算研究与实例化算法

理论计算机科学电子札记91（2004）4-20www.elsevier.com/locate/entcs强开同余的检验χ-微积分1陈涛略2南京大学软件新技术国家重点实验室，南京周泾阳3南京大学软件新技术国家重点实验室，南京韩婷婷4南京大学软件新技术国家重点实验室，南京建路5号南京大学软件新技术国家重点实验室，南京摘要χ-演算是移动进程演算的一个重要发展。开同余在χ-演算中得到了广泛的研究。然而，仍然缺乏一个算法来检查这种互模拟关系。本文将符号技术应用于χ -演算的研究，给出了不涉及置换上量化的强开同余的一个有效刻画.在此基础上，提出了一种有限控制过程强开同余的实例化算法关键词：移动进程，卡-演算，开同余，符号互模拟，算法。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.12.003T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-2051介绍十多年来，移动进程的各种演算，特别是π演算[13]，一直是并发理论研究的焦点。这些演算与传统的进程演算（如CCS [12]）的区别在于，它们允许进程交换特定的值-通道名称，因此能够处理其通信结构在其演化过程中可能发生变化的进程动态创建通信链接的能力是移动性的核心。最近，一些出版物关注π演算的许多变体，例如异步π演算[8]，πI演算[17]。除了π-演算之外，Fu提出的χ-演算[2]是移动进程演算的一个重要发展。引入χ-演算有两个动机[2]。一种是通过对名字的统一处理来消除π演算中前缀运算的特殊性质，从而得到一种概念上更简单的语言。另一种是具体化一个通信作为切割消除的观点，因此采取了并发理论的证明理论方法，这种方法在函数世界中已经被证明是非常富有成效的。π-演算和χ-演算之间的区别主要在于通信发生的方式。前者采用常见的价值传递机制，而后者采用信息交换或信息更新的观点。在移动进程代数理论的研究中，进程间的互模拟等价性是进程代数中最重要的问题。为了对χ-演算的双相似性进行系统的研究，Fu引入了L-双相似性的概念[3]，并证明了L-双相似性的集合构成一个四元格。还可以证明，著名的双相似性，即开放双相似性和倒刺双相似性分别是双相似格的底元素和顶元素。我们参考其他地方的读者[3]了解更多细节。在[3]中，所有这些同余都是在弱情形下研究的。然而，在强情形下，这四个同余都重合，即强版本互模拟格坍缩为一个元素，在这个意义上，当我们只处理强情形时，开同余是χ对于进程代数，用于检查一个进程的算法是1 支持关于NNSFC（60273034，60233010），863程序（2001AA113110，2002AA116010），国家973计划（2002CB312002），国家自然科学基金（BK2002203，BK2002409）2电子邮件：ctl@ics.nju.edu.cn3 电子邮件地址：jingyang@nju.edu.cn4 电子邮件地址：hantt@ics.nju.edu.cn5 电子邮件地址：lj@nju.edu.cn6T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-20对另一种过程描述语言的双相似性是重要的，这是使一种原型过程描述语言在实际中得到应用的关键。在CCS和π演算中，人们设计了各种各样的算法。一般来说，所有可用的算法可以分为两种类型。一种是划分细化算法[1][16]，这类算法的主要优点是它可以用来获得进程P的最小实现，即在所有与P互模拟的进程中具有最少数量的状态和转移的进程，但是它涉及有限转移图的计算，这是一项相当复杂的任务，在空间上是不充分的;另一种是由于χ-演算是一种重要的移动进程演算，因此有必要研究其互模拟验证问题，但据作者所知，这方面的工作还未见报道。本文的主要工作是给出χ-演算中开同余的一个验证算法。由于众所周知全π-演算是不可判定的，并且很容易证明这一结果在χ-演算中也是有效的，因此本文主要讨论了全π -演算的可判定性。在所谓的有限控制[1] x-演算上，即进程表达式不允许并行组合|出现在递归定义的主体中。 通过限定过程表达式来限定控制过程，是CCS有限状态过程的句法对应，我们得到一个可判定的等价问题。为了得到我们的目的，我们首先在符号框架中引入了开同余的另一种刻画[7][18]，这样我们就可以避免在原始定义中对替换的泛量化在此基础上，给出了一个有效的算法，因为它是足够的实例化的动作的绑定名称与一个单一的新鲜的名称。注意，在本文中，不包括失配算子，并且像往常一样，我们只关注强开同余。本文的其余部分组织如下：在下面的部分中回顾了χ-演算。在第三节中，我们给出了开同余的符号刻画，并证明了它能捕捉（具体的）开同余。在第4节中介绍了第五节是本文的最后一部分，并对相关工作进行了讨论。T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-207µPJJ2χ-演算与开同余在本节中，我们将回顾一些关于χ-演算的背景材料，我们将在其他地方参考读者[4]以获得更多细节。我们将为由以下语法定义的χ-进程集编写CP：= 0 |αx.P |P |P |㈩P |[x = y] P |P + P |A（y1，. ，y n）其中r e α ∈N。 Her e N是由字母s组成的名称范围的集合。 Theset{x<$|x∈N}的系数是d enot edbyyN<$。你的名字（x）P是有界的。一个名字在P中是自由的，如果它在P中不受约束。P的自由名、束缚名和名，以及符号fn（P）、bn（P）和n（P），都以它们的标准意义使用。接下来，我们将使用函数fn（-），bn（-）和n（-）而不作解释。如果α=a，我们把a<$写成α<$，如果α = a<$，我们把a写成a<$。 结合名引入了通常被称为α-e的概念。接下来，我们将确定仅在边界上不同的过程或动作。名称，因此符号表示语法平等和α-等价。此外，每当我们引入一个关于项的二元关系时，我们总是假设它是闭的。-是的操作语义由以下标记的转换系统定义：序列化：成分：αx。P→αxPSqnP→PJbn（μ）n（Q）=ny/xJP→PµP|QCmp0，y/xJcmp1号→沟通方式：P|Q→P|Q{y/x}α（x）PJα（x）Jα<$（x）J→P Q →QP→PQ→QP|Q→τCmm0，PJ{y/x}|QJP|Q→τCMM1（x）（P J）|QJ）P→αxPJQ→α<$yQJx/=yP→αxPJQ→α<$xQJy/x厘米2，τJJCMM3P|Q → P J{y/x}|QJ{y/x}限制：P|Q →（P |Q）P→λ PJx∈/n（λ）P→αxPJx∈/{α，α<$}y/x→P（x）P→λ（x）P条件：Loc0，J㈩Pα（x）→P一号线，J(x) P→τP2号线，JP→λ PJ匹配[x=x]P→λPJ8T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-20→→λ→总计：P→λPJ总和身份：P+Q→λPJP{y，· · ·， y/x，· · ·， x}→λPJdef1n1nA（x ···x ）=P1NA（y，···，y）→PJ1N我们省略了所有的对称规则。 在上述规则中，字母µ的范围为{α（x），αx|非更新作用的α ∈ N <$N<$，x∈N}<${τ}和更新时间t{α（x），αx，y/x}上的多项式r λ|所有动作的α ∈N<$N<$，x∈N}<${τ}。在αx和y/x中，所有的名字都是自由的。在α（x）中，名称x是有界的而另一个名字是免费的。在上面标号的过渡系统中，过程P{y/x}是通过在整个P中用y代替x而得到 的。 置 换 {y1/x1， ···yn/xn}是 从N到N的 函数 ， 其 将 xi映 射 到yi（ i∈{1，···，n}），并且将x映射到自身（x∈/{x1，· · ·，xn}）。 置换通常用yσ，ρ，etc表示。空替换，即N上的恒等函数，写为{}。 的将σ应用于P的结果表示为Pσ。 在下文中，通过α-转换，假设置换σ作为过程的约束名上的恒等式，并保持约束名和自由名之间的分离。我们在下面遵循这个约定，并将在证明中隐式地使用它。下面的技术引理[4]陈述了（具体的）标记变换的性质。引理2.1下列性质成立：(i) 如果P→PJthenP σ→µPJσ。(ii) 若Py/xPJ且xσi=yσ，则Pσyσ/xσPJσ{yσ/xσ}。(iii) 若Py/xPJ且xσ=yσtenP σ→τPJσ。正如前面[18]所做的，我们将使用M，N，L来代表有限（可能是空的）匹配序列。匹配序列定义了名称上的等价关系。给定一个匹配序列M及其等价关系RM，我们用σM表示一个特殊的替换，RM的每个等价类的代表，并将所有名称映射到同一个阶级的代表。如果M蕴涵N，我们写MN，也就是说，只要M中的测试为真，那么N中的测试也为真。类似地，如果M<$N和N<$M都成立，我们写M惠N。 我们说置换σ满足匹配序列M，如果对于每个x，y，它保持M[x=y]蕴涵σ（x）=σ（y），即条件Mσ为真。µT. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-209›→如果σ大于ρ，则我们将符号M<$N推广为σ<$ρ，即ρ（x）=ρ（y）意味着σ（x）=σ（y）。匹配序列和替换之间的关系由下面的引理[18]揭示。引理2.2下列性质成立：(i) 如果M <$N，则Mσ <$Nσ。(ii) 若M <$N，则σM<$σ N。(iii) 若σ <$σJ，则ρ存在s.t. σ= σJρ。接下来，需要修正一些符号。设fa表示集合{αx|a，x∈ N}的自由度s，batheset{α（x）|α，x∈ N <$N<$}的边界条件和u∈s{y/x|x，y∈N <$N<$}的更新日期，并设δ，λ的取值范围为{α（x），αx，y/x|α ∈ N <$N<$，x， y∈N}<${τ}.本节中给出的强开同余是之前研究的开同余的强版本[3][4]，它将Sangiorgi对π -演算[ 18 ]的定义修改定义2.3设R是C上的对称关系，称R是开同余关系，如果只要PRQ，则对任意置换σ，当P σ→δ时，PJ，则存在QJ的唯一性，条件是Qσ→δQJ和P JRQJ。开双相似性是最大的开同余。这很容易证明，确实是一个同余关系。请注意，这个定义可以复述如下：定义2.4设R是C上的一个对称关系，如果R在替换下是闭的，并且当PRQ和P→δPJ，QJx是tss. t。Q→δQJ和P JRQJ。这个定义的形式在其他地方已经考虑过[18]，并将用于第3节的证明。3符号表征正如我们在第1节中所述，检验开同余的一个直接困难是，第2节的定义涉及替换上的量化。在这一节中，我们展示了一个更有效的方法来检查进程的双向相似性，它是基于著名的符号转换系统。符号转换的形式为PM，δ PJ，其中，M是匹配序列，δ是行动上 直觉上，M代表作用δ实际上，它可以从P。 与之相比，10T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-20›→›→µ›→QµJ›→第2节是具体的，因为它们总是可以被激发，而不管术语被放置在什么样的上下文中。在此基础上，我们定义了一个遵循Sangiorgi [18]的符号开同余。χ演算的符号转换语义如下所示。为了便于记法，我们把M和N的并集写成MN。此外，还省略了Sum和Par的对称规则序列化：成分：P›→PJαx.Pbn（μ）n（Q）=nαx›→PSqny/xP›→PCmp0，Jy/xcmp1号P|Q ›→ P|Q沟通方式：P|Q›→PJ|Q{y/x}M，a（x）PN，nby J如果a/=b，则为[ a = b ]›→PQL，τJ›→QJL=0Cmm0P|Q ›→ P {y/x}|QMN，如果a=bM，a（x）PN，<$b（x）J如果a/=b，则为[ a = b ]L，τJ J L=CMM1P|Q<$→（x）（P|Q）MN，如果a=bPM→，axPJQN，<$byQJx=yL=L，y/xP|QPJ{y/x}|QJ{y/x}如果a/=b，则为[ a = b ]如果a=b，CMM2M，axPN，Nbx J如果a/=b，则为[ a = b ]›→PL，τQ›→QJ J L=CMM3限制：P|Q ›→ P |QMN，如果a=bPM→，λPJx∈/n（M，λ）M，λLoc0，PM→，αxPJx∈/n（M）<${α，α<$}M，α（x）位置1㈩P ›→（x）PJ男，y/xP›→P㈩Px∈/n（M）›→ PJ㈩PM→，τPJ2号线，条件：PM→，λPJL=[x=y]PL，λPJM[x=y] ifx/=yMifx=y匹配›→PQJJJJT. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-20111N›→Mδ总计：身份：PM→，λPJP+QM→，λPJ 总和P{y，· · ·， y/x，· · ·， x}M→，λPJ1n1nA（x ···xdef PA（y，· · ·，y）M→，λPJ1n）=下面的技术引理显示了符号转换的一些性质。引理3.1下列性质成立：M，δ(i) 如果P(ii) 如果P<$→Q，则n（M）<$fn（δ）<$fn（P）.M，δQ，则以下性质成立：M σ，δσ· 如果δ∈/u，则P σ<$→Qσ。M σ，τ· 若δ=y/x且yσ=xσ，则Pσ· 若δ=y/x且yσ/=xσ，则Pσ›→Qσ。M σ，yσ/xσ›→Qσ {yσ/xσ}。MJ，δJJ(iii) 如果Pσ›→Q，则以下性质成立：· IfδJ∈ba<$fa，nPM→，δQ与hMJ惠Mσ，δJ<$δσ和QJ<$Qσ.· 如果δJ=τ，则以下性质之一成立：PM→，τQs.t. MJ惠Mσ和QJ<$Qσ。男，y/xP›→Qs.t. M惠Mσ，xσ=yσ和QJQσ。· 若δJ=YJ/XJ，则PM，y/x其中MJ惠Mσ，yJ=yσ，xJ=xσ，QJ<$Qσ {yJ/xJ}。证据 通过跃迁诱导。Q以下两个技术引理涉及具体的和符号的transi- tions。引理3.2如果P σM→PJJ，则以下性质成立：• 如果δ=τ，则以下性质之一成立：· PN，y/xPJ，其中M <$N[x=y]且PJ J=PJσ。›→M· PN，τPJ，其中M <$N且PJ J=PJσ。›→M• 若δi=τ，theNPN→，λPJ与hM<$N，δ=λσ，PJJ=PJσ.证据 通过跃迁诱导。 我们只查一些典型案例。• （P|P）σ→τ（PJJ|PJJ）是从Pσ导出的→AZPJJ和P σ→a<$zPJJ。通过›→J12T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-201 2M1 21个M12M2T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-201312›→2›→1M2τ归纳假设，我们得到与PN→1，bxPJPN→2，c<$yPJM<$N1，az<$（bx）σM，PJJ<$PJσM1 1M<$N2，az<$（cy）σM，PJJ<$PJσM2 2现在，我们可以推断（假设b/=c，相反的情况类似）P|PN1N2[b=c]，y/xPJ|PJ1 2 ›→1 2wth（PJ|PJ）σM<$PJJ|PJJ和M<$N1N2[b=c][x=y]s i nc e xσM=yσM。1 2 1 2• （（x）P）σ→τPJJ是从P σy/xPJJ导出的（注意，通过y的变换，M M→第2部分，（（x）P）σM=（x）PσM且x∈/n（σ））. 通过归纳假设，我们得到PN，z/xPJ，其中M<$N，zσ=y，PJJ<$PJσ。 现在我们推断›→M M（x）PN，τPJ，s由引理a3.1（i），x∈/n（N）.• （P|P）σy/x（P JJ{y/x}|P JJ{y/x}）由P σ导出→axPJJ和Pσ阿伊1 2 M→1 21个M12M→PJJ。 通过归纳假设，我们得到N1，bxJJN2，c<$yJJ与P1›→P1P2›→P2M<$N1，ax<$（bxJ）σM，PJJ<$PJσM1 1M<$N2，ay<$（cyJ）σM，PJJ<$PJσM2 2现在，我们可以推断（假设b c，相反的情况类似）N1N2[b=c]，yJ/xJJ JJJ J J与P1|P2›→P1{y/x}|P2{y/x}（P J{yJ/xJ}|P J{yJ/xJ}）σ M<$（P Jσ M{σ M（yJ）/σ M（xJ）}|P J{σ M（yJ）/σ M（xJ）}）1 2 1 2PJJ {y/x}|PJJ {y/x}1 2和M<$N1N2[b=c]。其他情况类似，由于篇幅限制，我们省略了细节。Q引理3.3如果PM，δPJ，则以下性质成立：• 若δ=y/x且M∈x=y，则P σ M→PJσ M。• Ifδ∈/u或δ=y/x且xσM/=yσM ，则P σMδ→σMPJσ。证据 通过跃迁诱导。 我们只查一些典型案例。• 假设一个b和（P|P）M1M2[a=b]，y/x（PJ{y/x}|PJ{y/x}）是从1 2 ›→1 2PM→1，axPJ和PM→2，a<$yPJ。我们可以和我们的公司合作作为σ和1122M1M2[a=b]M1ρ114T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-20M›→›→σM2ρ2对于某些ρ1，ρ2由引理2.2.根据归纳假设，我们得到（ax）σM1J（<$by）σM2JP1σM1→P1σM1 P2σM1→P2σM2而且可以推断，（ax）σM1ρ1J（<$by）σM2ρ2JP1σM1ρ1→P1σM1ρ1 P2σM2ρ2→P2σM2ρ2（P|P）σ→τ（PJ|PJ）σ1 2 M1M2[a=b]1 2 M1M2[a=b]因为根据M1M2[a=b]<$x=y和引理2.2，xσM1ρ1σM2ρ2=yσM1ρ1σM2ρ2代入{y/x}被σM1ρ1σM2ρ2所• [x=y]PM→，δPJ由PN→，δPJ导出，其中p∈x/=y，δ∈/u，nM= N [x = y]。通过引理2.2，我们可以将σM分解为σN ρ，对于某些ρ。通过归纳假设，我们得到P σNδ→σNPJσ，因此（[x=y]P）σMδ→σMPJσ。其他案件也是类似的，可以毫无困难地证明。Q现在，我们给出开同余的符号刻画，称之为符号开同余。定义3.4设R是C上的对称关系，如果PRQ蕴涵：(i) 如果δ∈fa∈ba且PM→，δPJ，则存在N，λ，QJ，s.t. QN→，λQJ，其中hM<$N，δσM=λσM和PJσMRQJσM。(ii) 如果PM，τPJ，则以下性质之一成立：· N，Q，J存在，QN，τQJ，M <$N和PJσR QJσ。›→M M· N，y/x，Q，J存在于s.t. QN，y/xQJ，其中M<$N[x=y]和PJσRQJσ。›→(iii) 如果PM，y/xPJ，则以下性质之一成立：· N，Q，J存在，QN，τQJ，M<$N[x=y]和PJσM MRQJσ。J JJ›→M MN，yJ/xJJ J J· N，y /x，Q存在s.t. Q<$→Q，其中M<$N，（y/x）σ M=（y /x）σM和PJσMRQJσM。· N，YJ/XJ，QJ存在s.t.QPJσ MR QJσ M。N，yJ/xJ›→QJ，其中M<$N[x=y][xJ=yJ]，符号开双相似性=是最大的符号开同余。现在，我们开始证明和=重合。引理3.5 =隐含了证据 让R={（P，Q）|P = Q}NT. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-2015·→MM›→›→›→›→首先，我们证明了R在替换下是 设S ={（P σ，Qσ）|P =Q，σarbitrary}，我们证明了S是一个符号开同余. 考虑Pσ可以采取的动作δ，我们有以下情况：• δ∈fa∈ba，thenbyLemma3. 1.相变可发生在P σM→σ，δσ对于某些M，δ和P Js. t， PM，δ P J. 由于P = Q，我们有QN，λ QJ，M<$N，δσM<$λσM和PJσM=QJσM。 根据引理2.2，我们有MσNσ，根据Sangiorgi3.1 定义3.4 在这种情况下，这个命题是正确的。• δ=τ，则过渡可以写为如下两个子情况之一：M σ，τPσ对于一些M和PJs。t. PM→，τPJ。 根据=的定义，有两种情况需要核实。但是，使用与第一种情况，这两种情况很容易被检查。M σ，τ·Pσ›→PJσ 对于M和P，S.T.P男，y/x›→P且xσ=yσ。通过对于=的定义，有三种情况需要验证。这里我们N，τ只举一个例子，其他两个是类似的。 取Q›→Q若M∈N[x=y]且PJσ=QJσ，则QσN→σ，τQJσ。 以来xσ=yσ，我们有Mσ<$Nσ，并在第一种情况下使用相同的参数，PJσσMσSQjΣσMσ，因此，Pσ的跃迁可以匹配。M σ，yJ/xJ• δ∈u，则过渡可以写为Pσ<$→PJσ {yJ/xJ}，M和PJs. t. PM，y/XPJ和xσ=XJ，yσ=YJ。根据=的定义，还有三种情况需要验证，这里我们选择了最难的一种。N，yJJ/xJJJJJ JJ J以Q为例›→Q 其中M<$N [x=y][x=y]和P σ M=Q σ M。现在我想，我们有两个子案例。·XJJσ=YJJσ，t∈nQσN→σ，τQJσ。注意，Mσ<$N[xJ=yJ]和PJσ{yJ/xJ}σMσ<$PJσσMσ，在第一种情况下，PJσσMσSQJσσMσ;·XJJσ/= yJJσ，则QσN σ，yJJσ/xJJσ<$→ QJσ{yJJσ/xJJσ}，我们有Mσ<$Nσ[xJ=yJ][xJ Jσ=yJ Jσ]和PJσ{yJ/xJ}σMσSQJσ{yJ/xJ}σMσ。现在我们检查定义2.4中的裸转换匹配，这相当简单。SupposeP→δP_J，t_（max）=3.2，P_（max），δP_J。Sinc eP=Q，由定义δ3.4，Q匹配这种跃迁的唯一可能情况是Q→QJ，且PJ=QJ。3. 3，Q→δQJ. 根据定义2.4，证明是完成Q引理3.6蕴含=。JJ16T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-20›→τ证据 让R={（P，Q）|P Q}我们证明了R是一个符号同余。 设PM，δ PJ. 我们检查以下情况：• δ=y/x且Mx=y，则根据引理3.3，P σM→PJσM。 由PQ，我们有QσM→QJJ，PJσMjj. 根据引理3.2，有两个N，yJ/xJ子案例，我们只选择了更困难的一个来验证。Q›→ QJ，M<$N[xJ=yJ]和QJJ=QJσM，则我们有M<$N[x=y][xJ=yJ]和PJσMRQJσM。yJ/xJJ• δ=y/x且xσM/=yσM，则P σMyJ/xJ →Q σM，其中y=yσM，XJ=xσM。 通过P<$Q，我们有QσMN，yJJ/xJJ→QJJ，其中PJσ M<$QJJ。于外稃3.2，N，Q，J存在，s.t.Q<$→QJ，其中M<$N，yJ/xJ=（yJJ/xJJ）σM，QJJ<$QJσ M，因此（y/x）σ M=（yJJ/xJJ）σ M和P Jσ MRQJσ M。• δ=τ，则P σM→PJσ，通过P<$Q，我们有QσM→QJJ，PJσMjj.根据引理3.2，有两个子情形，这里我们也检查其中之一。N，y/xQJJ J J›→Q其中M<$N[x=y]和P=P σM，则P σMRQ σM。其他的案子就简单多了。Q结合上述两个引理给出本节的主要结果：定理3.7 P= Q证据根据引理3.5和引理3.6。Q4动态算法符号开同余的定义不涉及考虑替换上的泛量化的要求，从而为有效的互模拟检查算法铺平了道路。图1和图2中的算法改编自用于值传递过程[ 10 ]和π演算[ 11 ]的它结合了著名的标准标号转换的系统的策略是使用单个新名称实例化绑定名称。如前所述[11]，它假设一个可数无限子集SN <$N是全序的。函数nextSN（P，Q）返回SN中未出现在状态P和Q的自由名称集合中的最小名称。函数bisim（P，Q）从初始对（P，Q）开始，并调用核心函数match，该函数试图找到包含τττJT. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-2017bisim（P，Q）={NotBisim：=0;returnmattch（P，Q，N）/=N;}match（P，Q，visited）={if（P，Q）∈visitedthenreturnvisited;else if（P，Q）∈NotBisim然后，返回[]。否则{PS{λ|λ∈{fa，u，τ}}={（PJ，M，δ）|PM→，δPJ};QS{λ|λ∈{fa，u，τ}}={（QJ，M，δ）|Q→M，δ};PS BA={（P J{z/x}，M，α（z）|P›→M，α（x）PJ，z =其次SN（P，Q），α∈ N<$N <$};QSBA={（QJ{z/x}，M，α（z））|Q›→M，α（x）QJ，z =其次SN（P，Q），α∈ N<$N <$};PS=λ∈{ba，fa，u，τ}PSλ;QS=λ∈{ba，fa，u，τ}QSλ;temp：=close（P S，QS，visited {P，Q}）;如果temp=0，然后，NotBisim：=NotBisim<${（P，Q）};返回<$;}elseif（temp：=close（QS，PS，temp））=/s然后返回温度;否则{NotBisim：=NotBisim<${（P，Q）};返回<$;}}}Fig. 1. 在线算法（上）18T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-20close（PSet，QSet，visited）={如果PSet=0然后再去拜访。否则，如果QSet=然后，返回[]。否则{hasvisit：=visited;对于每个（P，M，δ）∈PSet{如果存在（Q，N，λ）∈QSets.(i) δ∈fa<$ba<$（M<$N<$δσM=λσM）(ii) δ=τ（（λ=τMN）（λ=y/x MN[x=y]））(iii) δ=y/x<$（（λ=τ<$M <$ N [x=y]）<$（λ=yJ/xJ<$M<$N<$（y/x）σM=（yJ/xJ）σM）<$（λ=YJ/XJ<$M<$N[x=y][XJ=YJ]））（iv）（temp：=match（P σM，QσM，hasvisit））/=<$thenhasvisit：=temp;返回null;}返回hasvisit;}}图二. 在线算法（下）如果两个进程（P和Q）是开全等的，则该对通过匹配来自它们的转移而返回空集核心函数match在两个转换图的乘积上执行深度优先旅行，这两个转换图从未完全创建，而是在构造使它们相等的候选互模拟关系期间一起生成。参数visited用于存储之前遇到的对。如果两个状态之间的转换不匹配因此，给定两个进程P和Q以及一个被访问的关系，函数match首先检查（P，Q）是否已经在关系中。 如果是，则返回关系，否则如果（P，Q）在NotBisim中，则返回值，在相反的情况下，我们生成传出转换和xt状态集请注意，对于绑定操作，使用单个新名称来实例化绑定名称。 然后调用函数close来匹配彼此T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-2019通过符号开同余的定义，其中涉及在将替换σM应用于导数并使用扩展的访问关系时递归调用函数匹配该算法的伪代码在图1和图2中更详细地描述。算法的正确性不难证明。首先，我们给出以下引理来保证算法的终止性引理4.1对于有限控制过程P，Q，bisim（P，Q）总是终止。证据因为我们只考虑有限控制过程，也就是说，过程表达式不允许平行合成-出现在递归定义体中，事实上，它是由不包含平行合成的过程的平行合成建立起来的。所以很容易看出，亲，所搜索的进程空间是有限的，并且通过所访问的参数，该算法存储并检查是否已经针对每个递归检查了所讨论的当前进程。 因此，算法总是终止。Q部分正确性可以通过下面的引理得到。Lemma4. 2如果<$（P，Q）∈visited，P=Q且R=match（P，Q，visited）<$$>，则对<$（P，Q）∈R，P=Q成立.证据 通过对函数匹配的递归次数的归纳，得到了n.• 初始情况：对于n= 0，微不足道。• 诱导步骤。如果R=match（P，Q，visited）不立即返回，则P的所有导数都被Q匹配为开同余，并且每个导数都是归纳开同余。因此，R是由'for'循环在匹配导数时建立的。通过符号开同余的定义，如果被访集满足条件，则对于<$（P，Q）∈R，P=Q也成立.Q根据B个引理a，L∈visited=0，则可得：如果R=match（P，Q，0）/=当n（P，Q）∈R时，P=Q.下面的引理在检查图1和图2中的代码时很容易显示。Lemma4. 3如果R=match（P，Q，N）=N，则P/=Q。现在，我们有以下定理：定理4.4F或有限个P和Q，R=bisim（P，Q，n）总是终止的，且R/=n当且仅当P= Q。20T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-20为了观察算法的复杂性，由于众所周知，在值传递CCS中判定数据独立进程的互模拟等价问题在进程大小上是NP-难的[9]，因此移动进程代数的判定问题，例如π-演算和χ-演算，至少是NP-难的。5结论在本节中，我们总结了我们的工作。我们的贡献在于：（1）给出了χ-演算中强开同余的一个符号刻画由Hennessy和Lin [7]引入的符号技术在进程代数的研究中得到了广泛的应用本文给出了符号转移系统和符号开同余的定义，并讨论了与具体的关系。主要结果是，具体的和象征性的开放一致性。这是首次将符号技术应用于χ-演算的研究中;（2）给出了有限控制过程强开同余的一个检验算法。我们的算法属于非线性范畴。由于在强情形下开倒刺同余与开同余重合，作为副产品，该算法也可以用来检验开倒刺同余。值得指出的是，虽然本文只涉及χ-演算，但我们的结果可以很容易地适用于更新演算[14]和融合演算[15]，它们是χ-演算的非对称和多元版本。目前的工作在很大程度上依赖于符号技术，这是广泛使用的π演算。本文采用Sangiorgi的方法[ 18 ]对开同余进行了刻画，首先引入了开式互模拟，并给出了然而，由于χ-演算的性质，本文中的符号定义涉及较多。在进程代数中检验互模拟关系的出版物很多。对于π-演算，也解决了检查开同余的问题Mobility 算法[19]实现了一种开同余的“on-the-dummy”算法，Pistore和Sangiorgi [ 16 ]提出了我们知道，文献中没有考虑过χ有几个进一步研究的方向。弱版本同余尚未被研究。虽然我们T. Chen等/ Electronic Notes in Theoretical Computer Science 91（2004）4-2021有趣.本文所研究的χ-演算不包含失配算子，考虑χ-演算中的互模拟检验问题是一个有趣的问题。χ-演算已在其他地方提供和研究[5][6]。引用[1] Dam，M.，关于π-演算过程等价的可判定性。理论计算机科学，1997，163：214-228.[2] 傅，Y.，通信的证明理论方法。计算机科学与工程学院学报，1997年[3] 傅，Y.，张志华，张志华，[4] 傅，Y.，Chi演算的互模拟同余出现在信息与计算中。[5] 傅，Y。和Z.Yang。张文，计算机科学与应用，北京大学出版社，2000年，第385 -396页。[6] 傅，Y。和Z.Yang。理解Chi演算中的失配组合子。理论计算机科学，290，779-830，2003。[7] Hennessy，M.和H.林，符号互模拟。Theoretical Computer Science，138（2）：353-389，1995.[8] Honda，K.和M.陈文，基于对象的并行计算，计算机科学，第612卷，第21 -51页，北京，1991[9] 琼森湾Parrow，Deciding bisimulation equivalences for a class of non-finite-state programs.信息与计算学报，107（2）：272-302，11，1993.[10] 林，H.， 传递值的进程的“即时实例化”。 在FORTE/PSTV'98中，第215页-230. Kluwer Academic Publishers，1998.[11] 林，H.，有限控制π-演算的计算互模拟，计算机科学与技术杂志，第15卷，第16期。1，2000。[12] 米尔纳河，通信与并发，Prentice Hall，1989年。[13] 米尔纳河，J.Parrow和D.Walker，移动过程的微积分，第I/II部分。信息与计算学报，100：1-77，1992年9月。[14] Parrow，J. and B.李文，《微积分的新发展》，[15] Parrow，J. and B.李文，“融合演算：移动过程中的表达性和对称性”，《计算机科学中的逻辑》[16] Pistore，M.和D. Sangiorgi，π-演算的分区细化算法，在Proc. CAV' 9 6 ， 计 算 机 科 学 讲 义1 1 0 2 ， S p r i n g e r V e r l a g 。[17] Sangiorgi，D.，π演算，内部迁移和代理传递演算，理论计算科学。167（1996），235-274.[18] Sangiorgi，D.，π演算的互模拟理论，Acta Informatica 3（1996）69-97.[19] 维克多湾和F.Moller，流动性工作台-π演算的工具。在Proc. CAV'94中，计算机科学讲义，第428-440页。Springer-Verlag，1994.