理论计算机科学电子笔记175（2007）47-64www.elsevier.com/locate/entcs关于弱扩展PAD的符号验证AhmedBouajjania，1，JanStrejcekb，2 andTayssirTouili a，3aLIAFA、CNRS和法国b捷克共和国布尔诺马萨里克大学信息学院摘要我们考虑一类称为wPAD的无限状态系统的验证问题。这些系统可以用来模拟程序（可能是递归的）过程调用和动态创建并行进程。它们对应于用非循环有限状态控制单元扩展的PAD模型，其中PAD模型可以被视为前缀重写系统（下推系统）与上下文无关的多集重写的无同步Petri网（Synchronization-Free Petri Nets）最近，我们已经提出了符号可达性技术的PAD类的基础上使用一类无排名树自动机。 在本文中，我们推广我们以前的工作，类wPAD是严格大于PAD。 这种推广带来了一个积极的答案，一个开放的问题，对EF逻辑的wPAD模型检测问题的可判定性。此外，我们展示了如何符号可达性分析的wPAD可以用于（下）近似同步PAD的分析，一个（图灵）多线程程序的强大模型（在并行进程之间具有不受限制的同步）。 这导致了一种实用的方法，用于检测这些模型中存在的错误行为，该方法基于有界可达性范式，这里考虑的界限是同步动作的数量。保留字：重写系统，有限状态系统，符号可达性分析，模型检测1引言关于软件系统的推理需要考虑强大的模型，这些模型通常处于有限状态，即，它们可能具有无限数量的可达到的配置。状态空间的复杂性和无限性的来源可能与数据操作有关，例如在无限数据上使用变量域，动态和无限大小的数据结构等，或复杂的控制原语，如过程调用，（无界）动态创建并发1电子邮件地址：abou@liafa.jussieu.fr2部分由理论计算机科学研究所（ITI）研究中心项目No. 1M0545这一页是在J. 在L a B R I中，Strejjce k的位置不太重要，U i v e r i s t e B o r - deaux 1。电子邮件地址：strejcek@fi.muni.cz3电子邮件地址：touili@liafa.jussieu.fr1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.05348A. Bouajjani等人理论计算机科学电子笔记175（2007）47处理这种复杂性的一种流行方法是将抽象方法与模型检查相结合。谓词抽象等技术允许处理数据操作等方面，并在有限的数据域上生成抽象模型。然后，这样获得的抽象模型可以使用模型检查算法自动分析，只要这样的算法存在于所考虑的抽象模型类。当抽象模型是有限状态时，情况显然就是这样。然而，如上所述，为了考虑复杂的控制原语，例如过程调用和进程创建，有限状态模型的表达能力不够。例如，在具有递归过程调用的顺序程序的情况下，所需的抽象模型是（无界堆栈）下推系统，而对于具有通信有限状态进程的动态创建的程序，自然模型是（无界）Petri网。幸运的是，存在几种算法技术（例如，可达性分析，模型检查），这些都是为分析和验证这些无限状态模型而开发的。在本文中，我们考虑的情况下，程序可能包含（递归）过程调用和动态创建的进程（线程）。一种可能的方法来建模这样的系统是结合下推系统与Petri网。这与[17]中介绍的过程重写系统（PRS）的使用相对应。这些模型实际上可以被看作是prefix重写系统和multiset重写系统的组合。PRS在程序建模中的相关性已经在[8，9，7，1，2]中讨论过。对程序建模特别感兴趣的PRS的子类例如是PA过程的类，以及更大的PAD过程类，其概括PA和下推过程并且对应于无同步PRS（即，在重写规则的左侧不允许并行合成的模型这些类中的进程确实允许使用过程调用和paradec-parend块（即，启动多个并行线程，并在继续之前等待它们的终止）。PAD还允许从顺序过程调用返回值。Richard Mayr已经证明了PRS的可达性问题（给定状态是否可以从另一个给定状态到达）是可判定的，使用Petri网的可达性问题的约简[17]。为了获得实用的验证算法，已经研究了PRS的重要子类（如PA [16，9]和PAD [1，2]）的符号可达性算法这些算法使用（各种）树自动机来表示（规则）有限组的配置（即，过程术语）。特别地，我们在[2]中提供了一个通用构造，允许计算PRS的任何子类的（前向或后向）可达配置的集合，该PRS的任何子类是从前缀重写系统与多集重写系统的有效半线性类的组合构建的（即，一类系统，其可达集总是半线性的和有效可计算的）。我们已经表明，这导致了一个象征性的可达性分析算法的PAD进程在一定的正常形式。PRS形式主义不是图灵强大的，因为它对并行进程之间的同步方式有一个微妙的限制。粗略地说，A. Bouajjani等人理论计算机科学电子笔记175（2007）4749PRS的语义意味着同步只能在具有空栈的并行进程之间被允许为了扩展PRS的建模能力，一种方法是通过异步操作（a`laCCS）添加同步时钟，其中允许使用称为同步PRS的Turningpowful模型[21]。类似地，PAD可以扩展为同步PAD（这也是图灵强大的模型）。在[21]中已经提出了使用抽象技术的这些模型的近似分析算法用于增强PRS（和PAD）的建模能力的另一方法包括添加全局控制状态。 新模型称为sePRS [11]，可以看作PRS与代表全局控制的有限状态自动机的并行产品。显然，sePRS是图灵强大的，因为它们允许通过全局控制状态在递归并行进程之间进行然而，如果控制自动机的结构是弱的，这意味着它的所有循环都是自循环，那么可以证明所获得的模型（称为wPRS）具有可判定的可达性问题[12]（该证明使用了Petri网可达性问题的可判定性类似地，如果我们将控制状态添加到PAD过程中，我们获得了图灵强大的模型，但是用弱控制自动机扩展PAD导致到模型，称为wPAD，具有可判定的可达性问题，有趣的是，可以证明它是严格更强大的（w.r.t.[13]比《易经》强本文推广了文[2]中关于符号可达性分析的结果。虽然[2]只处理PAD过程在一定的正常形式（现在称为规范PAD），在这里，我们表明，可达性状态的集合是可计算的，甚至是（一般）wPAD系统的有效表示。为了做到这一点，我们采用基于所谓的交换对冲自动机（CH-自动机）的符号表示，允许以顺序组合的结合性和并行组合的结合性-交换性为模来定义过程项的集合。我们证明了这些表示是等价封闭的，对摄影后图像和摄影前图像的插补（即，所有后继者和所有前驱者的计算），以及在后图像和前图像下直接后继者和前趋者的计算）。此外，我们解决了全局模型检查问题的wPAD对EF逻辑。我们考虑EF逻辑的一个变体，它通过使用对应于（潜在无限）可使用CH-自动机定义的配置集的原子命题来推广标准的我们证明，对于这个逻辑中的每个公式，都有可能构造满足这个公式的所有配置（在给定的wPAD中）的集合的（基于CH-自动机的）表示。这一结果解决了[14]中关于wPAD的模型检验问题的一个公开问题请注意，全局模型检查是一个比确定给定配置是否满足给定公式更一般的问题最后，我们表明，我们的结果有关的符号可达性分析的wPAD可用于分析同步PAD（SPAD）与有限数量的同步。这导致了一个近似的分析程序SPAD的基础上计算下近似的可达集，由con-sort。50A. Bouajjani等人理论计算机科学电子笔记175（2007）47只考虑可达到的配置，直到某个固定数量的同步。SPAD的这种近似分析方法可以在实践中用于确定错误行为的存在，遵循[18]中提倡的方法。它构成了对抽象分析（在[21]中为SPAD提供）的补充方法，该方法基于考虑可能行为集的上近似，并且对于确定不存在错误行为是有用的。2预赛2.1工艺术语令Const ={X，. . }是一组过程常数。 对于每一个CConst，C上的过程项的集合TC由抽象语法t：：= 0定义|X|特什特|t<$t，其中0是空闲项，X ∈ C是过程常数;并且<$t和<$t分别表示顺序和并行组合。我们用ω来表示一种通用的方式或。我们用ω表示算子ω（resp.如果ω=ω（resp.ω= ω）。过程项被认为是模以下代数性质：结合性，结合性和可交换性，0 w.r.t.和 设是由这些性质导出的T上的我们将过程术语分为四类：1S- 顺序G-规范形式中的过程项是由下式定义的t：：= 0 |S|ps：：= X|p1p2. n，n≥2p：：= X|s1s2. 你好，n≥ 2很容易看出，每一项都有一个标准形式的等价项. 在下文中，我们使用规范形式的项。如果t = 0，或者对于常数X，t = X，或者t = p1<$p2<$.，则项t称为seq-term。其中n≥2。在最后一种情况下，该项也称为带根项。此外，如果t = X1<$X2<$.，则t在seq-term处被称为t。对于n≥0，n =X n（n=0的情况对应于项0，n= 1的情况对应于过程常数X）。通过类比，我们定义了par-terms、par-rooted terms和par-atterms。2.2进程重写系统与弱扩张令M ={o，p，q，.. . }是控制状态的有序集合，并且Act ={a，b，c，. . }是一组动作。设α，β∈ {1，S，P，G}是过程项的类，使得α<$β.（α，β）-wPRS（weakly extended process rewrite system）R是一个有限的重写一形式为（p，t1）<$→（q，t2）的规则，其中t1∈α，t1/= 0，t2∈β，p，q∈M，p≤q，且A. Bouajjani等人理论计算机科学电子笔记175（2007）47511R21R2Ra∈Act.通过M（R）、Const（R）和Act（R），我们表示在R的重写规则中发生的控制状态、过程常数和动作的集合。一个（α，β）-wPRSR诱导出一个状态为对（p，t）的标号转移系统，使得p∈M（R）是控制状态，t∈β是Const（R）上的过程项.转移关系→R是满足以下推理规则的最小关系：一（（p，t1）<$→（q，t2））∈R一（p，t1）→R（q，t2）（p，t）→a（q，t）一（p，t1<$t）→R（q，t2<$t）（p，t）→a（q，t）一（p，t1<$t）→R（q，t2<$t）我们以一种标准的方式将转换关系扩展到Act上的有限词的∗用→R表示→R的自反传递闭包。为了缩短我们的符号我们用pt代替（p，t）。一个（α，β）-wPRS（其中M（R）是单例）称为（α，β）-PRS（进程重写系统）。在这样的系统中，我们从规则和状态中省略了单个控制状态代替（S，G）-PRS、（S，G）-wPRS、（G，G）-PRS和（G，G）-wPRS，我们分别使用更可读的名称PAD、wPAD、PRS和wPRS。让我们注意到，类PAD和wPAD将无限状态系统的广泛已知模型作为下推过程（PDA），基本并行过程（BPP）和过程代数（PA）。PRS和wPRS类也是Petri网（PN）的子模型更多信息关于（α，β）-wPRS和（α，β）-wPRS的表达性可以在[13，12]中找到。给定wPRSR的状态pt，我们定义P ost R（pt）={pJtJ|pt→aRpJtJforsomea}P ost（pt）={pJtJ|pt→RpJtJ}JJJJajJjj前R（pt）={pt t| p t →Rpt，对于某个a}PreR（pt）={pt| p t →Rpt}后向（pt）和前向（pt）集合称为（向前和向后）可达性R R集. PostR（pt）和PreR（pt）被称为1步（向前和向后）可达性集 这些定义和符号可以以显而易见的方式扩展到状态集合。2.3佳能PRS规范PRS R是一组重写规则，其形式为：一X1X2... X n<$→ Y1（1）一X1X2... Xn<$→Y1（2）其中n，m≥0。式（1）和式（2）的规则称为规则和规则分别 用Rω表示R的所有ω-规则的集合。 注意，集合R一和R′不必像某些规则那样不相交（例如，X <$→Y）是两种类型。设α，β∈ {1，S，P，G}是过程项的类一个规范的PRS被称为规范的一（α，β）-PRS如果R的每个规则t1<$→t2满足t1∈α和t2∈β. 最后，CanonicPAD代表Canonic（S，G）-PRS。请注意，规范PRS不一定是PRS，因为我们允许使用0的规则52A. Bouajjani等人理论计算机科学电子笔记175（2007）47RR一左手边此外，正则（α，β）-PRS的定义并不要求α<$β。Const（R），→R，PostR，PreR，. 是相同的给定一个正则（α，β）-PRSR，我们用R−1表示正则（β，α）-PRS，其规则是通过交换R的规则的左手边和右手边得到的。注意，对于每个过程项L的集合，PreR（L）= PostR−1（L），PreR（L）=后−1（L）。计算PRS系统的可达集的问题可以使用下面的定理转化为标准PRS的相同问题。这个定理的证明采用了[17]中给出的标准构造的一个变体然而，我们的定理在几个方面不同于[17]中的定理。特别地，（1）我们将（α，β）-PRS变换为正则（α，β）-PRS，这不是Mayr变换的情况项替换h是关于满足h（0）= 0和h（t1ω.的过程项的函数。ω tn）= h（t1）ω.ω h（tn）对于所有有限序列t1，.，tn的项，并且对于ω= ω，ω。换句话说，一个项替换完全由它在过程常数上的值来指定。我们说一个项代换h是有限的，如果集合{X|h（X）/= X}的过程常数是有限的。定理2.1对于每个（α，β）-PRS系统R和每个过程常数集C，我们可以构造一个正则（α，β）-PRS系统RJ和一个有限项替换h，使得对于C上的每个t1，t2∈Const（R）和每个a∈Act（R）我们有：aJ JJ J J一JJ(i) t1→Rt2i则存在t1，t2满足h（t1）=t1，h（t2）=t2，且t1→Rt2，(ii) t1→<$Rt2i表示存在 STJ，TJ满足gh（TJ）=t1，h（TJ）=t2，且DTJ→<$RJTJ.1 2 1 2 1 2aJ J证据 令size（t <$→ t）为在t和t中出现的次数。给定任意PRSR，设ki是既不是正则规则也不是正则规则的规则r∈R的个数，且size（r）=i。因此，对于每个i，R都是正则PRS iki= 0。在这种情况下，设n=0。否则，设n是最大的i，使得ki/= 0（n存在，因为规则集是有限的）。我们将范数（R）定义为对（n，kn）。首先，我们描述一个将（α，β）-PRSR变换为（α，β）-PRSRJ的过程，并定义有限项替换h，使得范数（RJ）范数（R）（相对于字典序），对于C上的每个项t1，t2，以及每个a∈Act（R），以下等价成立：
，其中QJ本身是不相交的并集QJ=Q0<$Q-，以及（2）Δ中的规则具有以下形式：（a）X→q，其中q∈Q−，X∈Const，（b）0→q，其中q∈Q0，（c）q→qJ，其中（q，qJ）∈（Q0）2<$（Q−）2<$（Q <$）2<$（Q）2，（d）<$（Reg）→q，其中Reg<$。Q\（QQ0）是正则语言，q∈Q<$，且（e）<$（<$）→q，其中q∈Q<$，<$是Presburger公式，使得FV（<$）={xq|q∈Q\（Q Q0）}.换句话说，Q中的状态（分别为）（1）树的根是（）。）。Q−中的状态识别C中的常数，Q0中的状态识别0。4计算规范PRS让我们考虑一个规范PRSR =RR，设A=（Q，F， Δ）是一个识别过程项集合L的我们证明了集合PostR（L）和PreR（L）是CH-自动机有效表示和可计算的。对于给定的正则PRS RJ和给定的一组项L1，我们写RJ（L1）作为PostRJ（L1）的缩写。在下面我们使用这样一个事实，即给定一个正则集L2的序列项，集合RJ（L2）也是正则的，并且很容易构造。这同样适用于任何半线性集L3的部分项和RJ（L3）。我们可以在AJ=（Q_i，F_i，Δ_i）中构造一个CH-平均，其中R（L）是可重算的，Q是状态的集合，F是状态的集合，Δ是规则的集合。LetC是一组有限的过程常数，使得C≠Const（R）和L≠C。4.1该组状态状态集合Q包括A的状态集合Q并且包含新状态qX，其被假设为精确地接受单例{X}（即，LqX={X}），对每个X∈C. 设QR是状态集QR={qX|X∈C}。 此外，集合Q包含识别Lq中的项的直接后继的集合R（Lq）的状态，对于每个q∈Q<$QR。为了确保（在构造过程中）识别出的树总是处于规范形式，我们需要划分根据它们的类型（由它们的根给出）识别树。我们将每个q∈Q<$Q R关联到不同的状态（q，−），（q，0），（q，n）和（q，n），识别出Lq中的项的直接后继项，它们分别是C中的常数，null（等于0），n-根项和n-根项。L etQ=Q0。我们证明了Q_n对以下几个集合的统一成立：（1）Q_n0=Q_n{（q，0 ） }|q∈Q<$QR} ， （ 2 ） Q<$−=Q−<$QR<${（ q ， − ） |q∈Q<$QR} ， 且 d （ 3 ）Q<$ω=Qω <${（q，ω）|q∈Q<$QR}，对于ω∈{ε，ε}. 更具 体 地 ， 我 们 可 以 确 定F={（q，−），（q，0），（q，−），（q，−）|q∈F}。4.2状态字母表上的重写系统CH-自动机中的规则（形式为ω（γ）→q）涉及对状态序列的约束，而系统R和R是在过程常数的字母表上定义因此，我们定义系统S=α（R）和S=α（R），其中α58A. Bouajjani等人理论计算机科学电子笔记175（2007）47.Σ˜˜.Σ ˜ΔωX˜1˜1我˜˜ΔΔ1ΔMΔΔ是替换，使得对于每个X∈C（以标准方式扩展到项、规则和规则集），α（X）=qX4.3转换规则集合Δ被定义为最小的转移规则集合，其中（1）包含Δ，（2）包含规则集合X→qX，对于每个X∈Const，以及（3）使得：（β1）闭合规则：过程常数和0的后继：(a) 如果X→εq，则nωS（q）→（q，ω）∈Δ，(b) If0→Δq，thennω。Sω（0）→（q，ω）∈Δ。规则（a）说，如果X在Lq中，那么通过应用一次系统R ω而得到的所有它的直接ω-后继也是Lq的直接后继。规则（b）对于0的后继者也是如此。（β2）闭包规则：ω-根项的后继：如果ω（γ）→p∈ Δ，则ω Sω（σ（γ））→（ p ， ω ） ∈ Δ ， 其 中 σ 是 置 换 ， 使 得 <$q∈Q<$QR ， σ （ q ）={q}<${qX|X→<$Δq} <${0|0→Δq}。这 规则 说 的如果 ω（X1，. ，Xn）∈Lp和ω（XJ，. ，XJ）∈Rω。ω（X1，.，Xn）n，则ω（XJ，...，XJ）是Lp的ω-后继.（β3）传播规则：若ω（γ）→p∈ Δ，则ω。Eω（γ）ε→（p，ω）∈Δ，其中E是一个正则PRS，定义为E={q <$→（q，−），q <$→（q，），q <$→（q，）}。该规则表明，如果n（t1，...，tn）∈Lp和TJ是t1的后继，则（tJ，.，tn）是Lp的后继者。 此外，如果n（t1，.，tn）∈Lp且tJ为1我t i的后继，则n（t1，. ，tJ，. ，tn）是L p 的后继者。注意，我们需要区分E（γ）和E（γ），以确保正确地考虑了预修复重写策略。（β4）术语解释注意规则：(a) Ifω（γ）→（q，ω）∈ΔandqJ∈γ，thenqJ→（q，−）∈ΔifqJ∈Q<$−，annd如果q j ∈ Q <$ω，则qJ→（q，ω）∈Δ<$i。(b) 若ω（γ）→（q，ω）∈Δ且0∈γ，则0→（q，0）∈Δ。如果ω（t）是Lq的后继，那么t也是Lq的后继。现在我们证明这个构造是正确的。引理4.1对于每个过程项t，以及每个q∈Q<$QR，我们有：(1) t→εe（q，0）i∈PostR（Lq）且t=0，(2) t→εe（q，−）i εt∈PostR（Lq）anddt∈C，(3) t→εe（q，ω）i∈P ost R（Lq）且root（t）=ω，frω∈{ε，ω}.证据我们考虑（更复杂的）从左到右的方向。证明是通过对t的结构归纳：• t=X→E（q，−）（eec与eret=0→E（q，0）相似）。不是因为有规则Δ Δ∗ ∗ofΔ不允许形式X→e（q，0）或X→e（q，w）的导子。MA. Bouajjani等人理论计算机科学电子笔记175（2007）4759˜.Σ˜1(i)存在w∈ {\displaystyle w}，||}，使得w（γ）→Δq，ω Sω（σ（γ））这种推导必然具有以下形式：X→eqX→e（q，−）Δ Δ其中规则qX→e（q，−）是β4-规则。有三种情况：Δ。ΣΔ，且qX∈Sω（σ（γ））. 假设ω= π，另一种情况，其中ω =||是相似的。这意 味 着 存 在 qX1···qXn∈σ （ γ ） 使 得 qX∈S<$ （ qX1···qXn ） 。 这 意 味 着 X∈R（X1，...，Xn）。 由于qX1···qXn∈σ（γ）且<$（γ）→Δq，则有<$（X1，.，Xn）∈Lq.因此，X∈R（Lq），即， X∈PostR（Lq）.(ii) 这是一个常数Y，满足Y→Δq，ω。Sω（qY）→（q，ω）isinΔ，anndqX∈Sω（qY）.这里还假设w= 0，另一种情况是w =||是相似的。这意味着qX∈S<$（qY），并且X∈R<$（Y）。由于Y∈Lq，它遵循X∈R<$（Lq），即，X∈PostR（Lq）.∗(iii) 0→Δq，ω.Sω （0）电子邮件→（q，ω）i s i n Δn，an n d q X∈Sω (0).这里还假设，w= 0 ， 另 一 种 情 况 ， 其 中 w =|| 是 相 似 的 。 这 意 味 着 qX∈S<$ （ 0 ） ， 且X∈R<$（0）。 由于0∈Lq，因此X∈R<$（Lq），即， X∈PostR（Lq）.• t=t（t1， . . ，tn）→ne（q，n）.当我们在这里的时候，||（t1， . . ，tn）→ne（q，||）issimilar.Δ有三种情况：(i) 存在n个常数X1，...，Xn，使得t= t（t1， . . ，tn）→nen（qX， .. . ，qXΔ）→e（q，n）.Δ1nΔ在这种情况下，每个ti都必须等于常数Xi。 然后，Δ-规则其中qX1···qXn∈Reg是β1或β2规则。让我们考虑它是β1-规则的情况，另一种情况也是类似的。设X当X→εΔq时，Reg=Sε（qX）. SinceqX·· ·qX∈Reg，n如前所述，这意味着，，Xn）∈R（X），即， 由于X∈Lq，（t1，.，tn）= n（X1，.，Xn）∈Post R（Lq）.(ii) 存在k个常数X1，. ，Xk和n-k状态qk+1，... ，qn，使得t= t（t1， . . ，tn）→nen（qX， .. . ，qX，qk+1， . . ，qn）→ e（q，n）.Δ1kΔ在这种情况下，对于每一个i，1≤i≤k，ti必然等于con-i。对于i，k+1≤i≤n，ti∈Lqi。Δn，Δn-规则→（q，ω）在60A. Bouajjani等人理论计算机科学电子笔记175（2007）47（Y1，.，Ym，tk+1，.，tn） .其中qX1···qXkqk+1···qn∈Reg必是β2规则.设φ（RegJ）→q是Δ中的规则，使得Reg = Sφ （ σ （ RegJ ） ） 。 由 于 qX1···qXkqk+1···qn∈Reg ， 因 此 存 在qY1···qYmqk+1···qn∈σ（RegJ）使得qX1···qXkqk+1···qn∈S（qY1···qYm qk+1···qn），则-前 的 qX1···qXk∈S（qY1···qYm），和 因此 的 X1，.，Xk）∈R. Ⓢ （Y1，.，Ym）n，兰蒂昂的X1，.，Xk，tk+1，. ，tn）∈R∞.ⓈA. Bouajjani等人理论计算机科学电子笔记175（2007）47611m.Σ11.Σ由于qY ···qYqk+1···qn∈σ（Reg J），我们得到，Y1，.，Ym，tk+1，.，tn）∈Lq，和以来X1，.，Xk，tk+1，.，tn）∈R（Y1，.，Ym，tk+1，.，tn），则可以得出：，Xk，tk+1，.，tn）∈后R（Lq）。因此t= t（t1，.，tn）= n（X1，.，Xk，tk+1，.，tn）∈PostR（Lq）(iii) 存在n个状态q1，...其中至少一个Q1具有形式（p，||）或（p，−），其中t= t（t1， . . ，tn）→εeε（q1， . . ，qn）→ e（q，n）Δ Δ在这种情况下，在推导过程中应用的最后一个规则必然是β3规则。那么，β3意味着对于每个i，2 ≤i ≤ n，qi∈ Q，并且状态q1具有形式（p1，||）（形式为（p1，−）的情况类似）。更确切地说，它意味着在Δ中存在规则<$（Reg）→q，n（RegJ）→（q，n）in Δnsuchthatp1q2·· ·qn∈Regandd（p1，||）q2·· ·qn∈Regj.通过结构归纳，得到t1∈PostR（Lp1）.设tJ∈Lp1为使得t1∈PostR（tJ）。 由此得出，n（t1，... ，tn）∈ Post R.（tJ，. ，tn）n，1 1并且由于对于i，2 ≤i≤n，ti∈Lqi 我们有：（tJ， .. . ，tn）→nΔn（p1，q2， . . ，qn）→Δq因此，t = t（t1，.，tn）∈Post R（Lq）.Q因此，我们有：定理4.2对每一个标准PRS R和每一个CH-自动机A，我们有PostRL（A）= L（AJ）。由于PreR（L）=PostR−1（L），前面的构造也可以用来计算1步向后可达集。5计算PAD和wPAD在本节中，我们解决了PAD和wPAD系统的可达集和一步可达集的计算问题。 计算可达集一般来说，对于PRS来说是困难的。原因之一是Petri网的可达集已经不是半线性的。在[2]中，我们证明了给定的正则PRS系统R的可达集可以有效地计算，只要其基础多集重写系统R∈E是半线性的。例如，由于[6]关于上下文无关的多集重写系统（BPP过程）的结果，规范PAD系统。定理5.1（[2]）设A是识别过程项集合的CH-自动机，R是规范PAD。然后，集合Post（L（A））和Pre（L（A））是com--R R可以用CH-自动机来表示。62A. Bouajjani等人理论计算机科学电子笔记175（2007）47RRRRRRR，RRq，qR利用这个定理和前一节的结果，我们得到如下结果。定理5.2对于每垫R和每个CH-自动机A，集合PostR（L（A）），PreR（L（A）），P
我的内容管理
展开
