π-演算空间逻辑的图形验证

理论计算机科学电子笔记154（2006）31-46www.elsevier.com/locate/entcsπ-演算空间逻辑的图形验证法比奥·加杜奇1和Alberto LluchLafuenteDipartimentodiInforormatica，Universita`diPisalargo Bruno Pontecorvo 3c，I-56127 Pisa，Italia摘要本文介绍了一种新的方法来验证有限π演算规范的空间属性。该机制是基于最近提出的移动演算的图形编码：每个过程都被映射到一个（排名）图中，使得表示相对于通常的结构同余是完全抽象的（即，当相应的编码产生相同的图时，两个过程完全等效）。用于推理π演算过程的行为和结构的空间属性然后在Caires引入的逻辑中表达，并且它们在过程的图形编码上得到验证，而不是在其文本表示上。更确切地说，图形表示允许提供基于图形编码的简单且易于实现的验证算法（当且仅当给定过程验证给定空间公式时返回true）。关键词：过程演算，空间逻辑，验证。1引言最近的一系列论文主张空间逻辑作为一种合适的形式主义来表达系统规范的行为和空间属性，通常作为微积分的过程给出。除了Hennessy-Milner传统的时间模态之外，这些逻辑还包括用于推理系统的结构属性的算子。例如，连接void表示*欧盟在HPRN-CT-2002-00275SEGRA VIS（可视化建模技术的语法和语义集成）和IST-2004- 16004SEN SORIA（面向服务的覆盖计算机）项目内部分支持的研究。1电子邮件：gadducci@di.unipi.it2 电子邮件地址：lafuente@di.unipi.it1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.03132F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）31（过程在结构上与）空系统一致，公式φ1|满足φ2的过程可以分解为两个平行的分量，分别满足φ1和φ2。此外，这些逻辑还配备了对系统中出现的名称进行推理的机制有几种方法来验证空间属性，在逻辑上用于进程演算（参见[2，3，4]及其参考文献）或其他数据结构，如堆[14]，树[6]和图[5]。在本文中，我们提出了一种新的方法来验证有限π演算规范的空间公式[2]，基于名义演算的图形编码[8]。尽管已经有几篇文章提出了对图形描述系统的验证（见[1，13，16]），但据我们所知，这是第一次尝试基于图形表示对名义演算过程我们的论文被认为是[8]中π演算的图形编码和[2]中空间性质的验证技术的结合，它提供了检查过程图形表示上的空间公式的机制。即使目前的工作集中在π演算的有限片段上（因此集中在空间逻辑的无递归公式上），我们相信它可能会在空间公式的模型检验上提供新的见解，可能将其与图的标准逻辑联系起来;此外，它还进一步证明了基于图的形式主义对于系统设计和验证的充分性。本文的结构如下。第2节介绍了π演算的有限片段和[2]中提出的过程的空间逻辑。第3节回顾了有关排名图的主要定义[7]。第4节提出了将π演算过程编码到排名图中，简化了[8]中已经讨论过的建议第5节介绍了我们的算法验证（封闭）空间公式，简要讨论其计算成本。最后一节概述了未来的研究途径。2π演算与空间逻辑2.1同步（有限）π-演算本节简要回顾了关于同步π演算的有限决定性片段的主要定义。定义2.1（过程）设N被一设置的姓名，不等超过由a，b，c，.. . 设Δ ={a（b），ab| a，b∈ N }是前缀算子的集合，其范围为δ。 进程P是由语法生成的术语，F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）3133P：：= 0 |（νa）P|P |P|δ.P我们让P，Q，R，. 在进程集合P上的范围。假设过程P的自由名集合的标准定义，记为fn（P）对于α-可转换性，关于限制算子（νa）P和输入算子b（a），也是如此。P：在这两种情况下，名字a都被约束在P中，并且它可以自由地进行α-转换。使用上面的定义，进程P的行为被描述为抽象进程上的关系，即，在结构一致的情况下通过封闭一组基本规则而得到的关系。定义2.2（结构同余）过程的结构同余是关系P × P，在过程构造和α-转换下是封闭的，由以下公理集P|Q = Q |PP|（Q|R）=（P |Q）|RP|0 = P（νa）0 = 0（νa）（νb）P =（νb）（νa）P（νa）（P|Q）= P|（νa）Q，其中a/∈ fn（P）定义2.3（归约）过程的归约关系是等价关系R πP × P，在结构同余下闭合，由以下公理和推理规则归纳生成a（b）.P|交流Q→P{c/b}|QP→Q（νa）P→（νa）QP→QP|R → Q|R其中P→Q表示（P，Q）∈Rπ。第一条规则表示两个进程之间的通信：进程ac.Q准备好沿着通道传递（可能是全局的）名称ca;然后它与进程a（b）.P进行递归，并在剩余进程P上用c替换本地名称b（像往常一样，避免捕获名称c）。后者的规则规定了封闭的约简关系方面的限制和平行组成的运营商。最后，我们提出了承诺关系，这是标准标记转换系统语义的变体，在[2]中引入用于验证目的。定义2.4（承诺）设Λ ={τ}{a[b]，ab| a，b∈ N }是承诺标签的集合，范围为λ。过程的承诺关系是关系Rc<$P× Λ ×P，在结构同余下是封闭的34F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）31c1k由以下公理和推理规则集归纳生成P→Qa，c/∈Na，c/∈NP→τQ（νN）（ac.P |Q）→（νN）（P |Q）（νN）（a（b）.P|Q）a[c]（νN）（P{c/}|Q）→b其中P→λ Qm表示λ∈R，Q ∈ P，λ∈R，且（νN）是（νa）. . （νa）对于任意有限个N={a1，.，ak} N。例2.5让我们考虑进程竞态=（νa）ba.aa|b（d）.dc。左边的子进程准备通过通道b发送绑定名称a。 在限制操作符的范围扩展之后，Racehusc o nba sync h r o niz a t io nb：race→τ（va）（aa|ac）。THE剩余过程陷入僵局，因为限制禁止观察。移除限制会导致可能执行提交aa|ac−a→aac（asentovera）a n d aa|ac−a→caa（c发送到a）。2.2空间逻辑本节回顾了[2]中提出的空间逻辑的有限片段定义2.6（逻辑语法）设V是一组变量名，其范围为x，y，. . ，且令λ =Λ λ {x [y]，xy |x，y ∈ V}是可观测量的集合，其范围为π。 空间公式是由语法生成的术语φ：：= T| ¬φ|φ∨φ|虚空|φ|φ |ηφ|x.φ |x.φ|η = η|⟨ξ⟩φ其中η∈VN。我们令φ，φ1，. 在空间公式的集合SF布尔连接词具有通常的含义; void表示在结构上与空过程全等的过程;φ1|φ2对于在结构上与两个子过程的合成一致的过程成立，分别满足φ1和φ2;ηφ对于那些在揭示名称η之后φ成立的过程成立;x.φ表征过程，使得φ分别适用于N中的一个名字和N中的一个新名字（见下文）;η1=η2要求η1和η2相等;如果P可以用标签λ提交给Q并且Q满足φ，则进程P满足φ λφ。一个公式是封闭的，如果它的所有变量都出现在一个存在或一个新鲜的quantifier的范围内。公式φ的自由名集合，记为ffn（φ），与其中出现的名集合一致，因为唯一的绑定算子是变量量化器。如果一个名称不同于公式（过程）的任意自由名称，则该名称在公式（过程）中是新鲜的定义2.7（逻辑语义学）表示φ），映射一个封闭的ACF. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）3135λ公式φ转化为一组抽象过程，定义为：<$T）=P <$aφ）={P| <$PJ.P<$（νa）PJand PJ∈φ）}<$$>）=P\<$$>）<$x.φ）=a∈N （φ{a/x}）<$φφ）=<$φ）<$φ）<$x.φ）=（φ{a/}）\ {P|a∈fn（P）}）1 2 1 2n（φ）xCUP 如果a=b（Φ void）={P|P 0}<$a =b）=否则 ，¢ φ1|φ2）={P|P1，P2.P2P1|P2和P1 ∈ φ1）和P2∈ φ2）}（φ）={P| <$Q.P→Qand Q∈ <$φ）}除了通常的缩写，我们将使用隐藏名称quantifier（Hx.φx.xφ）来对限制名称进行存在性量化。例2.8（空间属性）在我们运行的例子中，两个组件进程准备在同步后通过相同的受限通道发送不同的名称。我们可以用以下公式表示该性质：坠毁 =H x。很好z.y/= z|xz明确地说，该公式首先量化所有可能的受限名称X.然后，它对所有不同名称y，z对进行量化，使得在同步之后，剩余过程可以分解为两个分量，分别在同一通道x上发送名称y和z。2.3一些技术成果我们陈述一些技术引理。第一个是Gabbay-Pitts Property [2]。命题2.9（Gabbay-Pitts）设P是一个过程，φ是一个公式，使得x是唯一的自由变量。然后(i) P∈<$x.φ）i <$P ∈��}）。a/∈（fn（P）<$ffn（φ））x(ii) P∈< $x.φ）i <$P ∈<$x.φ）orP ∈a∈（fn（P）<$ffn（φ））<$φ{a/x}）。这些性质使得存在性和新鲜的量化是可判定的。考虑第1项：通过定义，新鲜名称量化器的语义是根据与既不出现在P中也不出现在φ中的那些名称的替换的并集给出的;因此，新鲜量化x.φ可以通过用任何新鲜名称替换φ中的变量x，然后检查所得公式来确定第二个引理描述了过程的范式这个结果被用在命题2.11上：它涉及到启示算子，说明只有一个36F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）31nn需要检查要显示的通道的有限实例集引理2.10（正规形式）设P是一个过程。那么，P在结构上全等于一个过程（νa1）. （νan）（P1|......这是什么？| Pm), such that a ll ai’s are不同的名字，所有的Pj都是前缀进程，并且{ a 1，. ，an}j fn（Pj）.于是我们将一个标准型记为（νN）Q，其中Q是一组预固定过程，因为限制算子和平行复合算子的阶是无关紧要的。命题2.11（启示集）设P是一个过程，φ是一个闭公式。则P∈aφ）i ∈ a/∈fn（P）且（i）P∈aφ）;或（ii）（νa）（νN）Q是P的正规形且（νN）Q ∈aφ）.为了检验aφ在过程P中是否成立，首先要检验a在P中不是自由的;然后，要么再次检验P，要么确定P的一个标准形式，并检验所有那些通过揭示任何限制名为a而得到的过程。这个结果将简化验证过程，因为标准形有一个明显的对应图形表示。3图及其排序版本我们回顾一些关于（标记超）图的定义，以及它们的排名扩展，参考[7]以获得详细介绍并与标准演示[11]进行比较。在下文中，我们假设一个选定的签名（S，S），其中S是一组运算符（边标签），S是一组排序（节点标签），使得一个算子在S中的元数是一对（s，ω），其中ω∈S<$且s∈S.定义3.1（图）一个图d（over（C，S））是一个元组N，E，l，s，tn，其中N，E是节点和边的集合;l是一对标记函数le：E→n，ln：N→S;s：E→N和t：E→Nn是源和目标函数;并且使得对于所有e∈E，le（e）的 arity 是（ln（s（e）），l（t（e）。我们让l代表函数ln到节点串的扩展，并且我们使用l作为ln和le的简写。我们还用Nd，Ed，ld，sd和td表示图d的分量，在清楚时去掉下标。定义3.2（图态射）设d，DJ是图。一个（图）变形mf：d→DJ是函数fn：Nd→Ndj，fe：Ed→Edj的一个对，它保持标号函数、源函数和目标函数.为了定义进程编码，我们需要对图进行操作。第一步是为它们配备与环境交互的定义3.3（ranked graphs）设dr，dv是没有边的图。 一个（dr，dV）-秩图（秩为（dr，dV）的图）是一个三元组G = dtr，d，v∈ G，其中d是图，r：dr→d，v：dV→d是根态射和变量态射.F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）3137⇐⇐我JvRv⇒R设G，GJ是秩相同的秩图.一个秩图态射f：G→GJ是底层图之间的图态射，其保持根态射和变量态射。我们让d表示（d， d）-秩图d. 有一辆公共汽车r v r v符号，我们有时将根态射和变量态射的图像分别称为根和变量更重要的是，在下文中，我们通常会隐式地将排名图称为其同构类的代表，仍然使用相同的符号来表示它及其组件。定义3.4（顺序和并行组合）设G=dr德乌夫di和H=diRJ dJvJdv是排序图。然后，他们的顺序组成是排名图GH=dRJJrDJJVJJdv，对于dJJ，不相交unionddJ，模由v（x）=rJ（x）诱导的节点上的等价，对于所有x∈Nd，RJJ：dr→DJJ，VJJ：dv→DJJ是唯一诱导箭头.设G=ddH=dJRJ dJvJdJ是分级图。然后他们的r vrv平行合成是排序图GH=（ddJ）rJJdJJvJJ（dRr ⇒⇐vv对于dJJ，不相交的并集d dJ，模由下式导出的节点上的等价J和v（y）=v（y），对于ally∈Ndv<$NdJ，an drJJ：drdJ→ dJJ，vJJ：dvdJ→ dJJ是唯一诱导的箭头。序列合成G<$H是通过取G和H下的图的不交并，并将G的变量与H的相应根粘合而得到的。类似地，通过取G和H下的图的不交并，并将G的根（变量）与H的相应根（变量）粘合，得到平行合成G<$H。这两个操作是具体定义的，但它们旨在作用于同构类的排名图（因此，具有相同的排名）。事实上，结果与代表的选择无关，直到同构。例3.5（一些图）图1描述了两个排序图（我们运行示例的编码的一部分）：它们的顺序组合出现在图2（左）中。图3表示图1中的曲线图的平行组成。二、根（变量）态射的域中的节点被描绘为左（右，分别）上的垂直序列;变量和根态射分别由从右到左和从左到右的虚线箭头表示。边缘由一个带框的标签表示，从箭头指向目标节点离开的地方，到箭头从源节点到达的地方;目标节点的顺序通常是触角起点的顺时针顺序，即使有时它是由触角上的编号表示的：对于图中最左边的图的边缘 1的序列是（v（p），v（b），v（a））。图1的最左边的图具有秩（{p}，{p，a，b}）、四个节点和一个节点。r（x）=r（x），对于allx∈Ndr<$N dRJ38F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）31R、你好，R、你好，pz·，pz·，zou，tz·，az，，rabzzzz，，rbFig. 1.排序的图出b，a（左）和aaJid{a，b}（右）。pzz0zzzz1z，，r•出来•出来21·r，razh，，rb◦Bpz·，zin，0z·，zou，t0z·，2ZZ，，rc21rz，图二.排序的图出b，a，a，b（aaJid{a，b}）（左）和b，b（d），dcJ（右）。pz·，out0z·，zou，tz·，zh，，ra121zin，0z·，zou，t0z·，2zh，，rb阿夫拉克但是，21图三.排序图是一个简单的排序图，它是一个简单的排序图。最右边的图有秩（{p，a，b}，{a，b}），四个节点和一条边标记为out。为了图形的方便，在底层图中出现的具有不同标签的节点也被不同地表示。图表达式是一个语法术语，包含作为常量的分级图，以及作为操作符的并行和顺序组合。一个表达式是良构的，如果这些运算符的所有出现都被定义为子表达式的秩，根据定义3.4：它的秩是归纳计算的，它的值是通过计算它的运算符得到的图。4从流程到图表现在，我们基于[8]中提出的编码，将π演算过程编码到排名图它是由签名（π，Sπ）构建的，并且它保持了结构一致性。排序集Sπ是{sp，zou，tz·，，F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）3139sn}：直观地说，从排序为sp的节点可达的图对应于一个进程，而排序为sn的每个节点代表一个名称。 集合π包含三个运算符：{in，out}of sort（sp，spsnsn），{v}of sort（sp，sn）。显然，运营商40F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）31·，，rppz·，zop，zrbpz·，az，，ra一个z轴，pz·，见图4。秩图op a，b（对op∈ {in，out}），ν a，id a，0a和0p.in和out分别模拟输入和输出前缀;运算符ν代表限制。此外，请注意，没有明确的运算符来解释并行组合。第二步是一类图的特征，这样所有的过程都可以被编码到一个表达式中，该表达式只包含那些图作为常数，并包含并行和顺序组合作为二元运算符。让p/∈ N：我们的选择如图4所示，对于所有a，b∈ N。最后，设idΓ是x∈Γidx的简写，对于一个名称集合Γ（因为排序是无关紧要的）。将过程编码为排序图，将每个有限过程映射到图形表达式，如下所示。定义4.1（过程的编码）设P是一个过程。将进程P映射到排序图的编码图P J根据以下规则由结构归纳法定义⎧如果a/∈fn（P）（νa）PJ=（PJva）（0aidfn（P）\{a}）否则CUP|QJ=0p J= 0 pab.PJ=outa，ba（b）.PJ=ina，b<$（注意（νa）的条件规则。P：它是去除无用限制算子的必要条件，即：那些绑定一个名字没有出现在这个过程中。该映射是良好定义的，因为所得到的图表达式是良好形式的，并且编码的图PJ是秩（{p}，fn（P））的图。例4.2（映射一个进程）为了直观地理解前面规则的含义，我们展示了进程ba.aa（我们正在运行的示例的一个子进程）的编码结构，ν，阿F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）3141你好，pz·，zν，out0z·，zou，tz·，121zin，0z·，zou，t0z·，2zr，，vz，rb阿夫拉克◦¸21图五.排序图<$（νa）ba.aa|b（d）.dcJ.图示如图2（左）所示。ba.aaJ=outb，a（aaJid{ a，b }）的表示与（outa，aid{a，b}）（0pid{a，b}）重合，后者通过其图形表示清楚地匹配。另一方面，在图1B中描绘了水迹J的图形表示。五、映射π·J不是满射的，因为存在秩为（{p}，Γ）的图不（同构于）任何过程的像。然而，让我们把注意力限制在验证一个温和的句法条件的过程上，也就是说，禁止出现输入前缀，如a（a）。然后，我们的编码是健全和完整的，正如下面的命题所述（改编自[8]）。命题4.3设P，Q是过程。那么，P <$Q i <$$>P J =<$QJ。5一种验证算法本节介绍一种算法，用于验证过程图形表示上的空间公式。它以一个待验证的封闭公式φ和一个排序图G=rdv作为输入，使得对于某个过程P，G= rPJ，并返回一个布尔值，即，如果P∈φ，则返回true，否则返回false它是利用图形编码的结构，通过对要验证的公式进行案例归纳来定义的对于任何进程P，第一个调用是eval（φPJ，φ）。检查Booleans、Void和Name相等性。计算布尔公式和名称相等的过程是自解释的，并且为了检查void，它可以确定d是否没有边。42F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）31returntrue;return<$eval（G，φ）;caseφ1<$φ2returneval（G，φ1）<$eval（G，φ2）;格空 如果Ed=0，则返回 true，否则返回false;returna=b;检查成分（φ1|φ2）。该算法建立了所有的对，对应于一个分解的图在考虑。这些图是通过分裂从根发出的未标记为ν的边的集合而获得的。后一个集合在下面的伪代码中由E表示案例φ1|φ2E← {e ∈Ed|sd（e）= r（p）和ld（e）/= v};R← {（e，n）∈ Ed× Nd|sd（e）= r（p）<$ld（e）= v <$td（e）=n};foreachE1E doG1←由E1生成的G的子秩图;G2←E\E1生成的G的子秩图;foreach（e，n）∈Rdo若n∈d1且n∈d2，则继续最外环，若n∈d1，则d1<$d1<${e};若n∈d2，则d2<$d2<${e};如果eval（G1，φ1）等于eval（G2，φ2）则返回true;返回false;直觉上，E中的每条边对应于G所表示的过程的一个预固定子过程。然而，并不是每个图分解都对应于正确的过程分解，其原因基本上由结构公理（νa）（P|Q）= P|（νa）Q，其中a/∈ fn（P）。换句话说，在选择图分解G1和G2之后，需要考虑放置在顶部的限制算子范围内的所有名称并检查每个名称仅出现在两个图中的一个中。因此，该过程计算受限节点的集合R（连同对应的边），并且它检查R中的每个受限节点n是否属于d1和d2。如果是这种情况，那么所选择的图分解是无效的，因为对应于ln（n）的名称将在两个子过程中自由出现。另一方面，如果n仅出现在di在检查R中的每个受限节点后，算法递归地评估G1是否满足φ1，G2是否满足φ2。子排序图对应于从节点（即r（p））和一组相邻边可达的通常子图，并且它们通过深度优先探索而构建在线性复杂性中。F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）3143正在检查名称量化（x.φ）。我们利用命题2.9，让x在dvffn（φ）中的节点上取值，因为dv表示由G编码的过程中的自由名。如果在所有这些情况下结果都是负的，我们检查φ{a/x}是否对新名字a成立，依赖于新量化的情况casex.φ对每个a∈dvffn（φ）do，如果eval（G，φ{a/x}）则返回真;intn = int n（n）;检查新鲜定量（x.φ）。我们再次利用命题2.9。我们在dv和ffn（φ）中选择一个名a对于工艺和配方都是新鲜的名称然后，我们在G上评估φ{a/x}。casex.φa←new name not indv ffn（φ）;intn（n，n）;检查承诺（<$λ<$φ）。该算法区分了λ的三种不同情况。如果λ是τ，则该算法寻找在相同名称节点上操作的外标记边和内标记边。一旦找到这样的对，就通过构建残差图来模拟同步，即，通过将两个操作符的延续与进程的根以及正在发送的节点与正在接收的节点合并。然后，该过程移除两个涉及的边，并且它执行垃圾收集，删除限制算子和所有隔离节点的无用出现（即，这些节点唯一地出现在被移除的操作符的目标序列中）;最后，算法检查φ是否在结果图中保持输入和输出承诺的计算类似：注意，根据承诺语义，输入动作可能会收到一个已经在流程中自由出现的名称b，因此需要进一步控制。44F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）31案例<$λ<$φ如果λ=τ，则对于e1， e2∈Ed，其中ld（e1）=out，ld（e2）=in，如果sd（e1）=sd（e2）=r（p），td（e1）[1] =td（e2）[1]，则G1<$G;d1<$d{r（p）=td（e1）[0]=td（e2）[0]，td（e1）[2]=td（e2）[2]}\{e1，e2};如果eval（gc（G1），φ）则返回true;如果λ=ab，则对于每个e∈Ed，其中ld（e）=outdo如果sd（e）=r（p）且td（e）[1]=v（a）且td（e）[2]=v（b），则G1<$G;d1<$d{r（p）=td（e）[0]}\{e};如果eval（gc（G1），φ）则返回true;如果λ=a[b]，则对于每个e∈Ed，其中ld（e）=indo如果sd（e）=r（p）且td（e）[1]=v（a），则G1<$G;d1<$d{r（p）=td（e）[0]}\{e};如果b∈dvthend1<$d1{v（b）=td（e）[2]};eledv1<$dv{b};v1<$v{b<$→td（e）[2]};如果eval（gc（G1），φ）则返回true;返回false;垃圾收集阶段gc（G1）花费线性时间，因为它检查最多三个节点的连通性。它确保生成的图表示提交后剩余进程的编码：为此，垃圾收集还可以从变量图中删除节点检查Revelation（aφ）。根据命题2.11，算法首先检查a在G所表示的过程中是否自由，即它是否属于dv。如果这失败了，算法就会尝试检查P是否满足φ。最后，它将任何受限制的节点显示为a：这是通过删除从d的根向外的v-标记边并将a添加到变量来完成的。情况aφ如果a∈dv，则返回false;如果eval（G，φ），则返回true;对于每个e∈Ed，其中ld（e）=ν，sd（e）=r（p）doG1<$G;d1<$d\{e};dv1<$dv{a};v1<$v{a<$→td（e）[0]};如果eval（G1，φ）则返回true;返回false;例5.1种族是否=（νa）ba.aa|b（d）.dc满足属性crash=H x. 很好z.yzτ（xyT|xz 该算法将首先尝试并修复F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）3145变量x作为一个新的名称（比如a），并尝试将其显示为46F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）31但是，outz·，pz·，outz·，ra，ra你好，pz·，zou，tz，n，ra阿夫拉克pz·，z，，rar，rc见图6。 排名图|acJ（左）和两个子排名图（右）。限制性名称中的一个。因此，x被揭示为名称a，并且构建了图3接下来，算法将尝试找到同步。找到在节点b上通信的输入和输出边，并构造残差图：后者在图6（左）中描绘。然后，该算法查看每个可能的分解，在这种情况下（除了其中一个分量为空的平凡分解之外）是两个，即用两个外标记边缘形成有序对的两种可能性。对应的子排名图在图6（右）中表示。在分解中，首先是顶部图，然后是底部图，算法将成功地找到在通道a上发送名称a和c的承诺，从而返回true。我们现在声明所提出的评估程序的正确性定理5.2（正确算法）设P是一个过程，φ是一个闭公式.则P∈φ）i eval（PJ，φ）= true。关于算法的复杂性，大多数操作依赖于枚举边或节点的集合，因此需要多项式时间。唯一的例外是组成的验证，其中必须考虑指数6结论和今后的工作本文介绍了一种基于图形的技术，用于验证有限π演算规范的空间属性。我们只考虑了微积分的决定性部分，以便尽可能简单地表示：选择算子可以包含在其中，而不需要花费太多的精力。除了直观吸引人之外，图形表示也是抽象过程的典型代表，因为两个过程在结构上是一致的，它们被映射到相同的排序图（直到同构）。编码也有一个独特的优势，相对于大多数的approaches图形实现演算与名称的移动性（如你好，zou，tF. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）3147如Milner本文提出了一种有效的空间属性验证机制，从而为[2]中提出的技术提供了一种建设性的替代方案。事实上，即使没有进行正式的比较，我们的图算法也利用了过程的关于效率，我们的最坏情况是并行组合的验证，因为图分解对于一般公式是指数的。同样，没有任何比较可以追溯到结果[15]，因为他们的算法的效率没有完全报告。我们不知道有任何其他的工具可以用来检验空间逻辑中关于π演算过程的公式。然而，除了任何consideration的效率和可用性的算法，我们认为，我们的论文的主要贡献是进一步说明的有用性的图形技术的设计和验证的并发系统：索赔是支持一个健全的和完整的编码空间公式到公式的时间图逻辑，将出现在其他地方。本提案的重点是π演算的有限片段。我们目前正在研究如何推广我们的方法，以便包括递归规范，从而考虑[2]的完整空间逻辑。[8]的原始图形编码已经考虑了递归过程，因此我们的工作将扩展该算法。最后，我们正在计划实现我们的方法，可能是通过将其集成到现有的图形设计系统分析工具中，如[9，12]。引用[1] Bald an，P. 、杨A. Cor a d ini and B. Koénig，Astaticanailystechniqueforaphtran sfor mationsystems ， in ： K.Larsen 和 M. Nielsen ， 编 辑 ， 并 发 理 论 ， Comp.Sci.Lect.Notes 。 第 2154（2001）号来文，第2154（2001）页。381-395.[2] 凯尔湖行为和空间观测的逻辑为π演算，在：I。Walukiewicz，编辑，软件科学和计算结构的基础，Comp.Sci.Lect.Notes。2987（2004），pp. 72比87[3] 凯 尔 湖 和 L. Cardelli ， A spatial logic for concurrency （ Part I ） ， Information andComputation186（2003），pp. 194-235。[4] 凯尔湖和L. Cardelli，并发的空间逻辑比较科学322（2004），pp. 517-565[5] 卡尔代利湖，Gardner和G. Ghelli，用于查询图的空间逻辑，在：P. Widmayeret alii，编辑，自动机，语言和编程，Lect.Notes in Comp.Sci. 第2380（2002）号来文，第2380页。597-610[6] 卡尔代利湖，Gardner和G. Ghelli，Manipulating trees with hidden labels，in：A. Gordon，编辑，软件科学和计算结构的基础，Comp.Sci.讲义。第2620（2003）号来文，第2620（2003）页。216-23248F. Gadducci，A.Lluch Lafuente/Electronic Notes in Theoretical Computer Science 154（2006）31[7] Corradini，A.和F. Gadducci，An algebraic presentation of term graphs，via gs-monoidalcategories，Applied Categorical Structures7（1999），pp. 299-331[8] Gadducci，F.，项图重写和π-演算，在：A。Ohori，编辑，Programming Languages andSemantics，Lect。对比中的注释Sci. 2895（2003），pp.37比54[9] Kozioura，V. 和B. Künig，AUGUR：Anunfoldin g-baseddeviricationtoolforGTS，availableathttp://www.fmi.uni-stuttgart.de/szs/tools/augur.[10] 米 尔 纳 河 ， 双 图 反 应 系 统 ， 在 ： K 。 Larsen 和 M. Nielsen ， 编 辑 ， 并 发 理 论 ，Comp.Sci.Lect.Notes。第2154（2001）号来文，第2154（2001）页。16-35.[11] Plump，D.，项图重写，在：H。Ehriget alii，editors，Handbook of Graph Grammars andComputing by Graph Transformation，II ：Applications，Languages and Tools，WorldScienti fic，1999，pp. 3-61[12] Rensink，A.， GROOVE模拟器：状态空间生成工具， 在： J. 普法尔茨M.纳格拉和B。Bo？len，editor，ApplicationsofGraphTrannsforormationswithithndustrialRelevance，Lect. Notes in Comp. Sci.第3062（2003）号来文，第3062（2003）页。479 http://sourceforge.net/projects/groove。[13] Rensink，A.， 关于模型检验图文法，M. Leuschel，S. 格鲁纳和S. Lo Presti，editors，Automated Verification of Critical Systems，Technical Report DSSE-TR-2003-2，School of Electronics and Computer Science，University of Southampton（2003）.150-160[14] 雷诺兹，J.，Separation logic：A logic for shared mutable data structures，in：Logic inComputer Science（2002），pp.55比74[15] Torres Vieira，H.和L. Caires，空间逻辑模型检查器用户[16] 好的，D。，Automatedformalverificationofvisualmodelinglanguagesbymodelchecking，Softwareand Systems Modeling3（2004），pp.85比113