异步π-演算中控制可达性的符号化过程及名称约束的规范语言MSR NC关系

理论计算机科学电子札记98（2004）21-33www.elsevier.com/locate/entcs异步π-演算中控制可达性的符号化过程扩展抽象乔治·德尔扎诺Dipartimento di Informatica e Scienze dell摘要本文研究了异步π演算和在[ 10 ]中提出的结合一阶原子公式（MSR）和名称约束（NC）的多集重写的规范语言MSR NC之间的关系。我们利用这种联系来定义一个健全的和全自动的过程，用于攻击异步π演算中给定的无限状态规范的控制可达性，即，对于具有无限控制、名称生成和名称移动性的移动进程的规范。关键词：移动并发系统，控制可达性，约束，符号状态探索。1介绍在[13]中，German和Sistla建立了Petri网和CCS之间的联系，通过这种联系，像覆盖图构造这样的自动验证方法可以转移到类似CCS的模型（参见[5]）。在这种情况下，单个进程被视为“通信有限状态机”（具有一个位置缓冲器），而整个系统由任意（但有限）数量的进程组成。CCS和Petri网之间的连接已经以几种不同的方式扩展例如在1电子邮件：giorgio@disi.unige.it1571-0661 © 2004由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2003.10.00422G. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-[12]像广播这样的通信机制已经通过传输弧建模。对于[12]中提出的扩展Petri网模型，控制可达性仍然是可判定的。用于指定移动进程的形式主义，通常称为名义演算[14]，代表了值传递CCS的另一个重要扩展。在此设置中，使用通道名称作为值提供了网络的动态重新配置（即过程之间的通信链路）。名义演算的一个著名例子是π演算[16]。在π演算过程中，移动性是通过使用名称作为通信端口来实现的。由于新名称生成、名称移动性和无界控制的存在，π演算中规格的自动验证变得特别具有挑战性，即，它们的状态空间在几个维度上是无限的。应用自动验证技术开发的Petri网的具体规定，在π演算已探讨在不同的作品在文献中。例如，在[4]中，控制可达性已被证明是可判定的异步π演算（πa）的不同片段，通过减少到Petri网的转移弧。Petri网的使用表明了对具有一个无限维（例如进程的数量或名称的数量）的模型的限制。在用于移动系统的其他验证方法中采取类似的限制，例如，[17，18，19]，其中要求进程是无穷的（在执行期间生成的并行组件的数量有一个界限）。我们目前正在研究的研究方向涉及为具有多个无限性来源的并发系统开发的无限状态验证方法的可应用性[10]。具体地说，在本文中，我们将研究异步π演算中给出的移动过程规范与MSRNC [10，11]之间的联系，MSR NC是一种基于一阶原子公式（MSR）和名称约束（NC）的多集重写的规范语言MSRNC是Petri网的保守扩展，其中令牌通过原子公式表示，约束定义了附加到令牌的数据之间的关系。为了建立一个正式的连接，我们嵌入的异步π演算的公式在[4]中提出的基于规范化方程的概念到MSRNC。提出的编码保留（控制）可达性。此外，它允许我们将在MSRNC [10]的背景下研究的攻击控制可达性的验证过程转移到移动过程。具体而言，验证方法是基于未绑定πa规范的向上闭集配置的符号表示这个数据结构可以用来攻击控制可达性问题，使用符号向后可达性。事实上，通过使用编码和专门化预像算子，可以有效地计算πa规范的预像。G. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-23适用于MSRNC规格。由此产生的方法为我们提供了一个全自动和健全的程序，用于验证移动过程的安全属性（通常可还原为控制可达性）。对于通用πa规范，不能保证终止。然而，像抽象解释或启发到Petri网的结构理论的逻辑分析技术可以在这里用来强制终止，以加快分析的速度，或简单地计算近似结果。此外，与MSRNC的一元片段相关的πa片段的研究（向后可达性终止）可以代表一个有前途的研究路线，为移动过程找到新的可判定性结果1.1异步π-演算（πa）异步π演算（πa）是π演算的一个子演算，没有选择和匹配，其中消息发射是非阻塞的[15，6]。πa过程的集合定义如下P：：=0| XY| x（y）.P| P1|P2 | （νx）P| ! P术语0表示空进程。输出项xy表示具有目标x和内容y的异步消息。 对于输入prefix x（y）.P进程在通道x接收任意名称z，然后表现为P[z<$→y]。 过程P[z <$→y]是由z在P中置换y的所有自由循环的结果。x（y）的自变量y约束了P中所有y的自由出现。组合物P|Q由P和Q并行组成。约束（νx）P的行为类似于P，只是它不能与环境交换以x为目标的消息;（νx）的自变量x绑定P中x的所有自由出现。复制！P提供进程P的任意数量的副本（！PP|！P）。在[4]中，Amadio和Meyssonier提出了一个等价的基于归一化参数方程的重新表述，其中重复被替换通过重复。在本文中，我们将讨论一个参考模型。我们使用e→a来表示一个元组a1， . . . . ，anofnames，and[→a<$→→b]toindicateasubsn对于i：1， . . 将 a i 映 射 到 b i . ，n. 因此，设m（v→v）P表示（v v1）.（νvn）P.在[4]之后，标准化参数方程定义如下A（→x）=a（→u）。 （v→v）（a1→y1|.... . . 你 好 。 . |an→yn|A1（w→1）. . . |Am（w→m））我不知道我去。X`乌乌普图x `continpuzzoapplicationsx24G. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-一当A，A1， . . . 表示过程的定义;（边界）名称sin→x，→u，→v都是完全不同的;ai，→yi和w→j是n个从→x，→u，→v开始的名称，其中i：1， . . ， n和j：1，...，M.我们用Fn（P）表示方程A（→x）=P中自由名的集合。一个过程是通过一个非线性参数方程的集合E和一个初始配置来定义的。配置通常定义为形状的归一化过程（v→v）（a1→y1|.... . . 你 好 。 . |an→yn|A1（w→1）. . . |Am（w→m））`messagesx`procesesx两个构形P和Q是等价的，记为P<$Q，如果P在语法上等于Q直到重命名的束缚名，以及并行复合的结合性和交换性。过程的操作语义被定义为在配置上定义的归约关系·πa·的自反传递闭包，如下所示。Le tPbe是构形（νw→）（A（→u））|c（→v）|Q），其中Q是平均值和约束值的乘积，且当方程A（→x）=a（→y）时，l令D ∈ E. （v→z）R表示 名集 →x， →y ， →z 和 w→ 与Fn（ P） 是完 全 不 同 的. Givenσ=[→x<$→→u ，→y<$→→v]及其自然扩张σ∈s，如果σ∈（a）=c，P约化为PJ，记为P<$πPJ，其中PJ=（νw→，→z）（σ<$（R））|Q）。控制可达性问题[4]定义如下。 给定一组方程E包含过程标识符A和初始配置∗P，P是否等于πaQ=v→a。（A（→b）|对于e→b和QJ？例1.1让我们考虑以下等式：Init（a）=（νp）（ap|W ait（p）），W ait（p）=p（x）.EndI（p，x），Resp（a）= a（y）。（v ok）（yok|EndR（y，ok））。给定P =（νc）（Init（c）|Resp（c）），可能的减少如下P=（νc，p）（cp| Wait（p）|（c））πa （v c，ok，p）（W ait（p））|波ok|EndR（p，ok））nπa（v c，ok，p）（EndI（p，ok））|EndR（p，ok））这种简化描述了协议的运行，其中Init和Resp交换专用信道名称p，Resp沿着该专用信道名称p向Init发送确认。 如果我们把方程Start =（v c）（Init（c）|呼吸（c）|开始）G. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-25那么Start将生成我们协议的任意数量的会话1.2规范语言MSRNC设V是一组变量。 我们把名字约束称为合取，... ，n = n的原子公式的形状为真，x > y，x = y，x/= y，或x≥y，x，y∈ V。一个约束条件的解集Sol由所有从V到Z（整数）的使条件为真的求值组成满足约束条件每当太阳（Sol）升起时，设P是一组谓词符号。 原子式p（x1，.，xn）使得p∈ P，且x1，.，xn∈V.原子公式的多集合表示为A1，.，A k，其中符号“，“是不出现在原子公式内的关联交换项构造函数。我们用“，“代替符号“|”[ 10 ]中使用，以避免与π a中的平行合成混淆。在本文的其余部分将使用M，N，. 表示原子公式的多集，k表示空多集，k表示多集并，g表示多集差。一个配置是基础原子公式的多重集合，即所有变量都用整数值实例化的原子公式。MSRNC规则的形式为A1，.，An−→B1，.，B m：其中M=A1，.，An和MJ=B1，.，B m是两个（可能是空的）原子公式的多集，它们建立在P中的谓词上，并且是一个约束，使得V ar（M）<$V ar（M）<$V ar（MJ），其中V ar（F）是公式F中的自由变量的集合。变量之间的等式约束可以是通过规则中多次出现相同变量来隐式定义。MSRNC规则的基础实例定义为Inst（M −→ MJ：）={σ（M）−→σ（MJ）|σ∈ Sol（ε）}其中σ以自然的方式扩展到多集。 规则集合R ={R1，.，Rn}定义为Inst（R）= Inst（R1）. （Rn）.MSRNC规范S是一个元组P，I，R，其中P是一组谓词符号，I是一组（初始）配置，R是P上的有限规则集。S的操作语义是通过在配置上定义的重写关系R来定义的（即，地面多组）如下。给定两个配置M1和M2，M1≠RM2当且仅当存在基原子公式Qs. t的多集M1=N1<$Q，M2=N2<$Q，且N1−→ N2在Inst（R）中一个配置M是可达的，如果存在∗ ∗M0∈ I使得M0<$RM，其中<$R是<$R的传递闭包.26G. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-1m2从πa到MSRNC在本节中，我们定义了一种将无限状态异步π演算规范编码到MSRNC中的方法。在这个初步的工作中，我们将把自己限制在封闭的πa规范和配置上。具体来说，我们将考虑形式为A（→x）=a（→u）的正规化方程。（v→v）RsuchthatFn（R）n{→x，→u，→v}和构形（v→v），Q满足Fn（Q）<${→v}，即，我们假设所有在不同方程上具有作用域的名称已经出现在与初始配置相关联的quantier中。封闭的规范和配置呈现了我们感兴趣的πa的所有特征（新名称生成、无约束并行性、名称和进程移动性）。封闭规范的编码定义如下。名称被编码为整数值。名称上的关系用符号表示为约束。首先，我们将输入动作a→x和输出动作a（→x）设为矩阵mulam（a，→x），其中a，x1， . . ，xn是自由变量。 输入消息将出现在编码过程定义的MSR NC规则的左侧，而输出消息将出现在其右侧。然后，我们使用谓词符号pA对进程标识符A进行编码，将其定义方程中的参数作为变量。最后，我们使用一个原子公式new（f）来跟踪新的值（即分离使用的和未使用的名称）。我们将用几行字来解释它的意思。让我们考虑定义为（v→v）（a1→y1）的初始构型P|.... . . 你 好 。 .|an→yn|A1（w→1）. . . |Am（w→m））P的编码通过MSRNC规则P定义，定义为init，new（f）−→m（a1，→y1）， . . ，m（an，n→y，n），pA（w→1）， . . ，pA（w→m），new（fJ）：f> v1，v1> v2，. ，v r−1> v r，v r> f.用于vrf，fJ，→v的控制器训练确保具有名称si n→v是唯一的，并且全局存储器new（f）包含严格大于所有使用的名称的名称。现在让我们考虑一个标准化参数方程D，定义为A（→x）=a（→u）。（v→v）（a1→y1|.... . . 你 好 。 . |an→yn|A1（w→1）|.... . .你 好 。 . |Am（w→m））G. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-271m·KD的编码通过MSRNC规则D定义，定义为pA（→x），m（a，→u），new（f）−→m（a1，→y1）， . . ，m（an，n→y，n），pA（w→1）， . . pA（w→m），new（fJ）：FJ> v1，v1> v2，...，v r−1> v r，v r> fn→v，f，fJ的正态分布确保了n→v中的项的解的存在。然而，如果D没有新值的生成（即r=0），则我们可以通过分别从左侧和右侧移除new（f）和new（fJ）来简化规则。示例2.1示例1.1的等式的MSRNC编码被定义如下（为了简洁，我们写为pInit，.作为init，.）init，new（f）→ init（c），resp（c），new（f J）：f J> c，c> f。start，new（f）→ start，init（c），resp（c），new（f J）：f J> c，c> f。init（a），new（f）→ m（a，p），wait（p），new（f J）：f J> p，p> f.wait（p），m（p，x）→ endI（p，x）：true。resp（a），m（a，y），new（f）→ m（y，ok），endR（y，ok），new（f J）：f J> ok，ok> f.现在，设P为πa构型，（v→v）（a1→y1|.... . . 你 好 。 . |an→yn|A1（w→1）|.... . . 你 好 。 . |Am（w→m））设t η是从→v到Z的单射，且tη（→v）dentη（v1）， . . ，η（vn）.我们定义P·（η，N）为MSRNC配置m（η（a1），η（→y1））， . . ，m（η（an），η（→yn）），pA1（η（w→1））， . . ，pAm（η（w→m）），n∈w（N），其中N是严格大于η（v1）的 整 数 ， . . ，η（vr）. 设η：→v~Z，ηJ：v→J~Z，且nd{→v}<${v→J}，当η（→v） =ηJ（→v）时，我们定义e η ≤ η j.THE编码的适当性通过以下命题来建立。命题2.2设E是一组封闭的规范化方程，P i是一个封闭的配置，i：1，. ，k使得P1<$πa. πa P k. 则存在η1≤. ≤η k，且N1≤... ≤Nk使得P1（η1，N1）≠E· ... 埃莉·P·（η k，N k）。证据证明是通过归纳法的长度k的推导，有趣的情况是归纳步骤，其28G. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-中k≥1。设P1<$πaG. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-29Kk+11我... 且存在η1≤η2. ≤η k，且N1≤N2... ≤Nk，··P1（η1，N1）≠E· ... Pk（ηk，Nk）. 设Pk为（νw→）（c→z|A（→b）|Q）假设存在一个归一化方程A（→x）=a（→u）。（v→v）R且asub s<$σ=[→x<$→→b，→u<$→→z]su chthatσ<$（a）=c. 然后，Pk<$πaPk+1其中，Pk+1是（νw→，→u）（σ（R）|Q）根据编码的定义，P·（ηk，Nk）是MSRNC配置m（η（c）， η（→z））， p（η（→b）），new（N），QJk k AK K其中reηk（c）v， . . 得 双 曲 余切值.> f.A1r其中RJ是对应于方程体编码的多集设γ是 FJ> v1 的解 ，.，v r> f使得γ（a）= η k（c），γ（→x） =ηk（→b），γ（→u） =η k（→z），且γ（f）=Nk. 因此，tηk+1是以这样的方式定义，即η k≤η k+1且η k+1（v i）= γ（v i），其中i：1，.，r，设Nk+1= γ（FJ）. 然后，p（η（→b）），m（η∈（c）， η（→z）），new（N）−→γ（RJ），new（N）∈Inst（D·）.一kkkkk +1其中，ηk、γk表示ηk和γ到（多个）项s的自然扩展。此外，P（ηk+1，Nk+1）为MSRNC配置Jnew（Nk+1），ηk+1（Q），ηk+1（R）··通过定义<$E·，则得出Pk（ηk，Nk）<$E·Pk+1（ηk+1，Nk+1）。Q命题2.3设E是一个封闭的规范化方程组，E·是它的MSR NC编码，P1是初始封闭配置，M1=P·（η1，N1），对于某个η1和N1。 如果M1=E· ...埃莉· Mk，则存在P2，.，Pk，η2≤. ≤ η k，且N2≤ N3≤. ≤ Nk使得η1≤η2，N1≤ N2，P1πa... πaPk，并且Mi= P·（η i，Ni），其中i：2，.，k.30G. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-证据证明是通过归纳的长度k的推导，并遵循一个模式类似的证明前面的命题。Q3控制可达性控制可达性对于异步π演算中的泛型规范是不可判定的，而对于可以嵌入到Petri网中的受限片段是可判定的（具有转移）[4]。然而，在前面的章节中描述的编码允许我们通过我们在[10]中为MSRNC定义的符号模型检查过程为了研究异步π演算中的控制可达性问题，我们对用任意数量的名称和进程来有限地表示配置感兴趣。我们将通过采用π演算配置的MSRNC编码来实现这一目标具体地说，我们引入了一种向上闭集配置的符号表示，称为约束配置。一个πa约束配置是一个公式m（a1，→y1）， . . ，m（an，→yn），pA1（w→1）， . . ，pAm（w→m），new（f）：n（1）定义变量V={f，a1， . . ，an，→y1， . . ，→yn，w→1， . . ，w→m}使得f是V上的NC约束，并且f，f> x对于任何x∈V xf（在每个可达配置new（f）中，未使用的名称）。πa约束构形的集合S的表示是其元素的基实例的向上闭包，即[[S]]={N|M“N，M ∈ Inst（M），M ∈ S}其中Inst（M：M）={σ（M）|σ∈ Sol（ε）}。因此，像（1）这样的πa约束配置表示形状的πa（v→v）（n（a1）n（→y1）|.... . . 你 好 。 . |（an）|A1（n（w→1））|.... . .你 好 。 . |Am（m（w→m））|Q）其中，Q是通过将Q的解σ与从Z到名称集合→ v的单射（可能不是单射）映射组合而获得的，并且Q是消息s的任意p〇ol，并且由名称s的集合→v定义。这种符号表示允许我们在有限的配置集上进行推理，从而忘记给定运行的实际数量或进程/消息。此外，一阶项的使用使我们可以象征性地G. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-31前R（S）={ A<$N<${new（x）}：| 下面列出的条件（1-7）成立}(1)A <${new（x）} −→ B <${new（x′）}：<$ ∈ R，(2)M <${new（y）}：<$∈S，(3)B′(4)σ=mgu（M′，B′），(5)γ=w∈ V ar（A <$N）x > w，(6)n=nx′，y，→z。（σγ）是不稳定的（7） →z=Var（σ<$N）\（Var（A<$N ）<${x}）.Fig. 1. πa逻辑编码的符号前置算子表示同一进程/消息集合的无限数量的不同实例。约束定义了不同进程/消息的数据之间的关系3.1πa的符号态探索我们现在可以定义一个符号向后可达性过程，该过程计算给定的πa约束配置集合的所有前趋状态，关于E·。 该程序是基于对无限状态MSRNC规范的空间，该规范是由前几节。搜索是基于符号前导算子和蕴涵关系（过约束配置）定义的，两者都在[10]中正式定义。为了简单地解释[10]中给出的过程背后的思想，在本节的其余部分，我们将提出一个特殊化的符号前导算子的类的MSRNC规格产生的编码πa过程。首先，让我们回顾一下一些定义。给定两个具有不同自由变量t和tJ的原子公式（的多个集合），t和tJ的一个单位元是一个代换σ，使得σ（t）=σ（tJ）。最一般的单位元mgu（t，tJ）是幂等代换σ，使得任何其他单位元γ都可以从σ得到，对于某些替换η，γ=ση;最一般的单位元总是存在的，并且是唯一的。在我们的设置中，统一化可能会导致integer变量的新绑定。mguσ也可以被视为（和使用）对于某些变量x，y的等式x=y的合取的形状的NC约束。设S是一个πa约束的构形集合，其变量互不相同.在异步π演算E·中的一个规范的MSRNCR =E·中编码的符号前导算子在图中定义1.一、在图1的定义中，我们结合了统一（通过计算最32G. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-一般unifierσ）和约束求解（通过满足性测试和变量消除）;需要σ来记住通过项unifision引入的整数变量约束图1中的条件3-4确保了在规则的右侧和S中的πa约束配置之间共享的消息和过程的公共池的存在。 图中的条件51允许我们修剪所有违反生成的新鲜度的配置。名称（这是特定于πa编码的）。条件6确保所选择的公共多重集在数据部分上一致（即它们的约束的合取是可满足的）。潜在的量化用于投射所有变量（条件）。(7))在象征性的前像中不需要。符号运算符PreR返回一组πa约束配置，使得[[前R（S）]] =前R（[[S]]）对于任何π的集合， 一 个约束配置S。这个结果来自于[11]中证明的与MSRNC规范相关的符号前导算子的结果。图1中的专用算子在这里只是为了直观地说明如何使用MSRNC的一般搜索技术。工程.符号模型检查过程产生的迭代Pre R的应用，然后可以用来攻击控制的可达性为无限制的π a规格。设P为初始配置，A为我们希望达到的过程标识符。然后，我们可以从sy mbolic配置A（→x），new（f）开始运行符号向后搜索。 ： -是的如果你不介意的话我们必须检查init是否属于结果fixpoint。显然，在MSR NC中，我们可以使用搜索过程来检查这个问题的推广，其中目标配置集通过π a约束配置来定义，如keA1（→xk）， . . ，Ak（→xk），new（f）：n和n表示不同过程名称之间的关系。例3.1作为一个例子，假设我们想检查例1.1中的初始配置开始|new（f）总是生成彼此不干扰的会话，即，我们从来没有达到这样的配置，（v c，d，dJ）（EndI（c，d）|EndR（c，dJ）| .. . ）其中dJ=d，即，会话中涉及的进程总是交换这两个名称。为了检查这个性质，我们可以从πa配置开始应用上面描述的符号向后分析endI（x，y），endR（x，z），new（f）：z/=y，f> x，f> y，f>zG. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-33使用我们基于CLP的实现，该计算在6秒内终止，经过4步，计算22πa约束配置。最终的固定点不包含配置开始，new（f）：true。这证明了我们最初的规范对于任意数量的Init-Resp会话是正确的。4相关及未来工作据我们所知，本文是建立基于约束[1，3，2，10，11]的无限状态验证技术与用于将进程的移动性表示为异步πa演算的演算之间的联系的第一篇论文。我们的验证方法将[1，3]中提出的时间Petri网的思想推广到更一般的并发系统类，这些并发系统可以通过多集重写和约束来指定。在以前的工作中（参见例如技术报告[11]），我们将我们的框架应用于互斥和数据一致性协议（例如缓存一致性）。Cervesato等人在[8]中提出了一阶原子公式上的多集重写来指定作为未来的工作，我们计划将编码扩展到全π演算中的规范，并研究所提出的关系对发现πa和π规范的新的可判定验证问题的可能影响。引用[1] P. A. Abdulla和B.琼森时间进程的网络1998298-312，1998年。[2] P. A. Abdulla和B.琼森协议验证中的通道表示。CONCUR[3] P. A. Abdulla n dA. 不，我不。 Bet et r isBett r th anWell：OnE. LICS[4] R. Amadio和C.梅索尼耶异步π-演算中控制可达问题的判定性。发表在Nordic JournalofComputing上。[5] T.球，S。Chaki和S. K.拉贾马尼多线程软件库的参数化验证。TACAS[6] G.布多异步和π演算。1702年研究报告，INRIA。索菲亚-安提波利斯，1992年。[7] A.布阿贾尼湾Jonsson，M. Nilsson和T.图伊里定期模型检查。CAV[8] I. Cervesato，N.A. Durgin，P.D.林肯，J.C. Mitchell和A.谢德罗夫协议分析的元符号。在Proc. CSFW[9] S. Chaki，S. K. Rajamani和J.作为模型的类型：消息传递程序的模型检查。POPL34G. Delzanno / Electronic Notes in Theoretical Computer Science 98（2004）21-[10] G.德尔赞诺多维参数系统的断言语言。 VEPAS[11] G.德尔赞诺关于参数化并发系统的自动验证TR-DISI，《联合国教育、科学及文化组织》，2002年7月。一个在www.example.com上http://www.disi.unige.it/person/DelzannoG/MSR。[12] J. Esparza，A. Finkel和R.迈尔关于广播协议的验证。LICS[13] S. M. German和A. P. Sistla. 多进程系统的推理。 Journal of the ACM，39（3）：675[14] A. D.戈登关于安全性和移动性的名义演算的注记。FOSAD'00，第262-330页，2000年。[15] K.本田，M.时郎异步通信的对象演算。ECOOP 1991：133-147[16] R. Milner，J. Parrow，and D.沃克移动过程的演算。信息与计算，100：1[17] 联合Montanari和M.皮斯托雷检查有限个π演算的双相似性。CONCUR'95 ，第42-56 页，1995 年。[18] P. Yang，C.R. Ramakrishnan，S.A.斯莫尔卡π演算的逻辑编码：使用表格解析的移动进程模型检查。VMCAI[19] B. Victor，F.莫勒的流动性计算：一个工具的圆周率演算。CAV