π演算的模态逻辑及模型检验算法

理论计算机科学电子笔记123（2005）19-33www.elsevier.com/locate/entcsπ演算的模态逻辑及模型检验算法1陈涛略2南京大学软件新技术国家重点实验室，南京韩婷婷南京大学软件新技术国家重点实验室，南京建路南京大学软件新技术国家重点实验室，南京摘要π-演算是移动进程演算中最重要的一种，在文献中得到了广泛的研究。时态逻辑被认为是描述方便和抽象之间的一个很好的折衷，可以支持有用的计算应用，如模型检查。本文利用继承自π-演算的符号迁移图对并发系统进行建模。一类广泛的过程，即有限控制过程可以表示为有限符号转移图。引入了一个新版本的π-μ-Logic作为π-演算的合适的时态逻辑。由于我们区分了命题和谓词，递归和一阶量化之间可能的相互作用就可以解决了。 给出了模态逻辑的一个简明的语义解释。在此基础上，提出了一种基于Winskel标记集方法的模型检测算法，该算法对定点算子进行了处理。 至于名称实例化的问题，我们的算法遵循的“上的-的-的”风格，并系统地采用示意图名称。证明了算法的正确性保留字：π演算，符号转换图，π-μ逻辑，模型检测算法。1国家973计划（2002CB312002），国家自然科学基金（60273034，60233010），国家自然科学基金（BK2002203，BK2002409）资助2电子邮件地址：ctl@ics.nju.edu.cn1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.04.04320T. Chen等人理论计算机科学电子笔记123（2005）191介绍在过去的几十年里，移动进程的各种演算，特别是π演算[13]，一直是并发理论研究的焦点。由于用代数方法来建模和描述系统的相关性质（如移动性、安全性）的局限性，大量的研究集中在微积分的模态逻辑上。模态逻辑（特别是时态逻辑）被认为是描述方便性和抽象性之间的一个很好的折衷。此外，许多模态逻辑支持有用的计算应用，如模型检验.作为一种描述移动和动态过程网络的强大语言，基于π演算的一般时态和功能性质的验证问题得到了深入的研究。 已有文献给出了一些π演算的模态逻辑系统。据我们所知，最初的工作属于Milner等人。在[14]中，他们为Hennessy-Milner逻辑[8]提供了一组扩展，并证明了其中两个扩展刻画了两个互模拟等价，即强晚期和早期互模拟。然而，它们的扩展相当简单。这可能是由于他们的动机，以描述双同时关系。在[1][4]和最近的[6]中，Amadio和Dam通过定点将递归引入模态逻辑，如在命题μ-演算中，因此能够表达具有无限行为的过程的属性。这些逻辑系统可以称为π-μ-演算。这两篇论文的主要关注点是制定证明系统，用于导出断言过程是否满足公式的语句。而且，从我们的角度来看，这两篇论文中的合成证明系统虽然很微妙，但有点繁琐，尤其是完备性证明。我们认为这是因为缺乏足够的“象征性”信息。我们的出发点是在某种意义上弥补这一缺陷。众所周知，符号技术已被广泛用于名传递演算，特别是提供了完整的互模拟等价性证明系统，并设计了有效的互模拟检验算法，例如[10][9]。在本文中，我们借用这种技术的思想，并适应它设计模型检测算法。我们简要地介绍一下我们的主要思想。在本文中，首先，我们使用符号转移图来建模并发系统。一个广泛的过程类，即有限控制过程可以表示为有限符号转移图。 以及从过程项到符号转换图的转换 是直接而简单的。其次，我们引入了一个新版本的π-μ-Logic，它是模态μ-演算的扩展，带有对名称的布尔表达式，以及名称输入和输出的原语，作为π-演算的适当时态逻辑。注意，在我们的π-µ-逻辑中，“绑定输出”模态值得注意。新的名称量化由于皮茨这是T. Chen等人理论计算机科学电子笔记123（2005）1921N在空间逻辑[2]中使用的递归方法是隐式的，因此我们必须面对递归和一阶量化之间可能的相互作用的问题。为了解决这个问题，我们在逻辑系统的语法中区分了命题和谓词，从而在不需要“属性集”概念的情况下，对模态逻辑给出了一个简洁的语义解释。我们将更多细节推迟到第4节。我们工作的主要贡献在于本文所介绍的逻辑的模型检测算法。我们遵循著名的Winskel在名字实例化问题上，我们遵循“on-the-dummy”风格，系统地使用了所谓的模式名，即当前节点的新名字集和带有一个新名字的证明了算法的正确性本文的其余部分组织如下：π演算的一些背景材料，特别是符号转换图在下面的部分中进行了回顾第三节介绍了π-μ-逻辑，给出了它的语义，并讨论了它的一些有用的性质。第四节给出了模型检测算法，并证明了算法的正确性。第五节是本文的最后一部分，并对相关工作进行了讨论。请注意，在这个扩展的摘要中，由于空间限制，省略了大部分详细的证明。我们建议感兴趣的读者阅读这篇论文的全文。2π-演算与符号转移图在这一节中，我们回顾了π-演算的一些背景知识，并介绍了符号转移图的概念。布尔表达式和替换π演算的基本实体是名称，即通信信道的标识符。令a，b，m，n 是一个可数无限的给我一个。 一个我的向量或s将被一个，一个。 . .布尔表达式，范围为φ，，由BNF定义如下：φ：：=真|x = y| ¬φ|φ∧ φ我们将为布尔表达式集编写BExp，并使用false，x y和φ表示<$true，<$（x=y）和<$（<$φ<$）。布尔公式Ev的求值是函数Ev：BExp→22T. Chen等人理论计算机科学电子笔记123（2005）19|联系我们联系我们[1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19][10][11][19][10][11][10Ev （ x=x ） =true Ev （ x=y ） =false ifx/y Ev（<$φ）=<$Ev（φ）Ev（φ）=Ev（φ）<$Ev（φ）用σ，δ等表示的置换是从N到N的部分映射. 如果σ=[y_n/x_n]，则当x_n的值与y_n的值相等时，m（σ）={x_n}，cod（σ） ={y_n}，n（σ） ={x_n}|{y_n}.如果fn（φ）≠V，则yφ是V上的一个布尔表达式.注意，对于x∈dom（σ），σ将x映射到y上，对于x∈/do m（σ），σ将x映射到自身上。在等式中，我们将用σ表示空的子空间，σδ表示σ和δ的合成。置换σ[x<$→z]与σ相同，只是它将x映射到z而不是xσ。σ对V<$N的限制，记作σ<$V，定义为如果x∈V则返回xσ，否则返回x本身。对于每一个名字x，函数νx在文献中以一种标准的方式定义我们建议读者参考[10]以了解详细信息。一个代换σ满足φ，记作σ| = φ，如果Ev（φσ）=真。 我们写φ表示σ|= φ表示σ|对于任何代换σ，φ =，φ =表示φ和φφ。φ是相容的，如果没有x，y∈ Ns. t。φ[x = y]和φ[x=y]与此同时 否则就是不一致的。很容易看出，如果存在替换σ，s. t，φ是相容的。σ=φ。φ是有效的，如果Ev（φ）=true。 注意，对于一个有效的布尔表达式φ，我们有σ |= φ对于任何替换σ，因此它可以表示为真。仅交换一对名称的置换，称为换位，以θ为界，在以后的技术发展中将发挥特殊的作用。更准确地说，n和m的换位，记作mn表示置换σ：m，nn，m。事实证明，换位是一个有用的工具，在证明性质的新鲜的名字。符号转移图由于π演算和相关概念是众所周知的，为了节省空间，我们将省略对其语法的详细介绍。 不熟悉它的读者可以参考一些标准文献，例如[13]。我们只指出，在本文中，我们不允许并行复合算子| 出现在递归定义的主体中，并将这种受限语言称为“通过将过程表达式限定为有限控制过程，这是CCS有限状态过程的语法对应物，下面的符号转换图是有限的，因此我们得到可判定的模型检查问题。现 在 ， 我 们 引 入 符 号 转 换 图 （ Symbolic Transition Graph ， 简 称STG）的概念作为π演算过程项的一个新模型接下来，让SAct=T. Chen等人理论计算机科学电子笔记123（2005）1923∈∈φ，α→nGG{τ}{a（b），a<$b，a<$（b）|a，b∈N}表示对称作用的集合。对于N中的一组名称V，函数new（V）返回N \ V中最少的名称。定义2.1（符号转换图）符号转换图（Symbolic transition Graph，简称STG）是一个有根有向图，其中每个节点n都有一个自由名的有限集合fn（n），每条边都用元组（φ，α）标记，其中φ是布尔表达式φ BExp，αSAt是符号动作。 一个STG是良构的，如果其中（φ，α）是从n到m的边的标号，写为n<$→m，则fn（φ）<$fn（m）和fn（n）<$fn（m）<$bn（α）.真α我们写m›→ n为mn为简单起见。给定π中的一个过程t，微积分，相应的STG可以由一些系统的规则生成。由于篇幅所限，我们省略了细节。值得指出的是，对于有限控制过程t，生成符号转移图的过程t是有限的。我们没有给出π -演算项的运算语义，而是给出了STG的具体运算语义。首先，我们介绍一些符号。给定一个STG，一个状态nσ是由一个节点n和一个与之相关的替换σ组成的一对。自由名集合fn（nσ）定义为fn（n）σ，并且可以理解，σ被限制为fn（n）。后期（具体）操作语义被定义为由规则生成的状态之间的最小关系，如下所示：φ，τ›→nτφ，a′bσ|= φm›→ nσ |= φφ，a（b）mσ→nσa<$σbσσ σφ，a<$（b）M›→naσ（c）σ|=φ <$c∈/fn（mσ）m›→na<$σ（c）σ|=φ <$c∈/fn（mσ）mσ→nσ[b<$→c]mσ →nσ[b <$→c]标签转移的一个重要性质是所谓的单调性。众所周知，当不匹配包含在微积分中时，此属性的常见表示（使用替换）不成立。然而，当使用换位时，我们有：引理2.2给定STG，s，sJ是的节点，θ是转置，以下性质成立：(i) 如果s→α(ii) 如果sθ→αSJ，当sθ→αθSJθ.sJ，当re存在αJ， sJJ，则 s→αJSJJ，αJ θ<$ α和SJJθ <$s。证据 通过结构归纳法对相变进行研究。QαMM24T. Chen等人理论计算机科学电子笔记123（2005）19∈∈ N <$VVNXN VNV∀ ⟨ ⟩ ⟨⟩3π-µ -逻辑语法我们假设一个可数无限集合的名称变量，范围是x，y，z. ，这样=。我们假设一个可数无限的谓词变量集，由X，Y，Z，. . 每个谓词变量都被分配了一个元数n ω，写为X：n。公式的语法由BNF定义如下：α：：= τ|你呢？（十）|你呢？v|u！v|u！（x）φ：：=true|u = vA，B：：= φ|Λ（u）|欧元|A组B组|你好一|αΛ：：=X|（x）A|VX. Λ其中，u，v。句法分为两类：命题和谓词。在语义上，命题表示STG中的节点集合（即过程项），而谓词表示从名称集合到节点集合的函数对于命题，算子是相当标准的，因为它是从著名的Hennessy-Milner逻辑[8]改编而来的。一个谓词是一个谓词v ariableX，或一个牵引（x）A，或一个固定的po intνX。A. 当要生成一个抽象（x_n）A时，我们的符号表示s，要求x_n是不同名称变量的向量。则谓词Λ的arity被定义为：如 果 Λh是f∈X或νX，则f ∈ X的arity。Λ，或x 的 长度，如 果 Λh为f<$（x<$）A. 在牵引和应用中，我们都需要满足要求。 对于形式x的多个。A，u？（十）. A，U！（十）. A，（x<$）A和νX。Λ，x和X的区别出现是有约束力的，与命题A或谓词Λ的范围。它们以通常的方式引入了绑定和自由名称变量以及绑定和自由谓词变量公式A的自由名、自由名变量和自由谓词变量的集合分别记为fn（A）、f（A）和fpv（A）。没有自由名称变量的公式是名称封闭的。没有自由谓词变量的公式是谓词闭合的。如果公式既是名称封闭的又是谓词封闭的，则公式是封闭的我们以标准的方式在公式上定义了α -同余的关系αα，也就是说，作为识别公式的最小同余模绑定（名称和谓词）变量的重命名。我们将考虑总是模α-同余的公式。注意，对于公式，名称替换的概念被扩展到函数from to，即我们允许名称变量被名称替换。注意，为了方便起见，我们确定了m的β-等价，t是，（（x<$）A）（u<$）anddA[u<$/x<$]。一元运算符<$是负数。谓词变量的出现T. Chen等人理论计算机科学电子笔记123（2005）1925（Ⅲ）记为s∈A）。≡≡（Ⅲ）N →G±K（2）（Ⅲ）（2）（2）N → NN如果它在偶数个负运算符下，则为正X在公式A中出现的位置是正的，如果X在A中的每次出现都是正的。否则我们说X在A中负发生。定点谓词v X。Λ是良构的，如果fn（Λ）=f（Λ）=f且X在Λ中正出现。注意，我们要求预表示Λ没有名字，h_s_n（Λ（u_n））和f_v（Λ（u_v））完全由一个特定的上下文确定，这非常有利于语义的可靠性。一个公式是良构的，如果其中的每个定点子公式都是良构的。在续集中，我们只考虑格式良好的公式。请注意，像往常一样，在我们的π-μ逻辑系统中，我们可以定义一些标准的导出连接词。在本文中，我们选择了一种经济的方式来介绍我们的逻辑系统。语义给定STGG，根据具体的操作语义规则，可以得到一个具体的图G。公式的语义是通过给每个公式A分配G的一个节点集，即A，即G中满足由A表示的属性的所有节点来定义的。为了方便起见，我们用s表示nσ，阿纽什nσ，s[c/b]nσ[b <$→c]。由于使用了mula，所以可以包含自由名称变量和自由谓词变量，为了解释它们，我们需要名称赋值和谓词赋值。名称赋值ρ是替换的一个扩展版本，它是从有单位元到有单位元的全映射一个谓词赋值给元数为k的每个谓词变量X一个函数Nk→N k（G）。 像往常一样，关系可以逐点扩展为函数空间如下：对于每个k，两个函数f（k），g（k）：Nk → G（G），定义ef（k）±g（k）i <$f（n<$）<$g（n<$），其中nyn<$∈Nk。因此，功能空间n（）构成一个完备格w.r.t..公式的表示在图1中归纳地定义。如果A是名闭的，则Aρ;不依赖于ρ，记作A。此外，如果A是名闭的和谓词闭的，则Aρ;既不依赖于ρ也不依赖于，并且它将被写为A。 我们会写s |= A与一阶逻辑的情况一样，下面的引理将替换与赋值联系起来，这是常见的，并且将被隐式地使用。引理3.1下列性质成立：(i)A[b/x]ρ;n=Aρ[x <$→b];n.(ii)Λ [F/X]ρ;λ=Λρ;λ[X <$→λ（F）]。证据 通过对A和Λ的结构的相互归纳。Q对于任何公式A和B，其中A<$αB，<$A）ρ，<$=26T. Chen等人理论计算机科学电子笔记123（2005）19（）（）（）（Ⅲ）J<$X）=（X）ρ;J（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）J⟨⟩JJJτJJJJ（φ）ρ; =GIf ρ| = φ∅ o.w.ABρ;=Aρ; Bρ;<$A）ρ;=G\<$A）ρ;uvρ<$A）ρ;={s|埃斯蒂斯山s→s<$s ∈ <$A）ρ;ρ}你好！v<$A）ρ;={s|埃斯蒂斯山s→s<$s ∈ <$A）ρ;ρ}你呢？（x）A）ρ;={s|埃斯蒂斯山Suρ（b）→sεsJ[c/b]∈Aρ[x<$→c];对于所有的c∈ N}你好！（x）A）ρ;={s|埃斯蒂斯山 S你好vA ρ;={s|埃斯蒂斯山 S<$Λ（u））ρ;=<$Λ）ρ;（ρ（u））<$（x<$）A）ρ;<$=λy<$。A）ρ[x→y];Ku'ρ（b）→suρ（b）→sεsJ[c/b]∈Aρ[x<$→c];对于somec∈fn（s）<$fn（A）}εsJ[vρ/b]∈A）ρ;ε}X. Λ）ρ;ρ= H{F：N →C（G）|F± <$Λ）ρ;ρ[F/X]}Fig. 1.公式解释B ρ，对任何ρ和<$，这证明了我们确定α-等价公式的决定。同时，我们可以很容易地证明语义函数的单调性A，因为它需要在A中具有X个计数器。 我们，λ f。 Aρ，<$[X <$→f]是完备格（{f：Nk → <$（G）}，±）上的单调泛函. 通过Knaster-Tarski定理，我们可以得出结论，νX. Λ是fλf中的最大不动点。 Aρ，n[X <$→f]. 可以获得语义空间的声音。现在，我们对逻辑系统的模态选择做一些评论一般来说，有两种风格的语法的[14][15][16][17] [18][19][1我们遵循前者的风格，因为从我们的角度来看，它更清晰。然而，语义是显着不同的。首先，[14]缺乏一种用于绑定输出的模态，尽管syntaxa'（x）Aex是在逻辑系统中。不难看出，对于一个与直觉不太一致的人来说，他的语义与直觉并不太一致。其次，本文的输入模态与[ 14 ]中的a′（x）L相一致。我们不需要对其他两个“输入”模态进行相应的处理，因为它们可以在我们的JJT. Chen等人理论计算机科学电子笔记123（2005）1927def⟨⟩N →GN →G=N →G=如下所示：a（b）A defix。你是谁？xAa（b）E A defx. 你是谁？xA绑定的输出方式需要更多的注释。 请注意，我们对这种情态的语义与达姆的一致，尽管语法不同。为了使这个模态更清楚，我们参考了一下新的名称量化和Dam的语法。事实上阿吉拉！（x）A=ax.x←A我们认为熟悉的读者可以很容易地理解这一点。 我们建议读者参考[2][3]以了解详细信息。值得指出的是，正如我们在第1节中提到的，这样一个量化在给出解释时会带来困难，尽管它只是隐含在我们的逻辑中。文[2]中也考虑了类似的问题。作为一种补救措施，[2]引入了PSets（属性集）的概念。然而，这样的语义装置使得语义定义相当复杂。我们的解决方案是区分命题和谓词，从而解决递归和一阶量化之间可能的相互作用。我们的系统的优点在于，我们的逻辑语义更清晰，更简洁。更重要的是，它是更有利的模型检查的目的。此外，值得指出的是，我们不需要介绍一个！（b）类情态，由于从语义上看，选择具体的名称作为输出动作的内容是无关紧要的，因此，我们使用变量而不是名称。现在，我们开始建立一些关于逻辑公式性质的重要结果，这些结果对于模型检测算法是重要的。在文[2]中，我们利用转置作为一种有用的工具，给出了一些关于新名字性质的简明证明由于篇幅所限，本文省略了大部分详细的证明.我们建议读者阅读本文的完整版本以了解更多细节。下面的定义将转置的概念扩展到谓词。定义3.2设θ是一个跃迁。一个函数f：n （ ） 是θ-保持的，如果对任意n，（f（n））θ= f（nθ）.一个赋值是θ-保持的，如果对任意X，θ-保持。引理3.3给定一个转置θ和一个函数f：θ（），定义fθ：θ（）为fθ（n）=f（n）（f（nθ））θ，对任意n，则下列性质成立：(i) fθ是θ-保持的。(ii) 如果f ± g和g是θ-保持的，则f θ± g。28T. Chen等人理论计算机科学电子笔记123（2005）19（ii）<$Λ）是θ-保持的。ρ;ρ（Ⅲ）→⟨⟩S|JJ =a！（x）如果有新的名字c和s，使得s和→（Ⅲ）（i）s∈<$x. A）ρ;φi φs∈k∈fn（A）φ {c}<$A）ρ[x<$→k];φ.证据 通过换位和θ-保持的定义，证明是容易的。Q引理3.4假设θ是θ-保持的，则下列性质成立：(i) （<$A）ρ;θ =<$Aθ）ρ;θ。证据 通过对A和Λ的结构的相互归纳。Q根据语义学的x.A和a？（x）<$A，检查P是否∈ <$x. A需要用每个名字实例化x。然而，正如下面的引理所证明的，只考虑A的自由名加上一个新鲜名是足够的这种有限特征将在模型检查算法中得到利用。Lemma3. 5假设c∈/fn（s，A），则下列性质成立：(ii) s ∈ u？（十）（A）ρ;ρI sρ（u）（b）SJ和SJ[k/b] ∈A）ρ[x<$→k];对于k ∈ fn（A）<$fn（s）<${c}.A的语义定义！（x）A是以“存在主义”的风格陈述的a（b）[c/b]|=A[c/x]。我们给出了这样一个定义，它是从我们的观点出发的，它与我们对有界输出和约束算子直觉更吻合。然而，因为c在s或A中都不是自由的，所以c s的这种特殊选择不应被考虑。 因此， 任 何 具 有d∈fn（s，A）s的其他名称都应该同样有效。因此，语义学确实也可以被描述为引理3.6s∈A！（十）（A）ρ;ρi. re存在sJs.t。sa<$（b）sJ和sJ[c/b]∈Aρ[x <$→c];对任意yc∈/fn（s，A）都是n.4模型检测算法在本节中，我们致力于为我们的π-µ-逻辑提供一个模型检查算法。基于上一节的结果，现在最具挑战性的问题是处理定点运算符。对于命题μ-演算，许多研究者已经提供了很多解决这个问题的方法。我们选择所谓的局部模型检测算法，因为全局算法需要事先构造状态空间，这在我们的设置中是不可能这种算法的一个显著特征是用于跟踪展开定点公式的机制。有两个共同的，等价的，T. Chen等人理论计算机科学电子笔记123（2005）1929（Ⅲ）N→G<$）HK解决这个问题的方法：一种是引入固定点出现的常量，并使用全局推理规则来检测先前的解绕，另一种是将标记引入固定点公式，该公式准确地记住之前已经访问过的模型点。与[15]一样，我们采用后者的方法，并遵循框架，到Winskel [16]，有时也称为标记集方法。然而，与[15]不同，我们将其提升到谓词情况，并且在我们的算法中，标记集将包含相同的Vector和S T G的nde的对（n，s）。好吧，让我们T={（b∈1，s1）， . . ，（b<$n，sn）}，其中，n<$i（1≤i≤n）是这两个矩阵的一个或多个向量长度，sayk和f或i，j，i/=j，wehaveebibj。如果你不想让T，我们就λT表示函数Nk→λ（G），定义如下：（λT）（λb）=⎧⎨⎩i{si}if（ib，si）∈T如果O.W.现在，定点谓词νX。Λ可以推广到νX。[T]Λ，注意X必须与T具有相同的arity，并且T的用途在于记录模型的哪些点之前已经被访问过，因此只是一个簿记设备。n（νX. [T]Λ），fv （νX. [T]Λ）和fpv （νX.[T]Λ）与νX的相应定义相同。A.很明显，VX。Λ可以被覆盖为νX。[]Λ。v X的外延。[T]Λ是λ νX的简单扩张。Λ）ρ;ρ如下：X. [T]Λ）ρ;ρ=H{F：N→C（G）|F±<$Λ）ρ;<$[X<$→F]H λT}下面是一个技术引理，它是[16]中所谓的归约引理的推广，这是标记集方法的本质。引理4.1（归约引理）设L = Nk → N（G）是完备格，φ是单调泛函.则对于任何f∈ L，f± νg.φ（g）if ± φ（νg. （φ（g）Hf））证据 [16]中的证明的简单推广QSinceXocurspositi veinΛ，λ f. Λρ;<$[X <$→f]λT是k ∈（）上的单调泛函 ， 且 νX. [1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19]因此，使用引理4.1，可以很容易地证明下面的引理。Lemma4. 2若s∈/λT（λb），则ts∈<$VX。[T]Λ）ρ;τ（τb）i τs ∈ τΛ [νX. [T<${（b，s）}]Λ/X]）ρ;（b）30T. Chen等人理论计算机科学电子笔记123（2005）19¬¬∧∧d∈fn（mσ，A）<$new（fn（mσ，A）））=的）=的σ[d<$→b]<$fn（n）σ[c<$→d]<$fn（n）defcheck（mσ，φ）=Ev（φσ）;defcheck（mσ，A）=check（mσ，A）defcheck（mσ，A B）= check（mσ，A）check（mσ，B）;检查（mσ，Adef）=的b∈fn（mσ，A）检查（mσ，A[b/x]）check（mσ，A[new（f n（mσ，A））/x]）;检查（m，AdefEv（φσ）检验（n，A）;σ检查（m）=的你是说...（十）A类φ，τm›→ndefσEv（φσ<$[bσ=a]）σ）=∧φ，b（c）m›→n支票，A[d/x]）;检查（m你好！cAdefEv（φσ<$[a=bσ]<$[c=dσ]）检验（n，A）;检查（m你是说... bdefEv（φσ<$[a=cσ]）检验（n，A）;检查（m你好！（十）A类defEv（φσ<$[b=aσ]）σ）=1999年，φ，<$b（c）m›→nnσ[c<$→new（fn（mσ，A））]，A[new（fn（mσ，A））/x]）;check（mσ，（νX. [T]Λ）（λb））σφ，<$bdm›→nσφ，c（d）m›→nT. Chen等人理论计算机科学电子笔记123（2005）1931=真若（σb，mσ）∈Tcheck（mσ，（Λ [νX. [T<${（σb，mσ）}]Λ/X]）（σb）） o.W.图二. 局部模型检测算法现在，我们提出我们的算法如下。该算法输入STG用根n和代换σ和一个封闭公式A.像往常一样，我们σ32T. Chen等人理论计算机科学电子笔记123（2005）19将mσ表示为s。 如果s=mσ满足A，则算法返回true，否则，则返回false。该算法的伪代码如图2所示。回想一下，对于一组名称VfinN，函数new（V）返回的最少N \V中的名称。现在，我们致力于证明我们的算法的正确性。 建立T. Chen等人理论计算机科学电子笔记123（2005）1933算法的终止性，我们需要限制模型检查过程的名称，就像在[15]中绑定自由变量一样。首先，我们应该指出，根据转移过程的规则，对于STG而言，STG中的所有绑定名称是不同的。既然我们领养了公式的α-等价性，我们可以假设在公式也是不同的。现在，我们写NG代表名字的数量，34T. Chen等人理论计算机科学电子笔记123（2005）19GG（Ⅲ）⟨⟩⟨⟩（包括自由和绑定的名称）和NA的节点中包含的名称和名称变量的数量。请注意，公式的标记集中的名称不包括在内，因为它仅作为簿记。下面的引理很重要，通过它我们可以得出结论，假设每个项在每个标签集中只出现一次（就像我们的算法一样），标签集的大小是有界的，因为我们考虑的STG是有限的。引理4.3对于check的每个递归调用，调用者参数为（s，A），被调用者参数为（证据 通过对每个递归调用的实例分析，证明是常规的。Q我们现在用这个事实给公式一个有根据的排序 我们写A GAJi <$AJ不是定点公 式，A 是 A j 的真子 公式， 其 他 的 是 A 是 f∈ （ Λ [νX. [T<${b ，s}]Λ/X]）（vb），且AJ为（vX. [T]Λ）（λb）当re（εb，s）∈/T时，T仅是G的一个非零解. 我们要告诉你，传递闭包这个关系的+是一个良基序，每当G是没问题。G引理4.4如果G是有限的，则+是一个有根据的命令。证据 类似于[15]，命题4。Q定理4.5对于任何具有根r和封闭公式A的STG，以下性质成立：(i) check（r，A）终止;(ii) check（r，A）= true i <$r∈ A.证据（ 素描）(i) 将有理有据的归纳应用于G，终止是有保证的。(ii) 大多数情况下严格遵循公式的解释 φ，<$A和A的情形是：ba和a！uA是平凡的。A的情况的正确性由引理3.5（i）得出。A的情况下？（x）A遵循引理3.5（ii）。这是我的！（X）以下是引理3。六、 F或固定点（νX。[T]Λ）（λb），引理4.2适用。证据已经完成。Q5结论在本节中，我们总结了我们的工作，并讨论了相关的工作。本文研究了移动并发系统的模态逻辑及其模型检测算法.在本文中，我们使用符号转换图来建模T. Chen等人理论计算机科学电子笔记123（2005）1935并发系统π演算过程的一个广泛的类别，即有限控制过程，可以表示为有限符号转移图，这种转换相当简单，因此我们的模型具有很强的表达能力。本文介绍了一种新的π-μ-Logic，它是模态μ-演算的扩展，具有名字上的布尔表达式和名字输入输出的原语，是π-演算的模态逻辑我们的逻辑系统也可以看作是[14]中模态逻辑的推广。通过区分命题和谓词，给出了模态逻辑的简洁语义解释，从而解决了递归和一阶量化之间可能的相互作用.在上述工作的基础上，本文提出了该逻辑的局部模型检测算法。我们遵循著名的Winskel的标记集方法来处理定点算子。至于名称实例化的问题，我们的算法遵循的“上的-的-的”风格，并系统地采用示意图名称。证明了算法的正确性关于模型检查有大量的出版物，但只有少数几个涉及名称传递过程。本文最相关的工作可能是[4][6]，我们在引言中讨论了他的工作。也有一些关于值传递过程的工作，例如[15]扩展了[7]中的模态逻辑。这些论文的主要关注点是制定证明系统，用于导出断言过程是否满足公式的语句。针对这类模态逻辑的模型检测算法，目前还没有得到足够的重视。另一方面，[11]研究了CCS过程的模型检验问题，本文的一些思想受到了启发。 然而，与传值过程的工作相比，绑定输出的形式给语义解释和模型检测算法带来了困难，这是我们工作的主要挑战之一。我们还应该提到[2][3]，那里研究了关于约束输出模态的新名称量化。我们在第三节中把我们的工作和他们的工作作了详细的比较. 我们认为，我们的方法，至少，更有利于模型检测的目的。然而，一些有用的工具，如换位，来自[2]。有几个进一步研究的方向如何提高算法的效率，是一个有趣的问题。此外，我们正在研究如何生成信息诊断消息，这将是有用的，在调试系统时，由算法返回的答案是或许我们应该更深入地运用象征手法。引用[1] R.M.Amadio，M.Dam.关于π演算的模态类型理论。Proc. Formal Techniques in Real Timeand Fault Tolerant Systems 96，Uppsala.LNCS 1135，Springer，1996年。36T. Chen等人理论计算机科学电子笔记123（2005）19[2] 作者声明：by J.并发的空间逻辑（上）TACS[3] 作者声明：by J.并发的空间逻辑（第二部分）Proc. CONCUR[4] M.Dam. 模型检查移动进程。 信息和计算129：25-51，1996。[5] M.Dam.关于pi-演算过程等价的判定性。计算机科学183页215-228，1997年。[6] M.Dam. π-演算逻辑的证明系统。出现德奎罗斯（编辑），《逻辑与计算》，《逻辑与计算研究》，牛津大学出版社，2003年。[7] M.Hennessy，X. Liu.消息传递过程的模态逻辑。Acta Informatics，32：375- 393，1995.[8] 作者声明：John W.非确定性和并发性的代数律，ACM杂志，2003年，第32页。137-161，1985年。[9] 作者声明：Zhang. π-演算的强/弱互模拟等价性和观测相合性检验在ICALP[10] H.Lin. π演算中弱互模拟等价的完备推理系统[11] H.Lin.模型检查值传递过程。第八届亚太软件工程会议论文集。澳门：IEEE出版社，2001，3-10.[12] R.Milner. 通信与并发，Prentice Hall，1989年。[13] 题名其余部分：R.A Calculus of Mobile Process，Part I/II.信息与计算学报，100：1-77，1992年9月。[14] 题名其余部分：R.移动过程的模态逻辑。理论计算机科学，114：149-171，1993。[15] 作者声明：J.传值过程的局部模型检验。1997年第九届计算机软件理论方面国际会议论文集[16] G.Winskel.关于模态微演算的模型检验的注记。理论计算机科学83：157-167，1991年。