有限控制π演算中认知谓词CTL的模型检查

可在www.sciencedirect.com在线获取理论计算机科学电子笔记278（2011）229-243www.elsevier.com/locate/entcs一个认知谓词CTL有限控制π-过程迪米塔山口Guelev1保加利亚科学索菲亚Mads Dam2皇家理工学院计算机科学与通信学院瑞典斯德哥尔摩摘要我们研究了有限控制π演算过程对认知谓词CTL中的规范的模型检查。与分支时间设置（如CTL或模态μ演算）相比，即使对于LTL，一般问题也是不可判定的，本质上是因为进程可以将环境用作无界存储。为了避免这个问题的注意力被限制到封闭的进程，内部通信沿一组给定的已知信道是可观察的。这允许对在适当的内存受限环境中操作的过程进行建模。我们提出了一个具有完美回忆的认知谓词完全CTL，它在由这种有限控制π演算过程定义的计算树我们证明了模型检查的可判定性减少的有效性的可判定性在量化的完整的命题的CTL的。关键词：认知时态逻辑，pi演算，模型检测介绍π演算[12，16]作为分布式系统的计算模型吸引了很多兴趣。与大多数其他进程代数一样，微积分一般是图灵完备的.因此，大多数关于π-演算的有趣的决策问题是不可判定的。语法支持主要适用于其有限控制子集，其中并行组合的使用受到语法限制。时态逻辑的认知扩展被证明对表达分布式系统中智能体的进化知识的属性π演算1电子邮件：gelevdp@math.bas.bg2电子邮件：mfd@kth.se1571-0661 © 2011由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2011.10.018230D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229扩展了已建立的计算模型的认知TL的可能性，动态地创建新的通信渠道。这是有趣的，以审查如何这一特点可以容纳在认知逻辑框架。本文在有限控制π-演算过程的计算树上引入一个谓词认知CTL系统我们的认识算子符合既定的观点，即一个事实是已知的，如果它对于认识者发现与实际相同的所有计算都是真的认知TL指的是主体身份和“认知者”。π演算没有这些概念，但认识模态可以用其他方式解释π过程。科恩和达姆[4]从静态对等的角度解释了认知模态[1]，但他们的工作只涉及静态知识。Chadha等人[3]提出了一个基于迹等价形式的π-过程的单一认知者认知TL然而，目前还不清楚这是如何扩展到多个代理，以及为什么Q和Q是唯一考虑的时间运算符。在这里报告的实验中，我们采取了不同的方法：我们用他们的观察能力来识别认知者，这是由一组最初的“已知”或挖掘的通道决定的这个集合通过添加通道名称来增长，这些通道名称沿着已经点击的通道进行通信。我们写K×1，...，对于最初点击x 1的知道者，.，x n知道，然而，直接将纯分支时间情况下的已知可判定性结果[5]扩展到线性时间时态逻辑LTL，更不用说CTL逻辑的认知扩展是不可能的。即使有有限控制的限制，与外部环境的交换也使得LTL属性的模型检查无法解决，因为有可能限制环境表现为给定图灵机磁带的存储 一个证明在论文的最后画了一个草图。不可判定性延续到CTL的（认知扩展）。为了避免这种复杂性，我们通过将注意力转移到封闭系统来约束环境，并假设认知者只观察到沿着一组敲击名称的内部通信，沿着这些名称的通信是可观察的。其结果是，只有当过程被放置在一个固定的有限封闭环境中时，过程才能被预测。我们证明了我们的系统的模型检测的可判定性。我们将给定π-进程的执行树编码为有限Kripke框架，并将该树上任何给定谓词认知CTL公式的模型检查减少到树上的量化命题CTL公式（QCTL公式）的翻译的可满足性，这是已知的可判定的[8，9]。1关于π-Calculus有限控制π-项语法可以由BNF给出P：：= 0 |α.P|（νy）P|P + P|如果x = y则P否则P|p（y，.，y）Q：：= 0 |P|Q|Q|（νx）QD.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229231C CC kk+1C12α这里P、Q是使用（通道）名称x、y进行通信的过程术语一个通信动作α要么是一个名为y的输入沿着一个名为x的通道，记作x（y），要么是y沿着x的输出，记作xy，或者是中性的、不可解释的动作τ。名称可以通过操作符（νy）进行局部作用域，这会阻止沿着y的通信（但允许y作为参数传递 ， 导 致 所 谓 的 y 的 作 用 域 挤 出 ， 如 下 所 述 其 他 运 算 符 有 actionprefixing、choice（+）、conditionals和parallel composition。一个过程是一个形式为Q的项和一组形式为p（x1，...，xn）= P，对于Q中的递归调用和定义本身的右侧。下面我们省略了单个过程项P和并行组合物Q之间的区别，并使用P来在两者上范围。π-项P中所有名字的集合记为n（P）。自由名和绑定名的集合分别写为f n（P）和bn（P），绑定器分别为（νx）和绑定x的输入前缀x（y）。y. Binders引入了一个关于项的结构同余关系，包括α-转换，下面将详细介绍我们只考虑处决P0−τ→1P1−τ→2···−τ→Pk−τ→···（1）其完全由无声步骤组成，以防止环境相互作用，如在引言中所解释的。转换被注释的内部通信行为，这可能是由知者观察到的集Ck每个Pk都有形式（vx1）.（vxm）P（ 2）其中P没有ν的出现。这种形式可以使用结构一致性来实现。注释Ck由以c（x）形式书写的通信行为组成。注释转换由以下公理和规则导出，这是所谓的π演算早期语义【14】：τ.P−τ→x（z）P x（y）.P−→XY[z/y]P xy.P−→PP−α→CPJy/∈n（α）y/∈n（C）（νy）P−α→C（νy）PJP1−α→C PJP−α→CPJy∈n（C）（νy）P−α→CPJP2−α→CPJP−α→CPJP+Q−α→CPJx/=y1ifx=xthenP1elseP2−α→CPJ2如果x=y则P1elseP2−α→CPJQ1−→C QJ1bn（α）<$fn（Q1）=<$XYQ1−→Q QJ1x（y）Q2−→QQJ2年q1| Q 2−α→CQJ|Q2年q1|Q2−τ→QJ|QJ1α{x（y）}1 2（C一致）P−→CQ P<$PJQ<$QJPJ−α→CQJ+和平行合成的对称规则|可以用结构一致性推导出来。 注释可以是单例或单例。 与恒等式A合在一起|（νx）B（νx）（A|B），xf∈fv（A），和p（x1，.，x n）P，给定p（x1，...，xn）= P，同余规则允许避免使用绑定输∅232D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229出动作x（y），并且aD.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229233τ不0def关于递归调用的专用规则。 可以证明P−τ→{x（y）}Q根据上述语义i <$P−→（νx）（νy）Q根据早期[14]的语义，其中（νx）或（νy）中的一个或两个可能不存在。2有限控制π-过程上的认知谓词完全CTL使用α-转换很容易编写像（1）这样的执行，以这种方式，名称在下面的意义上永远不会重用定义2.1在执行E中，名称x的范围（生命期）写为def（1）是集合LE（x）={kω：x∈n（Pk）n（Ck）}。 E是标准的，如果对于每个x，LE（x）是一个实数，或一个有限或无限的整数。EPCTL的一个模型是Kripke框架（P0），其路径对应于从某个给定的π项P0开始的标准执行。确定一个可数无限集合D，包含T（P0）中的所有名字。定义2.2T（P0）=W，R其中W由以下形式的所有对组成：其中P是在从P 0开始的某个执行中出现的形式为（2）的过程项，并且C∈ {n}<${c（cJ）：c，cJ∈D}。PJ，CJPJ−τ→PJJ，或PJ=PJJ，CJJ=且Pj死锁或终止。C终止和死锁的P的条件P，C RP，P排除了T中的有限极大路。给定P0，存在无ν过程项的有限集合P，使得以下条件成立：令{y1，.，y N}=P∈Pn（P），设A为集合{n}{{y i（y j）}：i，j = 1，.，使用y1，...，y N. 然后所有带注释的无声跃迁Pk−τ→P可以写成Ck+1 执行（1）中的Pk+1σ（νu1）. （νu r）QJ−τ→σBσ（νv1）. （v v s）QJJ（3）其中QJ，QJJ∈P， u1，.，u r，v1，. v s∈{y1，.， yN}，B∈A，σ=[[n1/y1，...， n N/y N]是y1，...， y N，由两两不 同 的def姓名n1，.， n N，且σB ={nj1（nj2）：yj1（yj2）∈ B，j1，j2= 1，.，N}个。我们写σ使用[. 而不是[。]以指示它不影响y1，...， 也是。由于n1，…，n N必须是不同的，我们使用[. ]在语义上是正确的。特别地，（3）是可导跃迁i ∈（νu1）.（νu r）QJ−τ→B（νv1）. （νvs）QJJ 是.我们使用P作为T=T（P0）的谓词符号的词汇表。每个P∈P都被用作一个|fn（P）|-ary谓词符号。(Note这里P的范围是形式（2）中项的无νP的唯一绑定名称可以是作用域中的ydefx（y））。给定{z1，...， z|fn（P）|}= fn（P）n {y1，.， y N}，我们固定排序z1，.，z|fn（P）|，并且，对于任何n1，...，n|fn（P）| ∈D，我们定义PT（n1，...，n|fn（P）|）到234D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229我·· ·−→A我1≤ ∼∼2我保持<$Q，A<$∈W i <$Q = [n1/z1，...，n|fn（P）|/z|fn（P）|] P.同样，我们引入一个二元谓词符号C的最新的通信行为，和一个时间命题T的沉默的转变。这个词汇表可能不方便直接使用，但是通过存在量化和析取，人们可以很容易地定义谓词，例如，Z（n1，n2），因为存在一个名称y，使得当前过程项的形式为. |......你好。|.. . .对于写为（1）的带注释的执行E，在步骤k处由认知者a分接的通道的集合CE（a，k）定义如下。CE（a，0）被假定为预定义的，并且对所有E都是相同的。给定CE（a，k），我们将defCE（a，k+1）=CE（a，k）<${c：c（cJ）∈Ck+1，c∈ C E（a，k）}.（四）换句话说，一旦a观察到信道名cJ的通信，则cJ上的通信也变得对a可观察给定CE（a，k），k ω，再执行两Fi=Q0−τ→1τQk−τ→k+1i···，i=1， 2，我们定义F1a，k，EF2为等价关系（nj≤k）（nc∈CE（a，j））（ncJ∈D）（c（cJ）∈Aj参与（cJ）∈Aj）.换句话说，F1<$a，k，EF2i <$F1和F2在E中的a在所有步骤j≤k处观察到的信道上具有相同的通信。由于F1≠a，k，F1F2需要CF2（a，j）=CF1（a，j）对于j k，因此F1a，k，F1F2和F1a，k，F2F2是等价的，并且def安哥拉a，k=λF1F2.F1≠a，k，F1F2是一个等价关系. F1和F2不可分辨直到步骤ki <$F1<$a，kF2。 我们通过下面的公式来定义我们的认识模态：EPCTL的语法是：：= |P（x，.， x）的|ϕ ⇒ ϕ |x|g|Ⓧϕ|（S）|（U）|∃ϕ |Kx，.，X轴其中x的出现表示单个变量。T中标准执行的对应物是标准R-路径.定义2.3无穷序列ρ = P0，C0，.，P k，C k ∈ W ω（5）是一个标准的R-路径，如果P0是用来定义T的过程项=T（P0），对所有kω，C0= k，Ck<$R<$Pk+1，Ck+1<$R及相应的执行(1) 是标准的。给定R-路径ρ 1和ρ 2以及通道c1，.，cm∈D，我们记为一一JK我D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229235ρ1<$c1 ， . ， cm ， kp2，如果E1≠a ， kE2用于对应的执行E1和E2，并且a使得{c1，.， cm}= CE1（a，0）= CE2（a，0）.定义2.4给定一个标准R-路径（5），单个变量的估值v236D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229可表示为D，k< ω，并可表示为公式，T，v，ρ，k|=由以下条款定义T，v，ρ，k|=T，v，ρ，k| = P（x1，...，X|fn（P）|）i ∈ P k是[v（x1）/z1，.，v（x|fn（P）|）/z|fn（P）|] PT，v，ρ，k| = C（x1，x2） i <$C k={v（x1）（v（x2））} T，v，ρ，k |= Ti C k=T，v，ρ，k| =i T，v，ρ，k之一|=，或T，v，ρ，k|=T，v，ρ，k |=<$x <$i <$T，v [x <$→d]，ρ，k|对于某个d∈ D，T，v，ρ，k |= g<$i <$k> 0且T，v，ρ，k − 1 |=T，v，ρ，k|T，v，ρ，k +1 |=T，v，ρ，k |=（<$S<$）i <$存在一个n≤k s. t。 T，v，ρ，k−n|=和T，v，ρ，k−j|对于j = 0，...，n− 1T，v，ρ，k |=（<$U<$）i <$存在一个n <ω s. t。 T，v，ρ，k + n |=和T，v，ρ，k + j|对于j = 0，...，n− 1T，v，ρ，k |=<$$>i <$存在标准R-路ρJS.T. pj [0.. k]= ρ [0.. k]和T，v，ρJ，k |=T，v，ρ，k |= Kx1，...，xm i T，v，ρJ，k |=所有标准品均为0R-路ρJs.t. ρv（x1），.，v（xm），k ρJ这里ρ [0.. k]表示长度为k +1的ρ的有限前缀。正如所预料的那样，FV（Kx1，.，xm）= FV（）{x1，.，x m}。我们使用T、<$、、和惠作为常用的缩写;I、−Q、、Q、Q、（W）和（V）分别缩写为T、（TS ）、<$−Q<$、（TU）、<$Q<$、（U）、（U）和（S）。例2.5设P 0= p（c）|q（c）其中p（x）= xx.p（x）+（νy）xy.p（y），q（x）= x（y）. 如果x = y则0，否则q（y）。一个知道谁可以最初点击c是在一个位置，以检测右操作数的终止|在这个过程中，一旦一个被窃听的频道的 名 字 变 成 沿 着 同 一 个 频 道 传 输 ：T（P 0），P 0，v，0 |=<$x<$w（C（x，w）<$$>Q（<$z p（z）|0Kx（zp（z）|0）），D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229237其中原子式p（z）|0加下划线以提高可读性。为了实现这一点，知者必须沿着新的渠道进行沟通。238D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229σ1BσkBkσBk+1k+10τdef1N ），初始状态w0=在每一步。(Each这些通道中的一个被使用一次来宣布其后继者的名称，然后3从EPCTL无穷控制π-过程到QCTL无穷控制在树上再次考虑具有形式（2）的过程项的标准注释执行（1）和这些执行中的转换的表示（3）的表示（3）如果我们允许n1，...，n N也是辅助符号<$/∈D，只要n j=<$，则y j/∈n（QJ）<$n（QJ）。 为了便于介绍，在下文中，我们使用（3），其中hn1， . ，nN在D{\displaystyleD}上的范围，并将σ=[.. . ，n/yj， . . . ]而不是yj/∈ dom σ。我们固定P0，P，D，{y1，.，yN}=Q∈Pn（Q）和A用于该部分的其余部分。给定这些，形式（1）的带注释的执行E可以写为：σ0Q0−τ→1···−τ→σk Qk−τ→···（6）其中Qk∈P，Bk+1∈A和σk是如上所述的替换，满足σk+1Qk=σk Qk，以及附加条件ranσk\ {n} =n（σk Qk）<$n（σk Bk）=n（Pk）<$n（Ck），对于所有k。则显然LE（n）={k ω：n∈ranσk}。在续集中我们还要求，如果σk1（yi1）=σk2（yi2）满足E的形式（6），则i1=i2，对所有的k1，k2∈LE（σk1（yi1）），即一个名字n应该占据同一个槽y在E.直到Di（6）的置换由序列Qk，kω和B k，1 ≤ k <ω，并且对于每个j = 1，.，N，步骤k，σ k−1（y j）/= σ k（y j）。（七）为了认识到这一点，观察到在标准执行中（7）等价于k=min L E（σ k（y j））和到k−1 = maxLE（σk−1（yj）），条件是σk（yj）和σk−1（yj）/=。因此，直到名称的排列，从给定的P开始的标准执行可以通过以下方式来描述：def有限Kripke框架F=<$W，R，w0<$W=P×A×P（{y，...，y}定义P0，n，n（P0）n和转移关系Rsuch证明<$PJ，BJ，YJ<$R<$PJJ，BJJ，YJJ <$i <$YJJ=（n（PJJ）<$n（BJJ））Δ（n（PJ）<$n（BJ）），PJ−→BPj是一个可导跃迁，或PJ=PJ J，BJ=B，PJdef def要么是死锁，要么是被终止。 其中n（j）=n，n（{yj1（yj2）}）={yj1，yj2}，并且D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229239AΔB=A\B<$B\A，如预期。其中，Y∈P，B，Y∈W的分量Y表示y1，.，yN，它们分别在传入转换时消失或（重新）出现。我们使用F对从P0开始的所有标准执行树进行模型检查，以获得EPCTL的属性。我们使用一个描述F的路集的命题LTL公式E，而不是直接解释F上的EPCTL公式。本240D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229=- -- -最后引入一个有限词汇表L ={q1，.，q K}和赋值V：W→ P（L）。假设L的变量值与F的态结构之间没有联系我们仅要求V满足V（wJ）/=V（wJJ），无论何时wJwJJ，可实现i <$K ≥ log 2 |W|. 给定一个状态w∈W，令w^defq∈V（w）qiq∈L\V（w）<$q. 我们把Ew0w∈WQ（w）w∈R（w）w^J）。（八）现在，M中的任意QCTL公式的有效性等价于|= QCTL你好。 Bychj，总线yj，k，j，k=1， . ， N，和τ，我们不需要q 1，.的n个组合，q K，在等价情况下，由以下条件确定，其中M =W，R，w0，V，w =Q，B，Y：M，w|=c hjiyj∈YM，w|=bus yji <$yj∈n（Q）<$n（B）M，w|=τi τB=τM，w|=com mj1，j2i={yj1（yj2）}chj的本意是指yj的职业被c挂起在进入转换时，即， 或者k= 0，或者在rep中为σk−1（yj）σk（yj表示（6）执行;busyj表示yj当前持有一个名称，τ表示进入跃迁w为τ，τj1，j2表示进入跃迁为σ k（yj1）（σ k（yj2））.给定P∈P和一个指数序列j1，.，J|fn（P）|∈{1，.，N}，Pj1，...，J|fn（P）|表示q1，...，QK使得M，Q，B，Y|=Pj1，. J|f n（P）|i ∈Q是[yj1/z1， . ，yj|f n（P）|/z|f n（P）|其中z1， . ，z|f n（P）|“先有先有，先有后有，先有后有。接下来，我们描述一个翻译t（. 在树Kripke模型上，将EPCTL转化为QCTL树模型允许约束命题变量的值沿着路径不受限制地变化，而在非树模型中，沿着路径的状态的重复出现限制了量化变量在相应位置的值也是相同的。通过滥用符号，我们也将上述有限Kripke模型M分解为树模型的结果写成M=W，R，w0，VQCTL通过形式为q的公式扩展命题CTL。 M，ρ，k|存在VJ：W→ P（L）使得VJ（p）= V（p） p/= q且W，R，w0，VJ，p，k| = 0。EPCTL语句的QCTL翻译t（t）是一个可满足|其中E与（8）中的一样，i对于从固定的P 0开始的所有执行都是真的。如上所述，E允许在E中的名字的出现被确定为D上的排列。既然我们假设“”是一个句子，这就足够了。为了处理EPCTL中名字的量化，我们增加了对可能的执行E的描述，E可以从E中导出，并描述了出现在E中的名字与EPCTL中的（绑定）变量值之间的恒等式。在不失一般性的情况下，我们假设，没有一个个体变量的约束下，一次以上的出现的。 设x1，...， x M是所有的个体D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229241−Q（Q）∧∧jJl/=l的变量。为了描述v（x l）在相关v的执行E中的出现，我们采用E的形式（6）并引入命题变量p j，l，j = 1，.，N. 步骤k 处 的 p j，l的 预 期 含 义 是v（x l）= σ k（y j）。因为它在下文中变得清楚，这使得能够将P（xl1，...，x lm），j1，.，JMPj1，. jmpj1，l1. p jm，lm.形式的公式的翻译包括形式的公式第 一 ， 我... 其中，Vl约束 pj ， l以标记执行E中v（xl）的某个可能范围 LE（v（xl））=LE（σk（yj）），所述执行E对应于T中的路径和对应的QCTL模型M中的路径。沿着给定的路径，pj，l在任何地方都不满足的情况对应于名称v（xl）在E中任何地方都不出现。让Fj，lpj，lbus yjpj，lpj，l.Fj，l意味着xl在时间k处的值为σk（yj），并且j是唯一具有此属性，并且没有其他单个变量在时间k处计算为σk（yj）。包含后一个条件是为了简化使用=构建的原子公式的处理为了表示xl不等于任何名称σk（yj），我们使用公式GlNj=1普杰湖使用F j，l和G l，我们写Hj，l（GlWchj<$Fj，l（Fj，lchjWchj<$QGl））。在第0步满足fHj，l意味着要么LE（v（xl））=k，要么存在ksuch使得σk（yj）/=k，对于某个k和v（xl） =σk<$（yj），要么kJ∈LE（v（xl））=LE（σk（yj））. 现在我们可以把VlN我j=1H j，l）。翻译的条款除了认知公式，如下：t（）t（xl1=xl2）如果l1/=l2，t（xl=xl）Tt（P（xl1，...，xlm））j1，，jm.Pj1，.jmMi=1pji，liit（C（xl1，xl2））（nj1，j2pj1，l1 pj2，l2）j1，j2t（T）τt（X<$）Xt（<$），对于X∈ {<$，g，<$}t（（<$X<$））（t（<$）Xt（<$））对于X∈ {U，S，<$}t（xl）z∈FV（xl）t（[z/x l]）p1，l. N，l（Vlt（V））为了便于翻译形式为xl1=xl2的公式，t（xl）的子句242D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229HJ通过分别处理v（xl）是这些值之一的情况，提供了从xl形式为Kx1，...，xm要求我们为任意执行E和已知者a编写C E（a，k），k< ω的描述，使得C E（a，0）={v（x1），.，v（xm）}在我们的命题时态语言中。我们通过引入命题变量o j，j = 1，.，N.就像变量pj，l，oj在EPCTL的翻译中只会出现绑定的情况由于所考虑的执行E是以形式（6）书写的，因此在K a的翻译中o j的预期含义是... 在步骤k，σk（yj）∈CE（a，k）。下我们构造一个LTL公式来表示o j，j = 1，...，N，根据C E（a，k），k< ω的定义性质，相对于执行E的命题描述所采用的方式，表现。考虑一个单独的变量xl，使得v（xl）∈CE（a，0），令k ω。然后满足于Ij，lFj，l（ojSchjoj）oj（ojWchj）在步骤k处意味着如果k∈LE（v（xl））并且v（xl）=σk（yj），则A在其整个范围LE（σk（yj））=LE（v（xl））上抽头信道σk（y j）上的通信我们把NI LQ I j，I对于L{1，. M}。l∈L在步骤0处满足IL意味着A在由xl，l∈L表示的信道上的通信遍及它们的范围进行抽头。为了用CE（a，k）来表示CE（a，k+ 1）的定义（4），我们使用以下公式：CQ（o h惠（<$chho h）o jj，h）.（九）在步骤0处满足C意味着在任意步骤k处在观察到的信道σk（yj）上传送信道名称σk（y h）使得从步骤k+ 1开始在σk（yh）上的通信是可观察的，并且对于σk（yh）直到实际上达到步骤KJ> k，使得σk∈（yh）σk（yh），即由YCHH表示。 L e toOLbeformu l a−Q（I ILC）. OL表示Oj持有一个t对于所有kω和j∈L，步骤ki <$ σk（yj）∈CE（a，k）。表示Kx1，...，xm还需要参考执行Ej，其表现出与实际执行E相同的可观察动作序列。为此我们引入n个额外系数LJ={q1，J， . ，qKJ}的vocabularyL，模型M，我们用公式E描述了它的路径。我们把xJ写成b〇卷积合并[qi， J/qi：i=1， .. . ，K]x，x=tau，bus yj，com mj1，j2，chj。 类似地，我们假设附加集合pJj，l，oJj，j=1，.，N，l=1，...，M，以描述Ej中的各个变量和通道观测器vability的值的范围，以及W i t e I LJ、CJ等。 对于IL、C等的变体， 是用启动词汇写的D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229243.Σ⎞.H−N N⎛<$ej，hchjVchjΣ设替换项在记EJ时以形式（6）b e σKJ，k<ω表示。根据我们的编码，在E和EJ中观察到相同的动作意味着，如果oj和j，h，在某个步骤k保持不变，则对于somejJ，hj，证明了σk（yj）=σKJ（yj）和σk（yh）=σKJ（yh）. 为了表达后一种想法，我们引入原子比例ej，jn，j，jJ=1， . ， N. 在步骤k，ej，j的隐含意义是σk（yj）=σkJ（yj）/=σ k，k∈LE（n）<$LE（n），其中en=σk（yj）=σkJ（yj）。ej，j，j，jJ=1， . ， N，一条长的路径是正确描述的可能在一对执行E中的某个名称为n的元素LE（n）和LE_n（n）的集合中，和EJ，i，它具有由以下LTL公式ej，jbusyjbusyJ<$eh，jej，hh/=j⎜h/=jchjeh，jchjWchJj∨⎟ej，jej，jchjchjW公司简介H<$ej，hchjWchj- 是的hej，jej，jchjV齐泽 格.H中国日报<$eh，jchjVchJjΣ∨⎟⎠在第k步，第一个mula声明σk（yj）=σkJ（yj）/=σ k j可以对至多一对j，jJ成立。第二个和第三个定理表明，在第一步，σk（yj）=σkJ（yj）=nk表示对所有kJ∈LE（n）<$LE <$（n），σ k<$（yj）=σkj<$（yj <$），对所有h，σk<$（yj）σkJ<$（yh且kJ∈LE（n）\LE <$（n），对所有h和k j ∈ L E <$（n）\ L E（n），σkJ<$（yj<$）/=σk<$（yh）. 让j，j是这些公式的合取。We表示对于公式Q（IQj，jjj）j，j由N.利用变量ej，j_we可以用公式表示E和EJ具有相同的有效oj（ej，hoJh），oJ（ek，joh）（10）H Hej，j（pj，l惠pJj，l）（11）ojj，h（ej，jeh，hj，h）（12）j ，hoJjj，h（ej，jeh，hj，h）.（十三）j，h对于参考步长k，公式（10）规定CE（a，k） =CE（a，k）。公式（11）指出，由pj，l和pJj，l给出的单个变量的估值的说明与E和EJ中的恒等式一致，如用ej，j. 公式（12）和（13）指出，这两次处决是完全相同的。 W e表示（10）-（13）bySj，j，h，h的合取。We表示j，j，h，h⎟⎠244D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229Sj，j，h，hbyS. 在步骤k满足S意味着thatEa，kEJD.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229245⎝VOn{1，.，m}{1，.，MNS假设执行E和EJ对应于满意路径，则提供了总线yj，chj，τ，nj1，j2，总线yJj，chj，nj，τ和COMj，jj，j，τ正确1 2描述E和EJ，分别为y，pj，l，pJj，l和ej，j ，正确描述了E和EJ中涉及的名称与各个变量x l的值之间的一致性，最后，o j和oJ j正确描述了通道的可观测性。这个条件用连词来N <$E <$xn∈FV（n）Vn=0{1，.，m}EJxn∈FV（n）J J{1，.，M{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080}用i和j写的下标以及作为上面的主符号的l的范围超过{1，.，N}和{1，...，M}，分别。现在我们准备为Kx1，...，xm xm。(The最初可观察的通道被选择为前m个单独变量x1，...，x m为简单起见。）Kx1，.，xm转换为Jiangsu1J.. . 1JjpJ1，1.. . Mr.j.. p JN，1. . N，M⎛⎜N∧S∧EJ∧xn∈FV（n）Vnj一号机 . oN. oJN一，一.. . . 第一，N.. . N，1.. . N，N{1，.，m}OJt（t（Kx1，. xm= 0）提供了新的V_a_riable集合，. ，qKJ到使能EJ，pJj<$，l<$的描述 为了描述单个变量的值与在EJ，oj和oJ中所表示的名称之间的一致性，以分别标记E和EJ中的通道的观测值，以及一组变量ej，j，表示在它们的各种范围内在E和EJ这些变量的条件实际上迫使它们的真值给出了E j的一致性说明，各个变量引用E j中的名称的方式，两个执行中通道的可观察性，E和E j中出现的名称之间的恒等式，以及对于最初可以观察通道v（x1）的认知者a，.， v（x m）表示为在公式的矩阵中，EJ的左边，xn∈FV（n）VnJ，O{1，. m}，0J}，，和，分别。 总的来说，翻译说，如果一个不能从实际执行E中区分出一些EJ，那么E j的编码也满足t（k），这是满足Kx1的定义条件，...，xm x m。 t（Kx1，.，.）的自由命题变量xm=1，...，q K，并且p j，l，j =l，.，N，xl∈ FV（n），它描述了实际执行E以及E中出现的名称与n的（自由）变量值之间的恒等式，只要它们的真值分别满足E和相关的Vl。246D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229我们翻译的正确性可以用公式表示如下：定理3.1给定一个π-过程P0和一个EPCTL谓词语句T，T（P0），v，|= i |= QCTLE t（）。D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229247.Σ|证明可以通过下面对用于定义t（）的各个子句的公式的含义的详细解释来获得。）。4模型检验与外部通信的不可解性模型检查对于具有外部通信的有限控制π-过程是不可递归的，即使对于EPCTL的LTL子集也是如此，没有认识模态。为了证明这一点，我们定义了一类行为，其中环境e通过LTL公式充当无界存储。设I和O是二进制谓词符号，它们分别表示来自e的输入和到e的输出，就像关于内部通信的谓词符号C一样。我们打算声明，每当e沿着专用信道cons连续接收到两个名称x和y时，它就约束e以这种方式表现的公式可以写成如下。式沉默O（c，x）.声明最新的行动不是与e通信。让Qs（silenceU）和−Qs（silenceS）;R silen ce−Qsx I（reply，x）.R表示，与e的最新通信（如果有的话）是答复。然后时间复杂度：O（x）{\displaystyleO（x）{\displaystyle O（x）}zQs（I（reply，z）声明e在被要求检索先前注册为z的对x，y的第一个成员时必须返回x。可以写出类似的公式来表示检索y和注册对。 我们让读者意识到，假设以这种方式运行，可以构造有限控制过程PM来模拟任何给定图灵机M的工作，其中M的可以用上面的方式由e存储。这使得图灵机M的非停机问题归结为形式PM的过程的模型检验问题，该问题针对描述e作为存储器的工作的公式和陈述M的非终止性的公式的结合。同样的计划可以用来表明，模型检查有限控制过程的问题，它与有限内存环境通信以预测LTL属性，也就是说，是否存在有限控制E，使得给定P的PE的运行具有写在我们的EPCTL的LTL子集中的给定属性的问题，是递归可判定的，但仍然不可判定，只要E248D.P. Guelev，M.Dam/Electronic Notes in Theoretical Computer Science 278（2011）229是不受限制的这可以通过选择P在模拟图灵机M的过程P M上进行范围选择来实现，并且所讨论的属性为M终止，并且E以上述方式表现为存储，直到M终止。通过将M限制为确定性，P M|E可以被选择为只运行一次。对于终止M，P M的唯一运行|对于任何大到足以在模拟M的整个终止运行中充当存储器的E，E将满足上述性质。总结发言我们已经研究了有限控制π演算过程对公式的模型检查，在具有完美回忆的谓词CTL由于模型检查对于开放π演算过程甚至对于LTL都是不可判定的，因此我们转而解决封闭过程术语并通过一组独特的通道挖掘内部通信。这限制了进程的存储容量，从而使模型检查具有可判定性。π演算的模型检查已经被几位作者考虑过，但到目前为止只在分支时间设置中。 Dam [5]获得了第一个可判定性结果，模态μ-演算的谓词扩展。这个结果在[7，17]中得到了改进。后者的工作已被改编为随机π演算[13]。最近π演算及其方言在安全协议验证中的应用主要呼吁Dolev-Yao类型的知识提取。 一个例外是[3]，其中建议在π演算的上下文中使用认识推理。[11]中提出了模