RPPS系统的可达性分析方法基于树自动机技术

网址：http://www.elsevier.nl/locate/entcs/volume52.html20页RPPS系统可达性分析的自动机理论方法A. Labroue1和Ph.Schnoebelen2供应商认证，ENS de Cachan CNRSUMR 8643，61 av.Pdt. Wilson，F-94235 Cachan Cedex，France摘要我们展示了如何树自动机技术提出的Lugiez和Schnoebelen适用于RPPS系统的可达性分析使用这些技术要求我们表达的状态，RPPS系统在一个定制的过程重写系统，可达性是一个关系，可识别的尼特树自动机。关键词：纯态系统验证，进程代数，可达性分析，树自动机，模型检验。1引言本文研究递归并行程序方案（RPPS）系统的验证问题。RPPS系统是在[13，15]中引入的一个抽象模型，它用递归协程来模拟程序设计语言的控制流。如图所示，[9，10]中，这种模型的可达性分析在具有并行构造的编程语言的静态分析中具有重要的应用虽然RPPS系统可以被看作是某种带有嵌套标记的Petri网（在[13，15]中采用的观点），但我们认为值得将它们看作是一个处于初始状态的进程代数（或进程重写系统）。这种方法是非常活跃的（见[4]最近的成就调查），部分原因是它解决了广泛的验证问题（互模拟检查，时态逻辑模型检查等），也部分是因为存在几个有趣的进程代数（具有非常不同的表达能力），这些进程代数是通过对所允许的重写规则的简单语法限制而获得的[20，18]。1 电邮地址：labroue@lsv.ens-cachan.fr2 电子邮件地址：phs@lsv.ens-cachan.frc2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2树自动机最近[17]显示了PA进程代数3的可达性问题可以通过树自动机技术简单而优雅地解决。除了使用树自动机，该方法严重依赖于一个重要的想法：不应该考虑任何通常的结构同余模的过程项。这些一致性使过程符号更轻，并使它们更接近预期的语义，但它们隐藏了规律性，并不真正与树自动机方法兼容。PA的树自动机方法在[16]中得到了进一步的发展，其中表明PA过程之间的可达关系是有效可识别的关系，这给出了PA上的一阶转移逻辑的可判定性我们的贡献在本文中，我们调查是否Lugiez Schnoebelen方法PA可以工作的RPPS系统。本文主要有三个结果。首先，我们设计RPA，一个过程重写系统，编码RPPS系统在一个精心选择的方式。然后，我们证明RPA条款之间的可达性是一个可识别的关系：我们使用交替树自动机更直接的证明。最后，我们展示了如何RPPS标记之间的可达性可以减少到RPA条款之间的可达性问题，结束了一个直接的自动机理论算法。 作为 的推论，我们得到了NP-完全性的证明RPPS标记之间的可达性。这项工作中的困难来自于这样一个事实，即在过程代数符号中对RPPS标记进行编码的自然方式使得很难通过SOS（结构操作语义学，见[1]）规则来定义相应的转换，而不会丢失我们所针对的可识别性定理。特别是，我们看不到使用PA进程代数来完成这项任务的方法相关作品先前关于RPPS的可判定性结果[13，15]依赖于更多的特设表格方法或RPPS的良好结构[11]。这些结果弱于我们在第7节中给出的结果。最近，在[3]中，使用可识别的配置集进行符号模型检验被称为“正则模型检验“。这种方法更弱（但更实用），因为它不需要一组状态的迭代后继者或前导者形成有效可计算的可识别语言：只处理直接前导者或后继者（有时，可以处理循环的传递闭包存在其他几个系统，其可达性关系是3一个允许递归定义的片段，混合了顺序和并行组合，没有同步[2]。3可识别的：它是半线性的BPP [8]，可定义的添加剂理论时间自动机的实数[7]，一些字符串重写系统[5]中单词之间的可识别关系，包括下推过程（参见[14]中的微积分模型检查应用）。我们的方法在两点上有所不同：可识别性是在树自动机框架中，它需要我们发明一个新的进程代数来编码RPPS系统。文件计划我们首先回顾RPPS方案（第2节），然后介绍RPA（第3节）并展示如何忠实地编码RPPS方案（第4节）。然后，我们回顾树自动机的基本概念（第5节），我们需要证明我们的主要定理（第6节）并解释实际含义（第7节）。最后一节解释了如何RPPS标记之间的可达性可以解决NP与树自动机。2递归并行程序设计RPPS系统是作为RP程序的抽象模型引入的：我们请读者参考[13，15]以了解动机和示例。在这里，我们提出了正式的模型没有justi阳离子。2.1RPPS系统A = f a; b;：g是一组操作名称，不包含特殊操作cal l、wai t和en d。我们把A[fcall;wait;endg]写成A~（rangedoverbyy;;：：）。q0一问呼叫二季及六季BC第三季及第七季等q4aQ5端致电Q8等待Q9端Fig. 1.的方案一个方案是一个有限根图G= hQ; q0; i其中Q是节点的nite集合，q 02 Q是初始节点，4Pjf（ ）j=1gj=（1+jj）.一！！等级制国家之间：！是最小的三元组集合（s; a; s0），写为是将任何节点q映射到（A Q）[（fcal lg QQ）[（fwai tg Q）[fendg.具有笨拙的数学外观，但在图形上易于理解：每个节点后面通常是一个节点，有时是一对节点或根本没有节点。例如，图1中描绘的系统1具有（q 0）=ha;q 1i;（q 1）=hcal l;q 2;q 6i;（q 9）=en d.2.2行为语义学G的行为语义是通过一个无限标号的变迁系统MG给出的.非正式地，MG的状态是以父子关系（通过调用指令将进程与产生它的父进程相关联）组织的节点的多集合（表示并发进程的当前控制状态）。下面给出了相应的形式定义，我们参考[13，15]以获得更多的直观信息。形式上，系统G的分层状态（也称为“标记”或“状态”）的集合是最小集合M（G）s. t。对于G的任何n个节点（不一定是不同的）q 1;：; qn，以及分层状态s 1;：;s n2M（G），多集s=f（q1;s1）;：;（qn;sn）g在M（G）4中。特别是，2M（G）。我们使用习惯的符号\s+s 0“、\ss0“、：来表示多集的和、包含、：以及层次状态。 下面我们把单例多重集f（q; s）g写成（q; s）。状态的大小j s j由下式给出：defqi; si i;：i=1;：si我们现在正式定义什么是过渡！M（G）A~M（G）s！s0，满足以下规则：action：if（q）=（a; q0）then（q;s）！一（q0; s）对于所有 s，（Ga）端end：if（q）=endthen（q; s）！ s for all s，（Ge）call：if（q）=（calll;q0;q00）then（q;s）call （q0;s+（q0 0;;））对于所有s，（Gc）wait：if（q）=（wait;q0）then（q;;）wait （q0;;），（G w）第1节：如果s！第2章：如果！s 0然后s+s00！s 0then（q;s）！所有s00的 s0+ s 00，（Gp1）（q; s 0）对所有q 2 Q.（Gp2）511nn并行性的规则101和102表示任何活动的s！ s 0当兄弟在场时（即在一些s+s00中）或当父母在场时（即在一些（q; s）中），仍然可以发生。等待规则说明了我们如何4一个形式为s= f（q ;s）;：;（q ;s）g的层次状态有n个完全独立的-dentconcurrence ntactivities. 一个子活动sayy（qi;si）是协程（当前处于状态/n odeqi）及其类的子活动（si部分）的发起。6G0 00CB=defdef1如果所调用的子都被终止（然后不再存在），则仅在状态Q中执行等待语句。其他规则说明了如何创建和保持子调用。最后，M是hM（G）;A~;！其中，初始状态是sd=ef（q;;）。实施例2.1（q0;;）（q1;;）呼叫！（q 2;（q6;;））！（q2;（ q7;;））呼叫！（q 2;（q 8;（q 6;;）！ （q 3;（q 8;（q 6;;）是系统的执行序列，项MG与图1的方案相关联。1.一、正如等待规则所示，只能通过等待步骤退出的节点有条件地行为：我们用Q表示？Q的状态q的集合，使得（q）=（wai t;q0），对于某个q0，而Q！ 表示Qn Q？.3进程代数RPA我们现在定义一个RPA，一个进程代数，用于编码RPPS方案。3.1RPA术语设方案G= hQ; q0;i是固定的，def由t; u; v;：范围覆盖的RPA项的集合，或仅"\terms”，由以下语法给出：t; u：：= cjtI u：对于t项，我们将State（t）写为在t中出现的来自Q的所有节点的集合。t的大小，记为j t j，是t中符号的数量，由j c j = 1和j t I uj = 1+ j t j + j u j给出。RPA术语是二叉树，但左侧和右侧不起作用相同的角色，所以更自然地将它们看作梳子，在最左端有一些来自Const的c，在脊柱的右边有一系列子项（见图2中的示例）。这促使我们引入方便的缩写\cIn （u1;：;un）"，通过ycI0（）=0和cIn （u1;：;un）=cIn（u1;：;un1）Iun.我们只使用\In“在左边有一个c2常量的缩写。我IunIUN1cu1一7图二、cIn（u1; ：;un）8一个（保护的）RPA分类是TG上的有限集QA~C，规则，写作f q ic i; t ij i = 1;：; n g。 q i不需要是不同的。 为为了技术上的方便，我们要求所有的q2Q至少出现在一条规则的左边。3.2语义设Actd=ef A~f！;？G. 为了方便，我们写！ 然后呢？ 而不是（;！）和（;？）。一个声明并不意味着一个有标签的过渡！TG Act TG，由以下SOS规则给出：R1如果（q！！！q 0;t）2Q 2 Q！R3tt！问！q0It你好！uIt0R2如果（q！什么？什么？q 0;t）2Q 2 Q？R4tt！问！q0ItuItuIt0！不的t0R5？t！的t0R6if（ i）=;！tI ut0Iu什么？tIu！t0IuX直觉是，一个步骤t！u在T G中编码一个步骤st！su（单位：MG）（其中ST是由T表示的分层状态）。 额外的标签x=！（分别）x=？）意味着该步骤可以（分别不能）发生在活动子进程之上。标签由规则R1、R2选择，由规则R5、R6测试，并根据语义传播。我们写信给你！v（resp. u！？（五）当什么？v（resp. u！v）对于某些人，和uV当你！！v或u！？nn;！v. F或n2N，我们让\！”和\！“表示特别是迭代关系（！）n和！！nn. 还有！ 表示所述闭包Sn2N. 像往常一样，\u“和\u“分别意味着你！v3.3RPA步骤对于一些V（resp.对于无V）。00！9现在我们列出一些关于项之间的转换的关键引理。这些结果旨在解释如何将一个复合步骤分解成更小的步骤，并将成为第6节中构造的基础引理3.1如果u I v！w则w具有形式u 0I v 0，并且（u！u 0和v = v0）或（v！v 0和u = u 0）。证据 通过对规则R3{R6.2引理3.2如果u！ 则j v j> j u j。10nG！！（t 6！C！V，证据 通过归纳法推导出u v。基本情况是转换问！ q 0I t.2引理3.3q！q 0iq = q 0.证据 问！ q 0使得n = 0（引理3.2）。2接下来的六个引理在附录中得到了证明。 引理3.5给出一个C角色化！！ .引理3.4 u！引理3.5u！！iState（u）6=;.vi对于所有的t 2 T G，uIt！vI t.引理3.6 v It！！v0It0iv！！0和t！t0.（t06！ V！v0，或 v v 0.！引理3.8 q！v It i存在c和u s. t。（q！c ; u）是一个规则，，u！t和引理3.9q！！或者c！！ v.vItiq2Q！并且存在C和U S. T。问！c; u是a规则，你！t和c！！v.4将RPPS方案嵌入RPARPPS方案G的行为可以被忠实地编码在RPA中。我们考虑一组规则G从。对于任意的q2Q，操作：如果 （q）=（a; q 0）则包含q！一q0;0，（Da）端end：if（q） =end thenG包含q！ 0; 0，（De）呼叫call：如果（q）=（call1;q0;q00），则G包含qq0;q00，（Dc）等若（q）=（wai t;q0），则G包含qq0;0.（D w）引理3.7vIt！v0It0it！t0和11G可以看作是从Q到A~C的一个应用。我们现在将分层状态S（t）与任何项t2TG相关联，并且将项T（s）与任何s2M（G）相关联。目的是定义什么分层状态由项t编码，以及什么项可以用于编码分层状态s。121n1n11 nn11 nn1n1ndef命题4.2的含义是，对抽象映射取模映射S和T 归纳地定义为T（f（q;s）;：;（q;s）g）d=ef0In（qIT（s）;：;qIT（s））（T）S（0In（u;：：;u））d=efS（u）++S（u）（S1）S（qIn（u;：：;u））d=ef（q;S（u）++S（u））（S2）其中，T（s）的等式（T）要求我们对多集s的元素进行某种排序。S和T的行为类似于一个抽象-具体化对：引理4.1对于所有s 2 M（G），S（T（s））= s。证据通过对s的结构归纳，使用方程（T，S1，S2）。2S产生RPA项之间的等价：t Su，S（t）= S（u）。我们把u的等价类写成[u]w.r.t.。S和T S 对于TG的等价类的集合.注意S不是一个同余：（0个 Iu）S u，而（0Iu）I v6S uIv现在可以说明RPA项之间的步骤如何与RPPS分层状态之间的步骤相关。这是通过抽象的！还是？RPA步骤携带的额外标签，仅用于组成步骤的定义。 我爱你！ 当你！ t为一些“2f！;？G.4.21. F或u;v在TG和A~中，如果u！t则S（u）！S（t）。2. F或所有s;s0在M（G）和A~中，如果s！使得S（u）= s 0。s 0，然后T（s）！u为一些 u2tG证明（想法）。1.一、（分别）2.）的情况。通过对u（resp.s）和繁琐的案例分析。2从行为到发送“到，S是RPA之间的二进制运算G生成的变迁系统和我们要分析的变迁系统MG5树语言与树自动机在这里，我们回顾了我们需要的经典树自动机概念。 我们参考[6] [22]更详细。5.1树语言给定一个nite ranked字母表F = F0[ F1[：[ Fm，TF表示从F构建的nite树（或项）：例如，F0 = fa; b g，F1 = fg; h g13defS并且F2= ffg，TF包含树a，f（a; b）和f（g（f（h（b）; a））; b）.树语言是T F的任何子集L。5.2树自动机一个自动机是一个元组A=hF;Q;F;Gi，其中F是一个niteranked字母表，Q=fp;p0： g是一个 控制状态集合Q是一组接受态，而n[n2N（QFnQn）是一组转换规则. 我们参考[6]（或[17]）中关于树t何时为由A的状态p识别，写为p7！t. 对于p 2 Q; L（p）表示f t j p 7！tg。L（A）=p2FL（p）是A识别的树语言。例5.1继续前面的例子，设Q =fp0;p1g，规则集描述了一个自顶向下的树自动机p 07！一个p 07！ bp 17！ g（p 0）p 07！ g（p 1）p 07！ h（p1）p17！ h（p 0）p 07！f（p 1; p 1）p 07！f（p 0; p 0）p 17！ f（p 0; p 1）第17页！ f（p 1; p 0）f（h（b）; a）的一个可能的导数是p 17！ f（p 1; p 0）7！ f（h（p0）; p 0）7！f（h（p 0）; a）7！ f（h（b）; a）. 所以是17号！ f（h（b）; a）.5.3交替树自动机一个交替树自动机是一个元组A=hF;Q;F;n+i，其中n own是一个从QFn到B+（f1;：;n g Q）的n -索引映射族。这里，对于给定的集合X，B+（X）是X上的正布尔公式的集合（即，使用^和_）从X中的元素构建的布尔公式，其中我们也都知道for mulastrue和fals e。 F或例子we可以有一个ven（p;f）=（1;p1）_（（1; p 2）^（2; p 3）^（2; p 4））。我们参考[22]中关于树t何时被某个交替A的状态p识别的经典定义众所周知，标准树自动机可以看作是交替自动机，其中只使用析取，交替树自动机识别的树语言类正是非交替树自动机识别的树语言类。5.4树上的可识别关系我们遵循[6，第3章]和[16]。一 个元组h t 1;：; t ni，来自T F的n棵树可以看作是一棵树，记为t1tn，在产品字母表F nd=ef （F[f？g）n，其中f的假设，f？ 有arity0。*fn是最大值F或例如对hf（a;g（b））;f（f（a;a）;b）i也可以看作ff（af（？114a;？a）; gb（b？））。Fdef_<否则为false我们说一个n元关系RTn在所有t 1的集合中是可识别的tn for（t1;：;tn）2R是Fn上的正则树语言.6RPA可达关系的可识别性可达性关系！ 还有！！RPA术语之间的区别是：引理6.1集合L项=fu2T Gj u 6！g的终止条款是可识别的。证据u6！iState（u）=;（引理3.4）。因此，具有唯一接受状态p#和转移规则（p#;0）=truee;2我们现在考虑交替自动机A！其状态为p，p，p#所有的pt和pt对于t是某项的子项，出现在（因此，jQj在O（j，j））。A！识别成对的术语。 在这里我们定义交替过渡函数f*(2) 当f（p0;fg）没有明确定义时（对于某些p02Q和某些f;g2（F[f？g））这意味着 f（p0;fg）是假的，（3）我们可以量化所有的q2Q，所有的c2 Const和所有的f2（F[f？g）。（如果q=q0，n（p;II）=（2;p）^（1;p）_（（2;p#）^（1;p））（4）（p;II）=（1;p）^（2;p）（5）（p;qI）=问！c;u（2; pu）^（1;pc）_（（2; p#）^（1; pc））（6）8>_（2; p u）^（1; pc）如果q2 Q！、（p;qI）=q！c;u否则为false（七）10（p;qq0）=（三）>：11不不否则为false不不否则为falsef（p;f0）=f（p;f0）=（如果t=0，（八）f（p;fq）=f（p;fq）=（trueift=q，（九）（pt1It2;fI）=（2;pt2）^（1;pt1）_（（2;p#）^（1;pt1））（10）（pq;fI）=<$（pq;fI）=<$（p;qI）（13）该自动机满足以下正确性性质：引理6.2L（p）=fuvju！vg;L（p）=fuvju！！L（p）=fuvjt！vg;L（p）=fuvjt！！vg;（14）vg;（15）t tL（p #）=fuv j v 6！g;（16）其中u; v是TG[f？G.（S ket ch）的Pr。对于k（p#;：：：）的规则是（1）的明显修改，因此它们适用于一对u v中的第二个元素，而我们不考虑第一个元素。证明是通过归纳导子u！v，. . .，对于（）方向，以及对于（）方向，通过乘积项的归纳事实证明，（2）和（13）之间的每一个转换规则都是由我们已经证明的行为性质所例如，引理3.3解释了(3) 而引理3.4考虑了所有规则f（p#;fg）。类似地，（5）是一个直接的引理3.6的转置2我们得到一个重要的推论：第6.3章关系！还有！！是可以识别的。 而且有树自动机识别它们只需要O（j （j）国家。证据为了清晰起见，我们的构造使用了一个交替自动机（定义循环的12子句模仿了3.3节中的引理），但是很容易调整构造并得到一个O（jj）状态的（非确定性自下而上）树自动机。27应用定理6.3直接导致RPA项（和RPPS方案）的可判定性结果。这些结果的好处是，它们都涉及到13defC同样的平滑和一般自动机理论推理。真正的能力和设置。对于任意可识别语言L，集合Pre（L）d=effuju！v对某些v2Lg和Post（L）d=effujv!u对于某个v2 Lg是可识别的，并且对应的自动机可以通过自动机上的标准交集和投影构造在多项式时间内获得（假设L的自动机是已知的）。约束条件下的可达性这些结果可推广到约束条件下的能力，即 到 的 集前C（L）=fu ju！对于某些v2L和2Cg且Post（L）d=effujv！u对于v 2 L和2 C g，其中C作用 这是一个限制AC-可接受标签的可达性。 不是所有的正则CAct都可以用这种方法处理（见[17，16]），但有趣的正则约束，称为可分解约束，是允许的[21]。对逻辑EF进行模型 使用Pre和标准构造进行交和补，可以针对模态逻辑EF的任何公式“计算满足”的所有项的集合M od（“）（参见[17，19]）。在这里，EF甚至可以用可分解的约束来丰富。注意，由于双相似过程满足相同的EF公式，我们有sj=“iT（s）j=”，从而使本文的方法包含了所有的RPPS方案的模型.对转换逻辑进行模型检查。EF只需要Pre（L）的有效可识别性就可识别L.但要有辨识度！，我们得到一个简单的模型检测算法的全转换逻辑5，即。的一阶逻辑FO（！;！）. 详情和应用见[16]。8RPPS标记在这里，我们将RPPS标记之间的可达性问题简化为RPA术语之间的可达性问题。由此，我们得到了一个简单的RPPS可达性自动机算法，由此可容易地导出可达性的NP-完全性。写u） v当uu0！v0S对于某个u 0; v 0. 我们采用通常的扩展u）v（对于（2）（v）。RPPS之间的可达性标记简化为）-reachabilityybetweenRPAterms，infollowing-正常意义：命题8.1给定两个RPPS标记s和s 0，s！T（s））T（t）in T G.s0inMGi145很难扩展这个可判定性结果：通过将网格结构编码到RPA中，我们可以很容易地证明，模型检查MSO（），一元二阶逻辑，作为唯一的谓词，在RPA项上是不可判定的15是的。 Combine Prop. 4.2的定义）。28.1S的另一个特征我们的下一个任务是获得S的表征，这是更易于管理的，从一个正规的树语言的观点。我们通过几个小步骤，借助RPA项之间的一些简化或置换关系来实现这一点。基本概念（连续性，交换，. . .）在本小节中使用的是标准的减少系统的研究（见例如，[12]）。8.1.1简化关系y和y由以下擦除规则归纳定义0Iuyu（E1）cIn+m1（t1;：;tI1 ;u1;：;um;ti+1 ;：;tn（E2））如果tiu，则cIn（ t1;：; tn）cIn（ t1;：; ti1;u; ti+1;：; tn）（E3）我们让&表示y [&，并将使用并置来表示关系的组成。 注意ty&u暗示t&yu，并且tyyu暗示t&yu。 因此，我们写&的reexi ve-transiti ve封闭&，我们推出，&&符合y，然后与&y=，其中y=表示y[Id]。当t &u时，我们说u是t的一个化简。 我们写作。 和.以表示反向关系（&）1和（&）1。 因为u &t意味着j u j> j t j，&是Noetherian的，并且是一个良好的偏序。引理8.2（Conuence）如果u.v &w，则u = w或u &v 0。w表示某个v 0。证据 通过对v的归纳和案例分析。 见附录A.7。2因此，通过Newman引理，&是收敛的：我们让t #表示t的简化范式，即。 通过尽可能地简化t来获得唯一的u。8.1.2置换的关系由以下规则归纳定义：cIn（t1;：;tn） cIn（t1;：;ti1;ti+1;ti;ti+2;：;tn）（P1）如果tiu，则cIn（t1;：;tn）cIn（t1;：;ti1;u;ti+1;：;tn）（P2）是对称的 我们写的自传递闭包 .当t u时，我们说t和u是置换等价的。下一个引理允许交换简化和置换：引理8.3（交换）如果uv&w，然后u。 v 0cIn（t1;：;ti1;0Im（u1;：;um）;ti+1;：;tn）&