抽象加速方法在数值输入数据流程序中的可达性分析

理论计算机科学电子笔记267（2010）101-114www.elsevier.com/locate/entcs抽象加速方法在数值输入数据流程序中的Peter Schrammel1，2 and Bertrand Jeannet3INRIARhone-Alpes，Grenoble，France摘要在计数器模型的可达性分析中，加速方法常用于精确计算循环的效应。将这些方法应用于同步数据流程序，布尔和数值变量，例如 LUSTRE程序，首先需要枚举布尔状态，以便获得仅具有数值变量的控制图。第二，加速方法必须处理由数值输入变量引入的非确定性。 在这篇文章中，我们解决后一个问题，通过扩展Gonnord等人的抽象加速概念。数值输入变量。关键词：静力分析，加速度，抽象解释，线性关系分析。1介绍本文考虑了操作布尔变量和数值变量的同步程序的可达性分析，更一般地说，逻辑-数值程序的一种，它是结合了布尔变量和数值变量的符号自动机。这种可达性分析的应用例如是安全特性的验证[16]或基于模型的测试[19]。摘要解释和加速度以来 的 达性 问题是不可判定的逻辑数值程序，两个主要的方法已经研究：(i) 抽象解释技术[6，7]仅计算可达集的过近似，但总是终止(ii) 加速技术[21，2，3]在有利的情况下计算精确的可达集，但不保证终止。1这项工作得到了INRIA大规模倡议“科学”的支持。2电子邮件：peter. inrialpes.fr3电子邮件：bertrand. inrialpes.fr1571-0661 © 2010 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.09.009102P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）101∪Hτ=图1.一、简单循环转换（左）和加速转换（右）。在这两种方法中，可达状态的集合通过迭代求解形式为X=X0post（X）的方程来获得，其中X是状态的集合，X0是初始集合，并且post是与程序相关联的后置条件运算符。抽象解释是分析无限状态空间程序的经典方法。其关键思想是用抽象域的元素Y来近似状态X的集合。数值不变量X∈P（Rn）的一个经典抽象域是凸多面体Pol（Rn）[9]的域，它可以表示为线性不等式的一个连接. 计算可达集的近似值 通过在抽象域上迭代求解方程Y=Y0post（Y 为了确保当抽象域包含无限递增序列时的终止，应用了称为加宽的外推算子，这会导致额外的近似。加速的思想是加速程序控制结构中的循环τ，通过计算它们的传递闭包τ对一组状态的影响，参见图1。如果程序是可加速的（即它不包含嵌套循环），并且所有循环都可以加速，那么该方法是完整的。如果程序包含嵌套循环，则该方法是半完备的：开始枚举和加速非初等循环（形成无限集合），希望在有限步之后收敛到最小的不动点。如果某些循环中的转换函数表达能力太强而无法加速，则也适用相同的注释。 加速主要应用于使用Presburger算法[12，11，2]或使用正则表达式子类的FIFO队列[4，1]来操作整数变量的自动机。加宽基本上是在不涉及生成它们的程序的情况下推断抽象不变量序列的极限，而加速使用 程序的结构来执行精确的外推。Gonnord等人[15，14]提出了抽象加速的概念，它结合了这些方法：只要有可能，基本循环在抽象域中加速，在任何其他情况下（嵌套循环，太有表现力的转换），都可以使用加宽来保证近似不动点计算的收敛性。抽象加速与逻辑数值程序。 加速技术，如[21，2]考虑纯数值自动机。当应用于逻辑-数值程序（如LUSTRE[5]数据流程序）时，抽象加速方法有两个简短说明：(i) 为了将这样的程序简化为纯数值自动机，需要在控制图中枚举和编码布尔状态变量的所有可能的赋值。这种划分和部分评估过程可能导致Cc′τc′′P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）101103、k−→k控制位置的组合爆炸(ii) 在LUSTRE程序中遇到的输入变量的概念需要[15，14]的结果的扩展。与可以通过有限的非确定性选择在自动机中编码的布尔输入变量相反，数值输入变量需要更具体的处理。这篇文章特别讨论了第（ii）点，尽管第（i）点是我们的最终目标。贡献和大纲。 我们的贡献是将[15]中引入的抽象加速度概念扩展到具有数值输入的系统，这提出了一些微妙的观点。特别是，我们将展示如何加速循环组成的翻译与复位和输入，提供的警卫的循环约束分别状态和输入变量。如果没有这个限制，我们就可以在没有输入的情况下模拟出任何一个阿洛涅变换。在第2节中对所考虑的程序模型、凸多面体上的运算和我们用于分析的一般验证框架进行了一些初步的概念之后，我们回顾了第3节中抽象加速的主要结果。第四节详细介绍了我们的贡献。我们在第6节结束。2逻辑-数值程序分析程序模型。在这篇文章中，我们考虑将程序建模为一个符号转换系统初始化assert（s，i）→s=f（s，i）其中（1）s和i是状态和输入变量，它们或者是布尔的或者是实数的;（2）init（s）是状态变量上的初始条件;（3）assert（s，i）是依赖于状态变量约束输入变量的断言，并且通常对程序的环境（4）f是转移函数的向量。这样一个系统的执行是一个序列sis1i1... skik... 等初始化（s0），对于nyk≥0，断言（sk，ik）<$sk+1−→=f（s，i）。−→例如，该程序模型对应于前端编译同步数据流程序，如LUSTRE，并包括计数器自动机的各种模型（通过使用布尔变量模拟位置）[3]。通过对所有布尔状态变量（然后在控制位置中编码）执行部分评估[20]并通过非确定性选择消除布尔输入变量，可以从该程序模型生成仅操纵数值变量的控制图。在NBac工具[18]中实现的分区细化机制能够实现这一任务，并且已经用于将ASPIC工具[14，13]连接到LUSTRE。凸多面体。本文用凸多面体的抽象域表示数值变量的不变量除了经典的操作（相交，凸包，分配变量的线性表达式，。. .）描述的，例如： 在[17]中，我们将使用以下操作：104P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）101⊇→≤3.|∈}≤定理3.1Letτeatanslat.离子G→xs=x+d。Thecovenvexpolyhedron→时间流逝操作[17] XD=x+td xX，dD，tR≥0实际上是这样实现的：设（VX，RX）分别为（VD，RD）是多面体X和D的生成元系，则（VX，RX<$VD<$RD）是多面体X3 D的生成元系.的 Minkowski 总和 [10个国家] 的 两 多面体 X=X1+X2是 已定义 作为X（x）=x1，x2：（x=x1+x2）<$X1（x1）<$X2（x2）。3加速和抽象加速概述正如在引言中提到的，加速的思想（图1）是用计算τ的传递闭包的单个转换τ代替循环转换τ。抽象加速度[15，14]放松了精确加速度，因为它旨在通过其凸包τ（X）τ（X）来近似精确集τ（X 这种方法也受到了时间或混合自动机中使用的时间流逝算子的启发[17]。按照第2节的符号，循环转换τ将具有结构：G A，意思是通常，数值变量x的加速方法处理以下形式的转换：Ax≤b→x=Cx+d（1）其中，Ax b表示定义凸多面体的线性约束的合取，并且x∈=Cx+d是一个正交变换;C是一个平方矩阵。一个过渡被称为• 如果C是零矩阵，则复位• 如果C是单位矩阵，• 如果C是仅具有0和1的对角矩阵，则具有重置的平移• 周期性的α变换，如果αp>0：Cp=C2p，• 一个一般的阿洛尼变换。现有的加速方法不能处理一般的代数变换。我们将不讨论周期性阿洛涅变换的情况，因为它的实际意义似乎有限。在抽象加速的背景下，[15，14]表明平移（图2）和重置平移（图2）。 3）可以如下加速，其中X表示凸多面体，G（x）=（Ax b）是一个凸多面体（也是凸多面体）：τ（X）=XH。（XHG）3d<$HG（x−d）是τ（X）的凸过应用肟化。定理3.2设τ是一个带重置Gxs= Cx + d的平移.凸多面体P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）1011052D2GXXD11--≤→. .ΣΣ0JyKyDdG（x−d）xXd2GCd）图二.从X（暗阴影）开始的平移循环的加速导致τ（X）（整个阴影区域）。图三.具有平移/重置的循环的加速：在左手边，τ（X）的应用-在这里，x j 1 = x 1 + d 1和x j 2 = d 2，产生包含重置值的多面体（包括箭头的粗线）。在ue加速跃迁在右手边给出τ（Sτ（X）=XHτ（X）H（τ（X）HG）3CdHG（x−Cd）是τ（X）的凸过应用肟化。注3.3定理3.2利用了一个性质，即一个重置为常数的平移迭代N次，等价于一个重置为常数的平移后的纯平移迭代N-1次，因此得到了这个公式。注3.4理想情况下，定理3.1和3.2中定义的τ（X）应该是凸多面体对τ（X）的最佳过逼近。这不是如以下一维示例所示的情况。设X=[1，1]且τ：x14x=x1+2。 τ（X） =[1，6]，而τ（X）= 1，3，5的最佳近似是区间[1，5]。这是因为，τ（X）操纵稠密集，不考虑算术同余。我们不会在本书中改进这一点，但我们会在证明中指出这种稠密近似发生的地方这些定理可以通过用单个自循环划分位置来应用于控制图（如图1所示）。如果在一个位置中有几个自环，则必须区分保护重叠和不相交的情况，这导致位置的更精细的划分。[14]给出了一系列处理更复杂情况的方法。4数字输入我们现在扩展数值抽象加速度w.r.t.数值输入变量y。这意味着我们考虑形式的转换.AL.x≤。b→xs=.CT.x+u（二）`Ax+Ly≤bJy≤kx`Cx+Ty+ux注意，保护矩阵中的0并不意味着失去一般性。一个基本的观察是，任何没有输入Ax≤b→xs=Cx+d的一般的代数变换都可以表示为“有输入的重置”（Ax ≤b）。GD1XD1G（x−106P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）101∧→≤ ∧≤.中国（ ）=H（H）3.j=1吉尔吉克⎩- ≥≥⇒这是由Y定义的。一个零分。x≤。b→xs=.IT.x+u其中I是.- 是的Σ惠xss∈..（XHG）3D<$HG，<$ds∈D：xs=xss+dsb y=Cx+d）xs=y。这意味着，没有希望获得具有输入的这种重置的精确加速，除非我们知道如何在没有输入的情况下精确地加速一般的高斯变换，这超出了现有技术的范围。然而，当状态变量上的约束不依赖于输入时，即当等式n中L=0时，我们可以用输入加速转换。 （2）且保护区的形式为Ax bJy k。 我们称生成的守卫为简单守卫。另外，我们在4.3节中给出了一般守卫的精确结果4.1带有输入和简单保护的0Jy k y单位矩阵首先，假设在没有输入的平移中，d不是常数，而是被约束在凸多面体D内。定理3.1可以推广到这种多面体平移。命题4.1设τ是一个变迁G→xs= x + d，其中G（x）=（Ax≤b）， d∈D，D是凸多面体。集合T X X T X G D是τ（X）的凸过应用肟化。注意，τ（X）可以通过标准多面体运算来实现： （XHG）+D.证据 在证明中，保护G被看作是一个谓词或集合。xs∈k≥1τk（X）惠k ≥ 1，x0∈ X，d1，.， d k∈ D：⎧⎨xs=x0+ΣkdjG（x0）k∈[1， k−1]：G（x0+惠k≥1，x0∈X，d，dk∈D，xk−1：j=1dj）xk−1=x0+（k−1）d<$G（x0）<$G（xk−1）<$xs=xk−1+dk（因为D和G是凸的）<$xα≥0，<$x0∈XHG，<$d，ds∈D，<$xss：xss=x0+αd<$xs=xss+ds<$G（xss）（稠密近似）惠xs∈.（XHG）3DHG+D最后，我们注意到。（X H G）3D H G+ D = τ（X H G）3D Q注意，唯一的近似发生在线（）中，其中整数系数k1 0被稠密系数α0代替。这是备注3.4的技术说明。P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）101107⎧⎨⎩..3小时{|联系我们HH为Ea CH产生过渡。d∈D，取并集，即计算τ（X）{|∈|{\fn方正粗倩简体\fs12\b1\bord1\shad1\3cH2F2F2F}实施例4.5对照伊德尔波利赫德河在X={（x1，x2）|0≤x1≤x2≤1}，1注4.2人们可能认为定理3.1可以直接应用于加速器。byXH.d∈DXd，其中Xd= （XHG）3d<$HG（x−d），但有一个微妙的差异：这个公式计算G内所有可达状态的正确集合，但是对于跨越G边界的最后一步，它只允许那些已经用于先前迭代的向量d，而实际上在所有状态中有一个选择。d∈D。下面的命题将具有输入的翻译减少为广义翻译：命题4.3带输入和简单保护τ的翻译相当于一个没有输入的多面体平移，Ax≤b<$d∈D→x<$=x+dD={d |n=n = n + n =n注意，D可以通过标准多面体运算来计算。证据xs∈τ（X）惠<$x，<$y：Ax≤b<$Jy≤k<$xs=x+Ty+u惠x，y，d：Jy≤kd=Ty+uAx≤bxs=x+d惠x，d∈D：Ax≤bxs=x+d其中，D={d|y：Jy≤k d=Ty+u}Q定理4.4具有输入和简单保护τ的平移的加速转移ττ可以通过应用命题4.1和4.3来计算。过渡τ：x1+x2≤4→x1=x1+2y−1消除输入.≤y≤. x10 =x2+y在命题4.3中得到D =（d1，d2）1d13 d1+2 d2=1，见图1。还剩4 在将X转 换 为D之 后（图1）。4右）我们得到多面体{（x1，x2）} |x1≥ 0 <$−x1 + x2≤ 1 <$x1 + x2≤ 9 <$−2x1 +4 x2≤ 9 <$2x1−3x2≤ 0}。注4.6与定理3.1类似，我们可以考虑公式X（X G）D）（G + D））。为了证明这一点，我们推广了命题4.1在标签处继续（密集近似）：惠α≥0，<$x0∈XHG，<$d，ds∈D：xs=x0+αd+ds<$G（xs−ds）<$（<$α≥0，<$x0∈XHG，<$d，ds∈D：xs=x0+αd+ds）<$（ds∈D：G（xs−ds））<$xs∈（XHG）3D<$xs∈（G+D）使用x dD G（x d）= z+ddDG（z）=（G+D）.但可以观察到，对于例4.5的翻译，后一公式导致2108P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）101D2X2D1τ（X）1≤kD1G1X1X1≤ ∧−{∈|{\fnSimHei\bord1\shad1\pos（200，288）}{|联系我们 |∈ }0Jk≥yKy是τ（X）的凸过应用肟化。X2Jy1XyG+Dτ（X）G1x1见图4。例4.5：左手边显示了输入的转换：Jy k d=Ty+u（粗线）投影到变量d上。右图中的阴影区域是加速跃迁τ（X）的结果。图五.例4.5中使用根据备注4.6的近似公式时的精度损失。与图4中的结果相比，过度近似（参见图5）。 这反映了证明中额外的近似步骤4.2带有输入和简单防护装置的这是由Y定义的。一个零分。x≤。b→xs=.CT.x+u其中C是a对角矩阵Ci，i∈ {0， 1}。符号。设C=I其中I是IDENTY矩阵。一个向量x可以在x=xt+xr中分解，其中xt=Cx，xr=Cx. Weextendsuch集合符号：Xt= X tXXXr= X RXX. 如果I表示集合 It=i I Ci，i= 1和Ir=I It是平移的集合， 重置尺寸。 任何集合X都可以用闵可夫斯基和Xt+ Xr来近似，它也可以看作是X投影在平移维度的子空间上和X投影在重置维度的子空间上的笛卡尔乘积。这种情况可以用类似于第4.1节的方式来处理：我们结合Theo-rem3.2和命题4.3将有输入的平移/重置减少到没有输入的广义平移/重置。然而，请注意，注释3.3不再适用，并且不能在存在输入的情况下使用，因为被重置的变量可能在每次迭代中被分配不同的值4.7号提案 设τ是具有重置的平移G→xs=Cx+d，其中G（x）=（Ax≤b），d∈D，Dacon.让人烦恼。 TheSetττ（X）=XHτ（X）Hτ。（τ（X）HG）t3Dt+Dr证据 该公式对于0次或1次迭代是平凡正确的，因此，仍然需要表明，对于2次迭代的情况，我们的公式产生了过度近似：.k≥2τk（X）.P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）1011090⎪⎩∧⎩1惠k≥φ2，φx0∈X，φd1. . dk∈D，nx1.. .xk：.. .x∈（τ（X）HG）3D+ DH G+ D惠k≥φ2，φx0∈X，φd1. . dk∈D，nx1.. .xk：k−1⎪k−1⎪⎩k−1G（xk s）{\displaystyleG（xks）2k−10G（x1）k−1<$$>α≥<$0，<$x0∈XHG，<$d1，ds∈D，<$dt∈Dt，<$dr∈Dr，<$xss：j=1JK2xs∈.k≥2τk（X）xs=xk⎨⎪∗xksi=x0i+克·Jdjifori∈It克什蒂尔克⎪∈[1，k]：j=1当i∈Ir时，<$$>G（x）<$$>k<$<$∈[1， k−1]：G（xks）xs=xt+（<$$>G（x）<$$>k <$$> ∈[1， k−1]：G（xt+（<$kJ2dt）+drs）其中，dk≥2，dx0∈dxHG，ddk∈D，dddt. . dt∈Dt，dr.. . Drx1=xt+d1∈Dr，<$><$k <$<$∈[2， k−1]：xks=xt+（<$kJdt）+drs1000万xk：xs=xt+dk1j=2j k（D近似于（Dt+Dr）的和，其中k∈[2， k−1]）其中，惠k≥2，fx0∈XHG，fd1，dk∈D，fdt∈Dt，fdr. . Dr1∈Dr，nx1. xk：x1=xt+d1xs=xtk−1 +dk（因为Dt和G是凸的）<$ x1=xt+d1<$xss=xt+αdt+dr<$G（x1）<$G（xss）0 1xs=xsst+ds（稠密过近似）惠σα≥0，τx1∈τ（X）HG，τds∈D，τdt∈Dt，τdr∈Dr，τxss：xss=xt+αdt+dr<$G（xss）<$xs=xsst+ds惠xss∈. .（τ（X）HG）t3Dt∈HG，τds∈D，xs=xsst+ds最后一个表达式等于τ。.（τ（X）HG）t3Dt+Dr.Q定理4.8具有输入和简单保护τ的平移/重置的加速转移ττ可以通过应用命题4.7来计算，其中D如命题4.3所定义。j=1JK110P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）101例4.9考虑多面体X ={（x1，x2）|0 ≤ x1<$1 ≤ x2<$x1+ x2≤ 2}P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）101111GX1X1⊗.≤12→ .Xx2x21 1见图6。带输入的转换/复位：示例4.9。左侧：τ（X）（暗阴影）和（（τ（X）H G）t）Dt）+Dr（整个阴影区域）。 右侧：τ（τ（X）H G）t）Dt）+Dr）（暗阴影）和τ（X）（整个阴影区域）。和过渡τ： 2 x1+2 x2≤ 701→。 x=x1+y+1。消除输入=y.≤y≤. x10得到D ={（d1，d2）|1 ≤ d1≤ 2 <$d1−d2= 1}和Dt={（d1，d2）|1 ≤ d1≤ 2 <$d2=0}。我们得到τ（X）={（x1，x2）|x1 + x2≥ 1 <$x2≥ 0 <$2 x1−2x2≤ 9 <$2 x1 +11 x2≤ 22 <$x1≥ 0}，见图第六4.3将一般守卫削弱为简单守卫正如第4节开头所讨论的，允许对状态和保护中的输入变量（等式中的L0（2））使加速非常困难。我们解决方案是通过简单guard（或carbohydroproduct）G<$=（y：G）（x：G）并应用定理4.4`AJx≤bsx`JJy≤ksx和4.8。这很容易导致声音过度近似，因为较弱guard用于抽象加速。例4.10考虑多面体X ={（x1，x2）|x1≤ 1 <$x2≤ 1 <$x1+ x2≥ 1}和过渡2x +x+y6（）：22−≤x= x1+y+ 1。 弱化x=x2+1τ Xx y1.0 ≤y ≤ 1。 2守卫是G<$=（2x1+x2≤6<$x1+x2≤4<$x2≤3）<$（0≤y≤1）。消除输入得到D ={（d1，d2）|1 ≤ d1≤ 2 <$d2= 1}。 我们得到τ（X）={（x1，x2）|x1+x2≥1 <$x2−x1≤ 1 <$−4≤ x1−2x2≤ 1 <$x1+ 2 x2≤ 10 <$2 x1+ x2≤ 10}，见图。第七章精 确 结果的凸包是{（x1，x2）|x1+ x2≥ 1 <$−2≤ x2−x1≤ 1<$x1−2x2≤1 <$x2≤ 3 <$2 x1 + x2≤ 10}，见图2。八、5与加宽的凸多面体的标准加宽算子及其改进，如有限加宽[17]4有时可能会导致良好的结果。在本节中，我们将比较例4 - 9和例4 - 10中的加速方法和加宽方法。GX1X1112P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）1014有限加宽也称为带阈值加宽[8]。P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）101113l0τ⊗LLLsp≤20l0τ⊗LLsp≤20LHx2x2G1X 11x11x1见图7。例4.10：使用弱化的保护G（结果被阴影化）的加速转变τ（X）。τ见图8。例4.10：精确结果的凸包（深灰色），我们的方法（灰色），以及无延迟加宽和3（！）递减迭代（浅灰色）τXX Xp=p+1Xp=p+1见图9。 加速度分析（左）以及实施例4.9和4.10图 10.例5.1的加速度分析（左）和加宽分析（右）。分析这样一个在N个初始步骤之后使用加宽的程序，需要计算序列的极限Y0=XZ0=YNYn+1=XHτ（Yn），对于n N Zn+1=Zn（ZnHτ（Zn））其中Xn、Yn、Zn与图9上位置l相关联。加宽算子的技术性质保证序列（Zn）n≥0在有限步内收敛到Z∞[7]，这是位置l处可达赋值的过近似。这个结果可以通过计算序列W0= Z∞，Wn+1= X τ（Wn）的第一个元素来改进，它不一定收敛。带输入和简单保护的如果我们在例4.9的上下文中计算上面定义的序列，我们得到N= 0Z∞= Z1={（x1，x2）|x1≥0}W1={x1≥0<$x2≥1<$x1+x2≥1<$x2≤2}W∞ =W2=τ<$（X）延迟加宽一步（N=1）改进了Z∞的结果，并使序列（Wn）n≥0仅在一步中收敛：Z∞=Z1={x1≥0<$x2≥1<$x1+x2≥1}W∞=W1=τ（X）在这两种情况下，Z∞的精确度明显低于通过加速度获得的结果：x1和x2都没有得到上界（与图1比较）。（六）。114P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）101.0→21 .联系我们τ：.T{|联系 我们，X=（x1，x2，p） - 是的Xx=y≤y≤. p=p≤2μp =1μm∞W1线1∗∞.⎧2一个或两个下降迭代允许得到与通过加速获得的结果相同的结果。然而，应当指出，如果该循环是程序片段，例如嵌入在如图10所示的外部循环中，则不可能 在上升迭代的中间应用下降迭代（否则不能保证收敛）。此外，加速技术在计算上更有效（特别是它不需要收敛测试），并且它具有单调行为，这不是加宽的情况例5.1为了说明这几点，我们考虑图5所示的程序。10，其中内部循环τ是从示例4.9修改的：2x1 + 2x2≤px1=x1+y+1. 0≤x11≤x212在这两种情况下，我们在位置l上应用加宽，延迟N=1，并且我们在上升迭代收敛之后执行一次下降迭代。在没有加速度的情况下，我们得到一个非常弱的不变量：Z∞={（x1，x2，p）|x1≥ 0 p ≥ 1}W∞= W1= Z∞通过加速，我们获得了更好的结果：Z∞=Z∞∞{（x1，x2，p）|x1+x2≥1<$x1−x2≤4<$x1+5x2≤10}W=∞= Z<${（x，x，p）|p ≤ 20}我们也可以考虑用阈值加宽，这在加宽操作的结果中保留了一组固定的阈值约束的子集，这些阈值约束都被其两个参数所满足。 在例4.9的情况下，自然阈值约束集由τ的主体的τ的保护的后置条件定义，其仅为τ（ ）=的（x1，x2）0X21 .一、 在N=0的情况下使用它，可以获得与在N = 1的情况下应用标准加宽相同的Z ∞。在例5.1中，用p 21扩展相同的阈值集，结果得到了改善，但仍然不如通过组合加速和加宽获得的结果精确（特别是下降迭代不收敛）。带输入和非简单保护的在例4.10的上下文中，当N=0时，我们得到Z∞= Z1={（x1，x2）|x1 + x2≥1}W1={（x1，x2）|x1+ x2≥ 1 2 x1 + x2≤ 10 x2≤ 40≤x1≤ 6< $3x 1+5x2≥ 3}...W3={（x1，x2）|x1+ x2≥ 1 2 x1 + x2≤ 10 3 x2−2x1≤ 6 3 x2−4x1≤ 35x1−22x2≤ 8 29x1−157x2≤ 29}<$（X）+xP. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）101115同样，Z∞是非常不精确的，但这里的下降迭代并不收敛（即使我们使用阈值加宽），见图8的W3。如果我们使用N=1，则Z∞更精确，并且W∞=W1=τ（X）。这些结果只是小实验，但它们说明了加宽的敏感性（如果我们延迟它，它可能会改善结果，但这也不能保证，因为它不是单调的），以及如果循环是更复杂程序的一部分，结果可能会更不精确。六、结论我们已经提出了一个扩展的抽象加速数值输入。这种扩展没有想象的那么简单--最明显的原因是观察到输入可用于将翻译转换为任意的非线性变换;此外，将变量重置为输入值可能会导致一些微妙的行为。我们的方法可以用于纯数值自动机，采用[14]中的分割方法来处理比本文中提出的单自循环更复杂的循环。此外，将我们自己限制为包含在凸多面体中的凸保护和输入不是我们的方法的理论限制，因为非凸多面体总是可以分解为凸多面体。加速与加宽。从理论上讲，加速度-与加宽相反，一些有利的性质支持其作为处理循环的辅助技术的实用性：首先，可以获得更好的精度，因为它直接利用来自程序的信息。其次，固定点计算的迭代次数减少，因为加速转换有效地消除了控制图中的循环。此外，加宽不是单调算子，而加速是，这使得近似更规则和可预测。必须获得实践经验，以估计这些性能所达到的改进程度。尽管如此，我们不得不对无法加速的过渡采取扩大的办法，以确保趋同。今后的工作。正如在引言中提到的，找到一个合适的控制图是将加速应用于逻辑-数值程序的第二个问题（我们在本文中没有讨论），例如没有显式控制流的同步数据流程序。 一方面，控制图应该允许一个合理精确的可达性分析，另一方面，它应该使 使用数值变量的抽象加速，同时保持足够的符号化w.r.t.布尔变量，以防止组合爆炸。 我们的想法是，以启发式方式识别行为像定时或线性混合自动机的状态集，这样就可以应用抽象加速另一个方向是将[14]中关于围绕同一位置的多个自环的组合加速度的116P. 施拉梅尔湾Jeannet/Electronic Notes in Theoretical Computer Science 267（2010）101引用[1] Abdulla，P. A.，A. Collomb-Annichini，A. Bouajjani和B. Jonsson，Using forward reachabilityanalysis for verification of lossy channel systems，Formal Methods in System Design25（2004），pp. 39比65[2] Bardin ， S. ， A. Finkel ， J.Leroux 和 L.Petrucci ， FAST ： Fast acceleration of symbolic transitionsystems，in：Computer-Aided Verification（CAV）（2003），pp. 118-121[3] Bardin，S.，A. Finkel，J.Leroux和P.Schnoebelen，Flat acceleration in symbolic model checking，in：自动化技术验证和分析（ATVA），LNCS3707（2005），pp。474-488.[4] 布瓦格洛湾Godefroid，Symbolic verification of communication protocols with infinitite state spacesusing QDD，Formal Methods in System Design14（1997），pp.237-255[5] Caspi，P.，D. Pilaud，N. Halbwachs和J.A. Plaice，LUSTRE：一种用于实时编程的声明式语言，在：程序设计语言原理（POPL）（1987），pp. 178比188[6] 库 索 山 口 和 R.Cousot ， Abstract interpretation ： A unified lattice model for static analysis ofprograms byconstructionor approximationof fixpoints ， in ： PrinciplesofProgrammingLanguages（POPL），1977，pp.238-252。[7] Cousot，P. and R. Cousot，Abstract Interpretation and Application to Logic Programs，Journal ofLogic Programming13（1992），pp. 103-179[8] Cousot，P. and R. Cousot，比较伽罗瓦连接和扩大/缩小抽象解释，在：PLILP269-295。[9] 库 索 山 口 和 N.Halbwachs ， 自 动 发 现 程 序 变 量 之 间 的 线 性 约 束 ， 在 ： 程 序 设 计 语 言 原 理 （ POPL）（1978），pp. 84比97[10] de Berg，M.，O. Cheong，M. van Kreveld和M. Overmars，[11] Finkel ， A. 和 J. Leroux ， How to compose Presburger-accelerations ： Applications to broadcastprotocols，in：Foundations of Software Technology and Theoretical Computer Science（FSTTCS），Lecture Notes in Computer Science2556（2002），pp.145-156[12] 弗赖堡湖 和H. Ol s'en，通过编译到presburger算法中来保护无限状态系统的安全性，在：并发理论会议（CONCUR），LNCS 1243（1997），pp. 213-227.[13] 贡诺德湖 ASPIC工具：加速符号多面体不变计算，http：//laure。 gonnord.org/pro/aspic/aspic.html。[14] 贡诺德湖“Acc'el'erationabstraitepourl'am'eliorationdelapr'ecisionenAnalysedesRelationsLin'eires，”Th'esedeoctorat，Universit'eJosephF.，Grenoble（2007）.[15] 贡诺德湖和N.Halbwachs，在线性关系分析中结合加宽和加速度，在：静态分析研讨会（SAS），韩国首尔，2006年，pp. 144-160[16] Halbwachs ， N. ， F. Lagnier 和 P.Raymond ， 同 步 观 测 器 和 反 应 系 统 的 验 证 ， 在 ： 方 法 和 软 件 技 术（AMAST）（1993），pp.83比96[17] Halbwachs，N.，Y.-- E. Proy和P. Roumano，使用线性关系分析的实时系统验证，系统设计中的形式化方法11（1997），pp.157-185[18] Jeannet，B.， 线性关系分析中的动态划分。 应用于反应系统的验证，系 统 设 计 中 的 形式化方法23（2003），pp。5-37[19] Jeannet，B.，T. 杰隆 Rusu和E. Zin ovie v a，Sym bolictestsel ebanded onapp roximate analysi s，in：Tools and Algorithms for the Construction and Analysis of Systems（ TACAS ） ， LNCS 3440，2005，pp. 349-364.[20] Jones，N. D、C.高明，[21] Leroux，J.，-Imp l'ementation dans l'outil F AST，”T h'ese de dot ctorat，E 'cole Normale Su p'eriende deCa c han（2003）.