多线程程序的分析与验证

理论计算机科学电子笔记138（2005）153-178www.elsevier.com/locate/entcs同步PA系统的可达性分析艾哈迈德·布阿贾尼LIAFA，巴黎7大学，2 place Jussieu，75251 Paris cedex 5，法国abou@liafa.jussieu.fr哈维尔·埃斯帕萨计算机科学形式方法研究所，如果你想去斯图加特，你就得去斯图加特。38，70569Stuttgart，Germanyesparza@informatik.uni-stuttgart.de泰西尔·图伊利LIAFA，巴黎7大学，2 place Jussieu，75251 Paris cedex 5，法国touili@liafa.jussieu.fr摘要我们提出了一个通用的方法分析并发程序（无界）动态创建线程和递归过程调用。 我们根据一组术语重写规则定义了此类程序的模型，其中术语表示控制配置。该模型的可达性问题是不可判定的。因此，我们提出了一种方法来分析这些模型的基础上计算抽象的计算路径集。 我们的方法允许计算这样的抽象作为（路径语言）约束系统的最小解。 更准确地说，J给定一个程序和两个正则配置集（过程项）T和T，我们提供（1）一种系统结构，其特征是将组合部分的选择从T学习到T，以及（2）一种基于抽象解释的通用框架，允许解决这一问题系统在各种抽象领域导致不同精度和成本的抽象分析关键词：多线程程序与过程调用，进程代数，程序分析，验证。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.063154A. Bouajjani等人理论计算机科学电子笔记138（2005）1531介绍分析和验证多线程程序是当今程序分析和计算机辅助验证中最重要的问题之一。这个问题在编程语言允许（1）动态创建并发线程和（2）递归调用过程的情况下尤其具有挑战性众所周知，一旦考虑到同步和过程调用，可达性问题（即使是控制点）也是不可判定的（见[24]）。因此，任何对这类程序的分析或验证算法都必须考虑可能的计算路径集合的上近似。在以前的工作[5]中，我们介绍了一个通用的框架，用于计算一类多线程程序的路径集的抽象。我们已经表明，这个框架的实例化导致几个分析程序与不同的精度和成本。在这项工作中，我们考虑了没有动态创建线程的程序，即，具有递归过程但只有固定数量的通信线程的程序。在本文中，我们将我们的工作扩展到更一般的情况下，线程可以动态创建。为此，我们考虑[16]中提出的建模和分析并行程序的方法。在[16]中，一个基于术语重写系统和自动机技术的框架被用于分析没有同步的并行程序。在本文中，我们模拟类似的程序的条款重写规则集，但我们考虑到同步。更确切地说，在我们的模型中，术语集（定义程序的配置）通过以下方式定义：（1）对应的过程常数到控制点，以及对应于（2）顺序合成和（3）类CCS并行合成的合成操作符。（在顶层还需要限制运算符，以禁止同步动作之间的交错。）然后，我们考虑的基本问题是，给定两组配置（项集）T1和T2，计算从T1中的配置到T2中的某个配置的计算路径集P aths（ T1， T2）的表示。(This通过检查该集合的空性，特别地（但不仅如此）允许解决可达性问题由于结果的不可判定性如上所述，通常不能精确地计算该集合。因此，我们的目标是定义一个通用的方法（在我们以前的工作的精神[5]中提到的），用于有效地计算路径集合P路径（T1，T2）的抽象A（本文提出的方法包括：（1）描述集合P路径（T1，T2）作为约束系统（在路径上）的最小解，A. Bouajjani等人理论计算机科学电子笔记138（2005）153155语言），以及（2）定义一个统一的框架（基于抽象解释[11]），用于计算（以通用的方式）该约束系统的最小解的抽象。我们给出了一些抽象的例子，这些抽象可以自然地用于程序分析，并且可以被定义为我们框架的实例。此外，我们说明了我们的技术的适用性和使用这些抽象的并行算法的一个例子，计算最小值（任意长度）的输入流相关工作：关于并发程序的静态分析有几个作品（参见[25]的调查）。在[2，12]中，分析技术被定义为没有过程调用的多线程程序（线程是有限状态通信系统）。这些技术都是基于解决覆盖问题的Petri网。这种方法在[17]中使用具有转移转移的Petri网推广到具有广播通信的程序。程序分析的自动机方法已经在[15，14]中用于有过程的程序（没有并发性）。这些工作是基于计算下推自动机中的可达配置[4，18]。这种方法已经在[21，16]中扩展到具有动态创建进程但没有同步的并行程序，使用称为PA进程的模型进程重写系统。在[7，8]中，我们将这种方法扩展到允许过程返回值的更大类的过程在[5]中，我们使用路径抽象来分析并行递归程序（具有同步）。在那篇论文中，我们使用通信下推自动机作为程序的形式化模型，并基于我们的基于自动机的下推自动机可达性分析过程建立上下文无关路径语言的抽象[4，14]。在[19]中提出了一种不同的方法，用于分析带有使用路径语言抽象的过程的并行程序。在[26，22]中，定义了与我们在这里提出的方法类似的方法。 在 在这两篇论文中，作者定义了表征计算路径集的约束集。然而，这些特征在技术上与我们的不同，并且考虑更受限制的设置。(1)这些工作考虑的问题，计算抽象的路径集从一个单一的初始配置开始的所有可达配置的集合，而在我们的方法中，初始配置和目标配置的集合可以是任何正规的配置集。这使我们能够以统一的方式处理各种性质的分析问题。(2)[26]中的工作（如[16]中的工作）没有考虑同步，而我们工作的目的是考虑动态创建过程156A. Bouajjani等人理论计算机科学电子笔记138（2005）153和过程调用。最后，（3）[22]中的工作集中在一个特定的数据流分析问题（常数检测），而我们的方法旨在统一处理安全属性。还必须说，我们为更一般的设置付出了代价，即我们的某些抽象的更高复杂性另一项考虑在动态创建线程和过程的情况下对并发程序进行抽象分析的工作是[13]。本文提供了一个（特设）的近似分析，以确定哪些语句可以并发执行。我们认为，这项工作中使用的近似值可以在我们的框架中措辞，但需要对我们的两种方法进行仔细比较。最后，在[23]中，过程摘要用于表示执行过程的结果。该方法适用于具体的多线程程序（不需要抽象分析算法仅保证在某些特定情况下终止。2同步PA系统我们引入了一个基于进程代数的递归调用多线程程序模型，它是PA [1]同步动作的扩展。2.1语法令Lab ={a，b，c，.. . }是一组可见的动作。设Sync和Async是两个不相交的集合，使得Lab=SyncAsync。我们假设对于每个动作a∈Synccc，在Sync中有一个动作a <$，使得a <$=a。 因此，Sync是所有同步动作的集合，即，必须执行的操作同时在两个并行过程之间的“握手”中具有它们相应的共同动作设Act=Lab{τ}是所有动作的集合，其中τ是一个特殊的内部动作（正如我们将看到的，这个特殊动作将代表握手）。令Var ={X，Y，.. . }是一组过程常数。然后，我们将T定义为由下式给出的过程项tt：：= 0 |X|t·t|特什特直观地说，0是空闲或终止的进程（也称为空进程），而“。“（resp. “平行组合）。受限过程项的集合被定义为Tr ={t\Sync|t∈ T }。术语给定一组过程项T，令T\Sync表示A. Bouajjani等人理论计算机科学电子笔记138（2005）153157一12≡≡w∈Act一{t\Sync|t∈T}。定义2.1同步PA系统（简称SPA）是一个有限集一R的规则的形式X<$→t，其中t∈T和a∈Lab。2.2语义2.2.1条款的结构等效性项 被 认 为 是 模 等 价 的 ， 其 对 应 于 代 数 性 质 ： nutrali yofthenullprocess“0”w。室温“·“和”“，”·“和”“的默认值，以及”“的默认值 。 我 们 还 考 虑 了 T 上 的 等 价 关 系 φ0 对 应 于 0 的 性 质（neutralityw.r.t.“·“和““）。通过考虑t\SynctJ\SyncittJ，将上述等价扩展到Tr的项。设是集合{=，}的等价，其中=表示项之间的恒等式设t∈Tr，我们用[t]表示过程项t的模等价类， 即， [t]={tJ∈ Tr|t tJ}。一个项集L被称为是相容 的，如果[L]=L。2.2.2转换关系和计算：SPAR在T Tr上诱导跃迁关系→，定义为：aaJaJθ1：X<$→t2∈R;θ2：t1→t1;θ3：t1<$00，t2→t2X→at2t1·t2→atJ·t2t1·t2→at1·tJaJaJ阿杰阿θ4：t1→t1;θ5：t1→t1;t2→t2;a∈Sync;θ6：t1→t2;a∈/SyncaJτJJat1t 2→t1t 2t1t2→t1t2t1\Sync→t2\Sync一每个等价<$∈ {=，<$}在T <$Tr上导出一个转移关系→<$：t，tJ， t→a tJiuJ和uJtJ这种关系以通常的方式扩展到函数序列。F或如果t∈TT，则letPost[w]（t） ={tJ∈TT|t→wtJ}，令r≡r≡Post（t）=Post[w]（t）。这两个定义被推广到集合w∈Act条款像往常一样。现在，我们还考虑由推理规则θ1，θ2，θ3和θ4定义的T上的弱转移关系θa（即，同步和限制规则被忽略）。这种关系定义了SPA过程的语义，它正是PA过程的语义。 如上所述，我们还考虑了由以明显的方式定义的等价物引起的不确定性，我们定义对于每一项t∈T，WPost ∈[w]（t）={tJ∈T|t<$wtJ}和WPost<$（t）=≡≡≡WPost158A. Bouajjani等人理论计算机科学电子笔记138（2005）153∼给定两组项T，T J<$T <$Tr，从T到TJ的计算路径的集合定义为P aths（T，TJ）={w∈Act <$|<$t∈T，<$tJ∈TJ，tJ∈Post<$[w]（t）}. 当T，T j<$T时，我们通过考虑WPost关系而不是Post关系来类似地定义集合W P aths（T，T j）。2.3SPA作为多线程程序2.3.1从程序到SPA系统：由并行流图系统表示的程序（参见例如，[16，26，22]）可以直接转化为SPA系统。(We通常假设无限数据类型已经使用抽象解释的标准技术被抽象为有限类型图中的节点（对应于程序中的控制点，加上局部变量的抽象值）由过程常数表示，程序的动作是模的。一通过过程项重写规则来提取形式X<$→X1·X2的规则 一对应于过程调用，形式为X <$→X1<$X2的规则对应于以决定所有并行程序的执行情况。Complementaryactionsa，aèare用于模拟并行进程之间的同步（它们对应于send（a！）并接收（a？）声明）。因此，我们认为同步化算子集Sync是集合t{a，a′|a是通信ch annel}。程序的初始配置由T中的过程项的集合T表示。程序的行为对应于其SPA模型R的计算路径集，从限制项集开始T\Sync，即，路径（T\Sync，Tr）。2.3.2良好的系统：对程序的一个自然要求是，互补的同步动作只能出现在并行进程中（它们永远不能由同一个线程顺序执行）。对于具有固定数量的并行进程的程序，这一要求很容易得到保证。因此，可以认为每一对进程都通过不同的有向通道进行通信。然而，这一要求变得难以保证的情况下，程序与动态创建的进程。在下文中，我们将介绍一个确保这一属性的SPA系统的语法假设R是如上所述的对程序建模的SPA。我们将R与一个依赖图GR相关联，其定义如下。顶点可以是过程常数，也可以是中间顶点（R中的每个规则对应一个顶点）。存在边缘X→a一对于每个规则X <$一Y.对于每个规则X <$ XopX，其中reop∈{·，}，→一个行动→1 2op有三条边X→v、v→X1和v→X2，其中v是新顶点。我们说一个SPA是良构的，如果它满足以下条件：A. Bouajjani等人理论计算机科学电子笔记138（2005）15315921≡≡对于每两个过渡u1→u和v→av2在GR中，每个简单路径在对应于GR关联u1和v1的无向图必须包含一个边标记为“”。很容易检查格式良好的系统是否满足互补同步动作永远不能执行通过同样的顺序过程。引理2.2如果R是一个良型集对集，则对于T中的每一项t和tJ，我们有：tJia∈Sync，taa<$TJ我们在第6.2节中考虑一个并行算法的例子，它计算输入流的最小值，并展示如何将其转换为格式良好的SPA模型。3SPA系统的可达性问题设R是一个SPA系统。我们考虑的问题是，给定两个规则的（有限树自动机可定义，见后面的定义），潜在的无限的过程项集合T，TJT，检查是否：Paths（T\Sync，TJ\Sync）=？中国（1）我们表明，停机问题的两个计数器的机器可以减少到这个问题。定理3.1 SPA系统的可达性问题是不可判定的。证明：我们编码了两个计数器机器的停机问题。这种归约类似于[3]中用于证明PA系统的模型检验LTL的不可判定性的归约。设M是一个有m条指令的双计数器机器。让• Var ={X，Y，X1，X1，X2，X2}<${Xc|1 ≤i≤ m}，1 2 1 2i• Sync={i1，i2，<$i1，<$i2，d1，d2，d<$1，d<$2，z1，z2，z<$1，z<$2}，• 异步={halt，a}。设R是具有以下规则的集对分析，其中j∈ {1， 2}且k∈{1，.， m}：一(i)X <$ X1||X2||Xc，（二）→jzj1 1 1Xj，X1 <$→ 1（三）jijXj·Xj，X1<$→ 2 1（四）jijXj·Xj，X2<$→ 2 2一160A. Bouajjani等人理论计算机科学电子笔记138（2005）1531∼DJX2 <$→c'ijc(vi) Xk<$→Xh，如果（sk：cj：=cj+ 1; gotosh）是指令，cz<$jccd<$jc(vii) Xk<$→Xh1和Xk<$→Xh2，如果存在以下四种情况：（sk：ifcj=0，然后转到sh1elsecj：=cj−1;转到sh2）哈勒特(viii) Xm<$→Y。直观地说，过程变量Xj表示计数器j，并且具有n个Xj的项Xj···Xj·Xj2 2 1 2柜台j。第二个规则模拟计数器cj的相等性测试到0，第三和第四规则模拟cj的递增，而第五规则模拟cj的递减。最后三条规则模拟了机器的有限控制最后一条规则模拟机器的停止actinsij和atij表示cj的 增 量。同步化在这两个共同作用之间，只有在控制器允许的情况下。同样的直觉也适用于其他行动，其中redj和d′j表示cj的递减，而dzj和z′j表示c j的零。那么很明显，M停止i，Post（X\Sync）L\Sync/=，其中L是形式为t1的项的集合||t2||其中tj是以下形式的项：Xj···Xj·Xj表示计数器j的值。Q2 2 1由于这种不可判定性结果，为了解决问题（1），我们采用基于抽象的方法，包括像往常一样检查更强的条件，即，检查比P路径（T\Sync，TJ\Sync）更大的集合的空性我们的方法的独创性在于，它允许以一种通用的方式来考虑几种抽象。为了解释我们的方法，我们需要重新表述上面的问题（1） 这是一个简单的选择，Paths（T\Sync，TJ\Sync）=Paths（T，TJ）<$（Async<${τ}）<$，因此，求解（1）等价于检查是否Paths（T，TJ）<$（Async<${τ}）<$=？中国（2）此外，对于良型SPA系统类，引理2.2意味着A. Bouajjani等人理论计算机科学电子笔记138（2005）153161=W=（2）检查是否ΣWP aths（T，TJ）（Asynca∈Syncaa<$）=？中国（3）由于SPA的可达性问题是不可判定的，所以P路径（T，TJ）和WP路径（T，TJ）都不能作为任何可判定的词自动机或文法类的对象有效地计算.因此，我们解决的问题是如何计算路径语言P aths（T，TJ）和WP aths（T，TJ）的抽象，即，集合P aths（T，TJ）的上近似A（T，TJ）（re sp. WPaths（T，TJ）），使得集合A（T，TJ）的顶点s∈（Async），{τ}）n（re sp. A（T，TJ）（Asynca<$））可以决定。a∈ Sync我们定义了一种通用的方法来计算集合P aths（T，TJ）和WP aths（T，TJ）的抽象，• - 将P aths（T，TJ）和WP aths（T，TJ）中的每一个表征为词语言上的约束系统的最小解（该解不能如前所述一般地计算），以及• 计算抽象域中约束系统的最小解以获得P路径（T，TJ）或WP路径（T，TJ）的上近似注3.2我们将在后面看到，上面的两个公式（2）和（3）导致互补的分析方法：它们允许考虑具有不可比较的精确度的不同抽象（见注5.1）。接下来，我们假设TJ是一个相容集.在这种情况下，可以证明，集合P aths（T，TJ）和WP aths（T，TJ）可以在不考虑结构等价性的情况下条件：命题3.3<$T，TJ <$T，如果TJ是相容的，则（W）P aths（T，TJ）={w ∈ Act|（W）Post[w]（T）<$T J/=<$}。证明：包含项是直接的。 对于另一个方向，它表面上显示通过归纳，|W|如果u→ <$uJ，则存在uJ<$uJ，使得u→wuJJ. 这是由于重写的过程一直在进行中树的叶子（术语可以看作二叉树，更多信息请参见第4详细信息）。Q基于上述命题，我们可以提供（W）P路径（T，TJ）的一个特征，作为一组约束（在有限集合上）的最小解。162A. Bouajjani等人理论计算机科学电子笔记138（2005）153话）。这组约束是从两组给定的项T和TJ的有限树自动机表示中构建的。下一节将详细介绍这一特性。4描述路径语言4.1进程树自动机T中的项可以被看作是二叉树，其中叶子用过程标记，而内部节点用二进制操作符“·“和”“来标记。因此，T中的过程项的规则集合可以通过一种称为过程树自动机的有限底树自动机来表示，定义为：如下所示定义4.1过程树自动机是一个元组A=（Q，V ar，F，δ），其中Q是一组有限状态，V ar是一组过程常数，FQ是一组最终状态，δ是一组规则，形式为（a）f（q1，q2）→q，（b） X→q，或（c）q→QJ，其中X∈Var，f∈ {λ，·}，且q1，q2，q，QJ∈Q。在续集中，一项的形式t1·t2（resp. t1<$t2）也将由y·（t1，t2）（resp）表示。 n（t1，t2））。 让它成为一个程序员。A上的一个节点以自下而上的方式定义根据规则（b），则继续对项t的注释根据规则（a）和（c）：如果子项t1和t2分别由状态q1和q2注释，并且如果规则f（q1，q2）→ q在δ中，则项f（t1， t2）由q注释，其中f ∈{q，·}。 一个项t被状态q ∈ Q接受，如果A到达t在q中的根。 设Lq为可接受的项集在Q。 自动机A接受的语言是L（A）={Lq|q∈F}。一组过程术语如果被过程树自动机接受，则它是正则的在[9]中，正则过程树语言的类在布尔运算下是封闭的。此外，过程树自动机的空性问题在线性时间内是可判定的。4.2流程组成与执行路径组成为了表征执行路径的集合，我们需要将操作符“·“和”“关联起来，以便对执行路径上的操作符进行验证让我们从顺序合成的例子开始。很容易证明：引 理 4.2 对 于 每 个 u1 ， u2 ， v1 ， v2∈ T ， 和 每 个 w∈Actn ， 我 们 有 ：u1·u2∈Post[w] （ v1·v2 ） iw1 ， w2∈Actn ， 使 得 w= w1w2 ， u1∈Post[w1]（v1），u2∈Post[w2]（v2），且u1∈0，或w2=0。A. Bouajjani等人理论计算机科学电子笔记138（2005）153163=21一21根据我们与并行运算符关联的语义，我们必须考虑路径上的两个不同运算符。对于“强”语义，我们引入一个操作符“|||“归纳定义如下：ϵ|||w = w|||n = waw1|||a<$w2）+ a <$（a w1|||w2） |||w2) +τ(w1|||w2)aw1|||bw2）+ b（a w1|||bw2) +b(aw1|||w2)ifb a¯引理4.3对于每个u1，u2，v1，v2∈ T，和每个w∈Actn，u1w1，w2∈Actn，使得w∈w1|||w2,u1∈Post∗[w1](v1),andu2∈Post∗ [w2](v2).证明：让我们首先考虑从左到右的蕴涵。 设u1，u2，v1，v2∈ T，且w∈Act，使得n（u，u）∈Postn[w.Σ（v，v）1 2=2.我们通过归纳法继续进行，|W|：• |W| = 0。 则w = 1，并且该性质保持w1= w2= 1，u1= v1，u2=v2。• |W|>0，即，w = bwJ，其中b ∈ Act。 那么让uJ，uJ∈T使得1 2n（uJ，uJ）∈Postn[b.（v，v）1 2 =]1 2且n（u，u）∈Postn[wJ. （uJ，uj1 2 =]12）. 通过归纳可以得出，两个序列WJ和WJ使得WJ∈WJ|||wJ，u1∈Post[wJ]（uJ），并且1 2 1 2=1 1u2∈Post[WJ]（UJ）. 根据b的性质，有两种情况：=2 2(i) b/= τ。 令v = uJ且v → buJ，令v = uJ且v → buJ。两112=2221=1案件是对称的。例如，假设第一种情况。设w1=WJ和w2=BWJ。很容易看出w∈w1|||w2，u1∈Post[w1]（v1），1 2=且u2∈Post[w2]（v2）.(ii) b=τ。 设a∈Sync，使得v1→=J和v2a'= uJ。康-边w1=awJ所以w2= a'wJ.我们可以看到w∈w1|||w2,u1∈ Post[w1]（v1），u2∈ Post[w2]（v2）.=-我们现在展示另一个方向。设w，w1，w2∈Act，u1，u2，v1，v2∈T使得w∈w1|||w2，u1∈Post[w1]（v1），u2∈Post[w2]（v2）. 我们=0。 =Σ通过感应显示，|w1|+的|w2|证明了，<$（u1，u2）∈Post=[w]<$（v1，v2）：• |w1|+的|w2|= 0。 那么w = w1= w2= w，这个性质成立。• |w1|+的|w2|> 0。 设w ∈ w1|||w2，我们将证明，n（u，u）∈Postn[w.（v，v）1 2 =]1 2u→164A. Bouajjani等人理论计算机科学电子笔记138（2005）1531JB⊥设WJ，WJ，b，和BJ使得w1=BWJ和w2=BJWJ。的情况1 2 1 2w1=（或w2=）是直接的，因为在这种情况下w1|||w2= w2（w1|||w2= w1）。J JbJbJjJ设u1和u2使得v1→=u1，v2→=u2，u1∈Post=[w1]（u1），且u2∈Post[WJ]（UJ）. 有两种情况，取决于b的性质，bJ：(i) BJ=2 2b. 在这个地方，|||w2）+ B J（W1|||w2)+bJ(w1|||wJ). Letthen1 2wJ∈wJ|||W2，使得W = BWJ（其中对于W j，W = BJWJ的情况，w1|||wJ是对称的）。 由于u1∈Post<$[wJ]（uJ），u2∈Post<$[w2]（u2），2=1 1=和|WJ|+的|w2|<|w1|+的|w2|，我们通过归纳得到：∗1J.j- 是 的ΣPost=[w]<$（u1，v2），由此推断<$（u1，u2）∈Post=[w]<$（v1，v2）。(ii) bJ=<$b。在这种情况下，我们有一个|||w2）+<$B（W1|||（wj）|||wJ)+τ(wJ|||wJ)1 2 1 2设wJ∈wJ|||wJ使得w = τwJ（其他情况处理为1 2以前）。 通过归纳，可以得出：n（u，u）∈ Postn[wJ.（uJ，uJ）1 2 =]1 2因此，我们得到了<$（u，u）∈Post<$[w]。Σ规则θsincev→b1uJ和v2¯uJ。=]1（2）应用5 1=12→=2Q在弱语义的情况下（其中，交织对应于没有同步的纯交织），相关联的操作是对字的shu-bie操作HH上面的引理在Post被WPost替换时成立，并且|||被HH取代。4.3（W）路径（T，TJ）的不动点特征：设R是SPA系统，T和TJ是两个正则过程项集，A=（Q，F，δ）和AJ=（QJ，F，δJ）是两个过程树自动机，使得L（A）=T和L（AJ）=TJ.我们假设w.l.o.g. 对 于 每 个 s∈QJ ， t 在 这 里 是 一 个 状 态 s∈QJ ， 满 足 thatLS<$=LS<${t∈T|t<$00}（我们认为s<$=s<$）1然后，让我们考虑刻画P路径（T，TJ）的问题。WP aths（T，TJ）的特征可以完全以相同的方式完成，通过将所有Post替换为WPost，并且运算符|||关于HH[1]这样的状态可以通过A′与自动机的乘积来获得，该自动机识别tems0-equivaleto0的集合。该自动机的规则为：0→q，·（q，q）→q，·（q，q）→q，其中q是自动机的唯一状态，被认为是接受状态。状态s对应于乘积自动机中的（s，q）。A. Bouajjani等人理论计算机科学电子笔记138（2005）153165=1我们通过添加与R中出现的项相对应的状态和规则来引入自动机A和AJ的轻微扩展。 为此，让我们考虑集合QR ={qt|设δR为规则的集合：（1）X→qX，若qX∈QR，对任意yX∈Var，（2）<$（qt1，qt2）→qt，若t=<$（t1，t2）andqt∈QR，andnd（3）·（qt1，qt2）→qt如果t=·（t1，t2）且ndqt∈QR.很容易确定，对于R中的每个子项映射，Lqt={t}。现在，令Q = Q<$QR，<$j = δ <$δR，Q J= QJ<$QR，且<$J= δJ<$δR。然后，给定两个状态q∈Q和s∈ QJ，我们定义路径集λ（q，s）={w ∈ Act|后[w]（Lq）LS{\fn方正黑体简体\fs18\b1\bord1\shad1\3cH2F2F2F}.显然，集合λ（q，s）的计算允许定义P路径（T，TJ），因为根据命题3.3，这个集合是所有λ（q，s）的并集，使得q∈F且s∈FJ。4.3.1一组约束：我们在下文中定义了路径语言的一组约束，并证明了它精确地刻画了集合λ（q，s）。让我们考虑一组变量（代表路径集），定义如下：对于每个状态q∈Q，状态s∈ QJ，我们定义一个变量V（q，s）。然后，我们考虑以下集合限制：（β1）IfLqLS/=L，thenn∈V（q，s）（β2）若q1→q2是n的规则，s1→s2是N的规则，则V（q1，s1）<$V（q2，s2）（β3）If·（q1，q2）→q是f∈j的规则，·（s1，s2）→s是f∈J的规则，则nV（q1，s）V（q2，s2）<$V（q，s）并且，如果Lq2<$LS2/=<$，则V（q1，s1）<$V（q，s）（β4）如果<$（q1，q2）→q是<$j的规则，<$（s1，s2）→s是<$J的规则，则V（q1，s1）|||V（q2，s2）<$V（q，s）一（β5）若X <$→t∈R，则V（q，qX）aV（qt，s）<$V（q，s）166A. Bouajjani等人理论计算机科学电子笔记138（2005）153=∗4.3.2正确性：我们证明了：（i）前一组约束的最小解存在，（ii）这个解精确地对应于集合λ（q，s）的定义。命题4.4约束集（β1）-（β 5）的最小解存在。事实上，让x1，.，x，m是变量V（q，s）的任意编号，q∈Q和s∈QJ。则系统（β1）fi（x1，.，xm）<$xi，1 ≤ i≤ m（4）其中fi（x1，.，xm）是由变量x i和字连接运算符建立的函数，|||，和。（注意，形式为e1xi和e2xi的两个不同的内含物可以被内含物代替。 e1e2xi.）令X =（X1，...，xm），并且F是使得.ΣF（X）=f1（x1，...，xm），.，fm（x1，.，xm）。（4）的最小解是F的最小预定点。 设L是Act上语言的完全长度，即：，L=（2Act，λ，Actλ）. 可以看出，运算符·和|||是连续的。 由此可以得出F是单调的和连续的。因此，根据塔斯基定理，F的最小预定点存在，并且等于它的最小定点，根据克莱因定理，这个定点等于：Fi（m， . . ，J.）。（五）i≥0定理4.5设.L（q，s）Σq∈Q，S∈QJ是系统（β1）（β5）。然后，对于每个q∈Q和每个s∈ QJ，我们有L（q，s）= λ（q，s）。证明：我们证明，对于每个q∈Q和每个s∈ QJ，Post[w]（Lq）<$LS/=<$惠w∈L（q，s）.我们从隐含意义开始。设q∈ Q，s∈QJ，w∈Act，u∈Post[w]（Lq）LS. 设v∈Lq使得u∈Post[w]（v）。 我们继续=-通过归纳，|W|.• |W| = 0，则w = φ，且u ∈ Lq<$LS，这意味着φ ∈ L（q，s）（from（β1））。• |W|>0。 有两种情况：A. Bouajjani等人理论计算机科学电子笔记138（2005）1531671=11===一(i) V的根被重写了。 设X <$t∈R，w，w∈Act使得→1 2X∈Post<$[w1]（v），u∈Post<$[w2]（t），=-且w=w1aw2。以来|w1|<|W|和|w2|<|W|归纳假设的结果是：w1∈L（q，qX），w2∈L（qt，s）.因此，我们从（β5）得到：w=w1aw2∈L（q，qX）aL（qt，s）<$L（q，s）(ii) V的根没有重写。 我们继续进行结构归纳，u：(a) v=·（v1，v2）andndu=·（u1，u2）suchthatv1∈Lq1，v2∈Lq2，u1∈LS1，u2∈Ls2，其中re·（q1，q2）→q是f的规则，·（s1，s2）→s是f的规则因此：*U1 等 于 0 ， 即 ， u1∈Ls<$.L emma4.2 推 断 出 存 在 eistw1 ，w2suchthatw=w1w2，u1∈Post[w1]（v1），u2∈Post[w2]（v2）. 通过结构归纳法，我们有w1∈ L（q1，s2）和w2∈ L（q2，s2）. 我们然后由（β3）得到，w= w1w2∈ L（q1，s<$）L（q2，s2）<$L（q，s）.*u1不等于o0，它满足eu2=v2∈Ls2<$Lq2和u1∈Post[w]（ v1）. 通过结构归纳法，我们得到w ∈ L（q1，s1），通过（β3），我们得到，w∈L（q1，s1）<$L（q，s）.(b) v=n（v1，v2）和u=n（u1，u2）。引理4.3推断存在w1，w2使得w∈w1|||w2，u1∈Post[w1]（v1），u2∈Post[w2]（v2）. 让=-q1，q2∈ Qsuchthatu（q1，q2）→q是f的规则，v1∈Lq1，且dv2∈Lq2.此外，设 s1， s2∈ QJ，使得<$（ s1， s2）→s是<$j的规则，使得u1∈LS1，u2∈LS2. 然后，通过结构归纳法，我们推断出w1∈L（q1，s1）和w2∈L（q2，s2），并且由于（β4），我们得出：w∈ w1|||w2L（q1，s1）|||L（q2，s2）<$L（q，s）.考虑另一个方向。设w∈L（q，s），我们证明了Post[w]（Lq）LS/=100。从那以后。用饱和度方程重新构造了elsL（q，s），当L0（q，s）=0，Ln（q，s） =L（q，s）时，满足r个等式s，Li（q，s）0≤i≤nLi（q，s）是第i次迭代后得到的标号 我们通过归纳法证明了：如果w∈Li（q，s），则nPost<$[w]（Lq）<$LS/=<$. 当i=0时，这是直接的。对于i= 1的情况也是如此设i >1。设w∈Li（q，s），则：168A. Bouajjani等人理论计算机科学电子笔记138（2005）153==1====11==22• 或者存在（qJ，sJ）使得w∈Li−1（qJ，sJ），且Li−1（qJ，sJ）<$Li（ q， s） （ 规则 β2） 。 在这 种 情况 下 ， 我 们必 然 有 QJ→q∈N 和SJ→s∈N，并且ndheLqJ<$Lq，ndLSJ<$LS。通过归纳，Post[w]（LqJ）。它遵循Post[w]（Lq）<$LS=/since LqJ<$Lq和LSJ<$LS。•要么存在w1，w2使得w=w1w2，要么存在q1，s1，q2，s2suchthat·（q1，q2）→q∈N，·（s1，s2）→s∈NJ，w1∈Li−1（q1，sN），w2∈Li−1（q2，s2），w∈Li（q，s）（规则β3）. 通过归纳，我们得到：Post[w1]（Lq）L和=1S1Post[w2]（Lq）Ls.=2 2设u1和u2，u1∈Post<$[w1]（Lq）<$LS<$和=11u2∈Post<$[w2]（Lq）<$LS.=2 2很明显，（由于u1=0）·（u1，u2）∈Post <$[w]（Lq）<$LS• 或者ex是tq1，s1 ，q2 ，s2suchthat·（q1 ， q2 ）→q∈N， ·（s1 ，s2）→s∈NJ ， w∈Li−1 （ q1 ， s1 ） ， 且 Lq2<$LS2/=N （ 规 则 β3 ） 。设u2∈Lq2<$LS2. 如果cew∈Li−1（q1，s1），则由归纳法得出存在u1∈Post[w]（Lq1）<$LS1。我认为这是一个很明显的事实，·（u1，u2）∈Post<$[w]（Lq）<$LS.• 或者存在w1，w2使得w∈ w1|||w2，存在q1，s1，q2，s2使得<$（q1，q2）→q∈ <$，<$（ s1， s2）→s∈ <$J， w1∈Li−1（ q1， s1）， w2∈Li−1（ q2， s2）（规则β4）。通过归纳，我们得到：和后[w1]（Lq）后LS/=0后[w2]（Lq）后LS/=0。设u1和u2使得u1∈Post<$[w1]（Lq）<$LS和u2∈Post<$[w2]（Lq）<$=1 1=2LS2。我们从Lemma4.3获得，<$（u1，u2）∈Post<$[w]（Lq）<$LSA. Bouajjani等人理论计算机科学电子笔记138（2005）153169===∗∗• 或者存在规则X一<$→t∈R，w1，w2使得w=w1aw2，w1∈Li−1（q，qX），w2∈Li−1（qt，s）（规则β5）. 通过归纳，我们得到：X∈Post<$[w1]（Lq）且存在u∈Ls使得u∈Post[w2]（t）.很明显，u∈Post[w1aw2]（Lq）.Q5抽象路径语言系统（4）的最小解的迭代计算（5）一般不终止（因为可达性问题对于SPA是不可判定的）。如前所述，我们的方法不是计算精确的语言λ（q，s），而是计算它们的抽象。为了描述这些抽象，我们定义了一个基于抽象解释的形式框架[11]。5.1一个通用框架LetL是语言相对于行为的共同点，即：，L=（2Act），，Act）。例如，一个牵引力要求一个牵引力长度D=（D，±，H，H，H，T），其中D是某个抽象域，L和D之间有一个Galois连接（α，γ），即，一对映射α：2Act→D和γ：D→2Act，使得<$x∈2 Ac t<$，<$y∈D. α（x）±y<$$>x<$γ（y）。在我们的框架中，H是结合的，交换的，幂等的。我们还假设这个算子可以扩展到可数的有限集合（即，可数无限连接也是D的元素）。此外，我们认为两个抽象transcterationsA和B，并定义如下的元素：A和B是A的中性元素，A和B是H-连续体。注意，这个等式意味着（D，H，1）是幂等闭半环。直观地说，D的抽象运算H、n和n对应于联合、连接和单词并行组合（|||或HH，取决于170A. Bouajja