线性混杂系统的有界可达性分析的高效路径工具

理论计算机科学电子笔记174（2007）57-70www.elsevier.com/locate/entcs基于线性规划的线性混杂系统有界可达性分析的高效路径工具李宣东a，b，1，Sumit Jha Aanandb，2 和雷布a，3南京大学计算机科学与技术系新型软件技术国家重点实验室中国江苏省南京市210092b卡内基梅隆大学计算机科学系5000 Forbes Avenue，Pittsburgh，PA 15213，USA摘要现有的线性混合自动机的可达性分析技术不能很好地扩展到实际感兴趣的问题大小。与其开发一个工具来对线性混合自动机的所有路径进行可达性检查，一种补充方法是开发一个高效的面向路径的工具来一次检查一条路径，其中被检查的路径的长度可以非常大，自动机的大小可以足够大以处理实际感兴趣的问题。设计工程师可以使用这种符号执行路径的方法来检查重要路径，从而增加对系统正确性的信心。与简单的测试不同，我们框架中的每条路径都代表了被分析系统的一组密集的可能轨迹。在本文中，我们发展的线性规划为基础的技术走向一个有效的面向路径的工具，线性混合系统的有界可达性分析。保留字：线性混合自动机，有界模型检验，可达性分析，线性规划。1引言混杂系统的模型检测问题是一个非常困难的问题。即使对于一类相对简单的混合系统-线性混合自动机类[1] -最常见的可达性问题仍然是不可判定的[1]一些模型检测工具已被开发的线性混合自动机，但他们没有很好地扩展到实际问题的大小。 最先进的工具HYTECH [8]及其改进PHAVer [9]需要执行昂贵的1 电子邮件地址：lxd@nju.edu.cn2 电子邮件地址：jha+@cs.cmu.edu3电子邮件地址：bl@seg.nju.edu.cn1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.12.02358X. Li等人理论计算机科学电子笔记174（2007）57i=0时多面体计算，其算法复杂性是指数的变量的数量在自动机。近年来，有界模型检验作为基于BDD的符号模型检验的一种补充技术而被提出，其基本思想是在模型执行中寻找长度为某个整数k的反例[5]。已有文献[6，7]给出了利用有界模型检验技术来检验线性混杂系统的方法。在这些技术中，模型检验问题被简化为命题变量和数学约束的布尔组合的可满足性问题，但实验结果表明，检验模型的执行长度与实际问题的大小仍有很大差距。由于现有的技术不能检查所有的路径的可达性分析时，试图分析的问题规模是实际意义，一个补充的方法是开发一个高效的路径导向工具，检查一个路径的时间，其中被检查的路径的长度可以做得很大，自动机的大小可以做得足够大，以处理实际感兴趣的问题。设计工程师可以使用这种符号执行路径的方法来检查重要路径，从而增加对系统正确性的信心。与简单的测试不同，我们框架中的每条路径都代表了被分析系统的一组密集的可能轨迹。在本文中，我们提出的线性规划为基础的技术发展的一个有效的面向路径的工具，有界可达性分析的线性混合系统。本文的结构如下。在下一节中，我们定义了本文中考虑的线性混合自动机的类别。 在第三节中，我们用线性规划方法给出了线性混合自动机的面向路径的有界可达性分析的解。第4节介绍了一些技术，以减少相应的路径，我们正在检查的线性规划的大小。 第5节介绍了工具原型和案例研究。最后一节给出了结论。2线性混合自动机本文所考虑的线性混合自动机是文[1]中定义的一种变化，其中变量的变化率可以给定一个可能值的范围为了简单起见，我们假设在本文考虑的任何线性混合自动机中，只有一个初始位置，没有初始条件，也没有到初始位置的转换（我们假设每个具有初始值的变量都通过从初始位置的转换重置为初始值定义2.1线性混合自动机是元组H=（X，V，E，vI，α，β），其中• X是实值变量的有限集合。 V是一组有限的位置。• E是转移关系，其元素的形式为（v，φ，φ，vJ），其中v，vJ是在V中，φ是一组形式为a≤φm的可变约束c x≤b，且x是a 我我形式为x：=c的重置动作集，其中xi∈X（0≤i≤m），x∈X，a，b，cX. Li等人理论计算机科学电子笔记174（2007）5759.K和ci（0 ≤i≤m）是实数，并且a和b可以是∞。• vI是初始位置。• α是一个标记函数，它将V− {vI}中的每个位置映射到一个状态不变量这是一组形式为a≤m的变量约束，cx≤b，其中x∈X我我我（0≤i≤m），a，b和ci（0≤i≤m）是实数，a和b可以是∞。• β是一个标签函数，它将V−{vI}中的每个位置映射到一组变化.形式为x=[a，b]的速率，其中x∈X，a，b是实数（a≤b）。对于任何位置v，对于任何x∈X，有且只有一个变化率定义x=[a，b] ∈ β（v）。Q请注意，我们在这里考虑的线性混合自动机类可以用于近似任何一般的混合自动机到任何所需的精度水平，因为它们是足够的表达，以允许一般的混合自动机的抽象过程的渐近完整性[4]。我们使用位置序列来表示线性混合自动机从位置到位置的演化。对于线性混合自动机H=（X，V，E，vI，α，β），路径段是以下形式的位置序列：（φ1，φ1）v1−→ v2（φ2，φ2）−→...（φn−1，n−1）−→vn其中满足对于每个i（1≤i≤n− 1），（vi，φi，i，vi+1）∈EH中的一条路是从vI开始的一段路。线性混合自动机的行为可以用时间序列表示。任何时间序列的形式是（v1，t1）（v2，t2）. 其中vi（1≤i≤n）是一个位置，ti（1 ≤i≤n）是非负实数。它代表了一种行为也就是说，系统从初始位置开始，然后变为位置V1在那里停留T1个时间单位，然后改变到位置V2并在V2停留T2个时间单位，等等。定义2.2对于线性混合自动机H =（X，V，E，v I，α，β），时间序列（v1，t1）<$（v2，t2）<$. n（vn，tn）表示H的行为，当且仅当满足以下条件：• 在H中有一条路径，形式为v（φ0，φ0）v（φ1，1）（φn−1，n−1）...v;0−→1−→−→n•t1，t2，. ，t n满足φ i（1 ≤ i ≤ n − 1）中的所有变量约束，即 对于每个变量约束a≤c0x0+ c1x1+. +cm xm≤b inφi，δk≤γi（xk）≤δJ 对于任意k（0≤k≤m），且a≤c0γ i（x0）+c1γ i（x1）+.. +cm γi（xm）≤b其中γi（xk）（0≤k≤m）表示当自动机以延迟ti停留在vi时变量xk的值，并且对于任何k（0≤k≤m），δ k= d k+ u jk +1t jk +1 + u jk +2t jk +2 +. + u i t i，δJ=dk+uJtj+1+uJt j+2+. +uJti，k jk+1Kjk+2ki.Jxk：=dk∈<$jk（0≤jk3，ρ1是路径，ρJ，ρ2是路径段。我们说ρk在ρ中闭，如果1 2以下条件成立：k（φJJ，φJJ）k−2（φJJ，JJ） J（φJJ，φJJ）JJ• ρ2=ρ21 −→ρ3−→ρ21，其中ρ2=ρ21−→p21，|ρ21| ≤ |ρ21|得双曲正弦值.• ρ3 =v1（φ1，φ1）−→v2（φ2，φ2）−→...（φn−1，n−1）−→vn，对于任何x出现在变量中，X. Li等人理论计算机科学电子笔记174（2007）5765在φi或α（ui）（1≤i≤n）中的约束，x：=a∈n（J J）或x：=a∈n（j i≤1）.66X. Li等人理论计算机科学电子笔记174（2007）572123212k=0定理4.1设H=（X，V，E，vI，α，β）是线性混合自动机，R（v，v）JJ（φ，φ）k（φ，φ）J是可达性规范，且ρ = ρ1−→ρ2 −→ρ1是H中的路径，其中ρ k（k > 3）在ρ中是闭的。 如果ρ1中的任何位置不是任何变量约束中的变量与ρJ中的位置相关，则ρ满足R（v，n）J J（φ，φ）（φJ，φJ）J当且仅当ρ满足R（v，v），其中ρ=ρ1−→ρ3−→ρ1。证据 假设ρ k= ρ（φJJ，φJJ）k−2（φJJ，JJ）J221−→ρ3−→ρ21，以及ρ3=v1（φ1，φ1）−→v2（φ2，φ2）−→...（φn−1，n−1）−→v n.JJ（φJJ，φJJ）k−2（φJJ，JJ）JJJJ JJ（φJJ，φJJ）（φJJ，φJJ）JJJ因此，ρ = ρ1 −→ ρ3−→ρ1，且ρ = ρ1−→ρ3−→ρ1。的如果ρ满足R（v，n），则ρJ满足R（v，n），可以证明如下。 由于ρ满足R（v，v），假设相应的时间序列σ=σJJ<$σr<$Σ JJ满足定义3.1中给出的条件，其中σr对应于1 1ρ k−2。 因此，σ r= σ r1 <$σ r2 <$. <$σ rk−2，且每个σ ri（1 ≤ i ≤ k − 2）的形式为（v1，t1）<$（v2，t2）<$. n（v n，t n）使得t1，t2，.，n满足条件定义2.2。由于ρ k在ρ中是封闭的，并且ρ 1中的任何位置都不是与ρ j中的位置相关的变量约束中的任何变量的参考点，通过移除σ r2 <$σ r3 <$. 从σ得到满足条件的时间序列σJ，在定义3.1中，对应于ρJ。因此，ρJ满足R（v，n）。另一半的说法可以证明如下。 由于ρJ满足R（v，n），假设相应的时间序列σJ=σJJ<$σ3<$σJJJ满足下式给出的条件：1 1定义3.1其中σ3对应于ρ3。由于ρk在ρ中是闭的，并且ρ1中的任何位置都不是与a相关的变量约束中任何变量的参考点，在ρ j中的位置，用σ3<$σ3 <$. 在σJ中，我们得到一个时间序列σ1`2000xk−2它满足定义3.1中的条件并对应于ρ。 因此，ρ满足R（v，v）。Q设H=（X，V，E，vI，α，β），ρ是H中的一条路，其形式为（φ0，φ0）v0−→...（φi−1，φi−1）−→vi（φi，φi）−→...（φj−1，φj−1）−→vj（φj，φj）−→...（φn−1，n−1）−→v n.变量约束a≤m如果以下条件成立：ckxk ≤b与vj（1≤j≤n）在ρ中为正• ck≥0，对于任意k（0≤k≤m），且• 对于任意xk（0≤x≤m），如果参考点是vi，则任意vl（i l≤j）是.使得如果xk= [a，b]∈β（vl）则a≥0，我们说b − kc d是变量约束的边界，其中di=0k k k（0≤k≤m）是xk在vj上的参考值。设H=（X，V，E，vI，α，β）是一个线性混合自动机，R（v，v）是一个可达-JJ（φ，φ）k（φ，φ）J能力规范，且ρ=ρ1−→ρ2−→ ρ1 被 一 路径 在H在哪里k（φJJ，φJJ）k−2（φJJ，JJ） JX. Li等人理论计算机科学电子笔记174（2007）5767ρ2=ρ21−→ρ3−→ρ21（k >3）在ρ中闭，且ρ3=v1（φ1，φ1）−→v2（φ2，φ2）−→...（φn−1，n−1）−→v n.68X. Li等人理论计算机科学电子笔记174（2007）57i=0时⎪⎪223211.M...我伊伊⎪如果存在正变量约束a≤mcixi ≤b与位置相关，J，使得• 存在一个变量集合ωn {x0，x1，.，xm}（ω参考点在ρ1中，并且• 其中，f是集合的最小值如果x∈ω，- 是的- 是的如果x⎪⎪⎫∈ωthenCJ=cielseCJ = 0 for anyi（0≤i≤m）;⎪- 是的对任意i（0≤i≤m），δ=ut+ut+... +ut- 是的c Jδ。.ii 11J我22inni=0⎪⎩一. .....其中对于任意j（1≤j≤n），xi=[uij，uij] ∈ β（v j）;并且⎪（v1，t1）（v2，t2）. n（vn，tn）是一个时间序列，⎪t1，t2，.满足定义2中的条件。⎭（注意，可以通过线性规划来计算），现在，我们可以通过[100%/100%+3]来实现数据包，而这取决于数据包的来源Σ约束条件a≤mi=0 c i x i≤ b。定理4.2设H=（X，V，E，vI，α，β）是线性混合自动机，R（v，v）JJ（φ，φ）k（φ，φ）J是可达性规范，且ρ = ρ1−→ρ2 −→ρ1是H中的路径，其中ρ k（k> 3）在ρ中是闭的，并受kJ约束。如果k> kJ，则ρ不满足R（v，v）.证据 假设ρ k= ρ（φJJ，φJJ）k−2（φJJ，JJ）J221−→ρ3−→ρ21，以及ρ3=v1（φ1，φ1）−→v2（φ2，φ2）−→...（φn−1，n−1）−→v n.JJ（φJJ，φJJ）k−2（φJJ，JJ）JJJ因此，ρ = ρ1 −→ ρ3−→ρ1。 假设ρ满足R（v，n），且对应的时间序列σ=σJJ<$σr<$σJJJ满足给定的条件1 1定义3.1其中σr对应于ρk−2。它遵循σ r= σ r1 <$σ r2 <$. σ rk−2其中每个σ ri（1 ≤ i ≤ k − 2）的形式为（v1，t1）<$（v2，t2）<$... n（v n，tn）使得t1，t2，.满足定义2.2中的条件。 由于ρk在ρ中闭合，受kJ约束，如果k> kJ，则存在与a相关的正变量约束位置ρJ这是一个不满足的，这导致了矛盾，因此，主张成立。Q这个定理告诉我们，在某些情况下，我们只需要关注一条较短的路径，因为通过重复其中的路径段来扩展路径将导致给定的可达性规范不满足。ρ⎨⎪X. Li等人理论计算机科学电子笔记174（2007）57695工具原型和案例研究基于本文提出的技术，我们实现了一个线性混合自动机有界可达性分析的工具原型。该工具70X. Li等人理论计算机科学电子笔记174（2007）57˙˙˙、、，θ=15 、、、y：=1v1y≤10e1y= 10？v2x≤2x1：=6x2：=6v1θ= 6e1x1≥6）v2θ=−4v0）的情况）v0）xstec1=1xstec1=1e0xtec=1x：=0xstec=1e0xtec2=1（e2θ=3xstec2=1ystec= 1ystec= 1θ≤15X ：=0θ≥3J J\n\n\nJ1\nˆx= 2？e4e2 x=2？e3θ= 15e4\e5θ=3\x16\x26x2≥6vx2：=0\θ=15\，v、、、v4x≤2ystec=−2xstec=1（e3y=5？x：= 0v3y≥5ystec=−2xstec=1v3θ=−3xstec1=1xstec2=1θ≥3\v4关闭J（一） J J J（二）Fig. 1.自动机模型水位监测与温度控制系统它的图形界面允许用户交互地构造、编辑和分析线性混合自动机。该工具中集成的线性规划软件包来自于ORB-Objects公司这是一个免费的Java类集合，用于开发运筹学，科学和工程应用程序。在HP工作站（英特尔至强 CPU2.8GHz×2/3.78GB），评估了本文提出的技术的潜力通过几个案例研究。图 1 （ 1 ） 中 描 绘 的 一 个 示 例 是 [2] 中 的 水 位 监 测 器 。 沿 着 路 径 v0（v1v2v3v4）k，我们检查位置v4是否可达，并从工具中得到肯定的答案，k=100、 200、 230、 400、 450、 500、 10000分别表1分别显示了使用原始技术（未进行任何优化）、分解线性程序的优化技术和缩短路径的优化技术时的工具性能当k≥500，如果没有任何一种优化技术，该工具无法给出结果由于线性程序中出现ming包集成在工具中。实际上，通过缩短路径的优化技术（见定理4.1），对于这个例子，该工具可以给出任何k的结果。图1（2）中描绘的另一个示例是[2]中的温度控制系统。沿着路径v0（v1v2v1v3）kv1v4和v0（v1v2）k1（v1v3）k2v1v4，我们检查是否需要完全关闭（位置4是可到达的），并且得到具有k、k1和k2的各种值的否定答案。工具性能是如表2所示。对于路径v0（v1v2v1v3）kv1v4，没有任何优化技术有效，并且当k≥450时，由于集成X. Li等人理论计算机科学电子笔记174（2007）5771工具. 对于路径v0<$（v1<$v2）k1<$（v1<$v3）k2<$v1<$v4，定理4.2的条件成立，使得缩短路径的优化技术起作用。72X. Li等人理论计算机科学电子笔记174（2007）57路径：v0（v1v2v3v4）kK原始技术分解LP缩短路径约束变量存储器时间时间时间1003191997512M61.172s1.031s0.031s20063911997512M466.140s1.562s0.031s23073512297512M702.766s1.750s0.031s4001279139971470米3969.421s3.187s0.031s4501439144971470米4485.328s3.469s0.031s500Java.lang.内存不足错误4.109s0.031s10000Java.lang.内存不足错误38.047s0.031s表1水位监测仪的实验结果路径：v0（v1v2v1v3）kv1v4K原始技术分解LP缩短路径约束变量存储器时间时间时间10044151004512M90.218s90.218s90.218s20088152004512M686.938s686.938s686.938s230103152304512M1180.297s1180.297s1180.297s4001759139981470米5574.312s5574.312s5574.312s450Java.lang.内存不足错误Java.lang.内存不足错误路径（P）： v0（v1v2）k1（v1v3）k2v1v4K1K2原始分解LP缩短路径约束变量存储器时间时间时间50502215504512M10.532s10.532s0.016s10010044151004512M76.703s76.703s0.016s200200879119981004M496.609s496.609s0.016s表2温度控制系统路径：v0（v1v2v1v3）kv5v6KPHAVer原创技术（OriginalTechnique）时间时间202400s12.359s304h36.688s4020小时82.891s80616.671s1001143.344s1504067.391s表3实验自动机我们还将我们的技术与PHAVer [9]进行了比较，最先进的工具HYTECH[8]。由于PHAVer需要执行昂贵的多面体计算，其容量受到自动机中变量数目的限制。 我们简单地构建一个实验自动机，如图2所示，其中有七个位置和变量。 沿着路径v0（v1v2v3v4） kv5v6，我们分别检查位置 v6是否可由PHAVer和我们的工具到达。由于PHAVer不提供任何计时器，我们手动记录其执行时间。实验结果如表3所示。当k设置为20和30时，PHAVer分别花费约0.66和4小时进行检查，这比我们的工具使用原始技术的执行时间长得多X. Li等人理论计算机科学电子笔记174（2007）5773当k= 40时，PHAVer运行20小时后不能给出任何结果，但即使当k= 150时，我们的工具也可以在可容忍的时间内给出结果。请注意，为了公平起见，我们使用展开路径作为PHAVer的输入，以避免它进行完整的可达性分析。由于PHAVer算法需要执行昂贵的多面体计算，其算法复杂度与自动机变量数成指数关系，这对实验结果给出了直观的解释上述实验是初步的，并使用免费提供的线性规划-明包，但他们表明了一个明确的潜力，本文提出的技术与先进的商业线性规划包的支持。、、v1v2v0）x1：=15x2：= 6x3：= 6x4：= 0x5：= 0x6：= 0x7：= 0xstec1=6xstec2=[0，2]xtec3=[0，2]xstec4=[0，4]xstec5=[0，1]xstec6=[0，20]xstec7=[−10，0]1 ×10≤15Jxstec1=−4xstec2=[0，2]xtec3=[0，2]xstec4=[0，20]xtec5=[0，20]xstec6=[0，10]xstec7=[−20，0]x1≤33x5−x4−x7≥ 0x6−x7−3x5≥0Je4x1=3x4−x5−x6+0。1x7≥0，x3：=0，v4e2x1= 3，vx3：=0，v3xstec1=−3xstec2=[0，2]xtec3=[0，2]xstec4=[0，12]xtec5=[0，12]xstec6=[0，12]xstec7=[−20，0]x1≥3x7+ 10x6−10x5≥0\4x5−x4≤4Jx1= 3 x4− x5− x6+ 0。1 x7≥ 0e5 x3：= 0xstec1=6xstec2=[0，2]xtec3=[0，2]xstec4=[0，8]xtec5=[0，2]xstec6=[0，4]xstec7=[−20，0]，x1≤15x4−3 x5+ 0. 1x7≤0x6−0 。 1 x7−3x5≥0\4x5−x4≤4J，v，v5、、、v6xstec1=6xstec2=[0，2]xtec3=[0，2]xstec4=[0，16]xtec5=[0，4]xstec6=[0，8]xstec7=[−20，0]，x1≥153x5−x7−x4≥ 0x6−x7−x4≥0\4x5−x4≤4Jxtec1=1，xtec2=[0，2]xtec3=[0，2]，xtec4=[0，4]xtec5=[0，1]，xtec6=[0，2]xstec7=[−10，0]，x1≥15x4−x5≥0x5−x2≥0x4+ x6− x5+ 0。1 x7≥0 x6+ 0。1x7−x2−x3≥0x6 +x5−x4≤ 00的情况。1x7 +x5≥ 0 J图二.实验自动机6结论e1x1= 15，x2≥6）x4− x5− 0。1 x6+ 0。1 x7≥0（e3）x1=15，x2≥63 x5− x4≤ 0，x4− 2 x6≥0e6x1=15，x2≤5。九、x3≤5。9，x5−x4≤0x6+ 2 x5− x4+ x7≤ 0x7+ x5≤074X. Li等人理论计算机科学电子笔记174（2007）57本文基于线性规划理论，提出了一种有效的面向路径的线性混合可达性分析方法。X. Li等人理论计算机科学电子笔记174（2007）5775Tomata，它一次检查一条路径，其中被检查的路径的长度由于现有的技术还没有产生一个有效的工具来检查所有的路径在一个线性混合自动机的问题与实际利益的大小，工具来自本文提出的技术将成为一个设计工程师的助手线性混合自动机的可确认感谢Edmund M教授。克拉克和匿名重新观众的宝贵意见和建议。 第一作者和 第 三 作 者 分 别 获 得 国 家 自 然 科 学 基 金 资 助 项 目 （ No.60425204 ，No.60233020）、国家重大基础研究973计划资助项目（No.2002CB312001）和江苏省科学基金资助项目（No.BK2004080）。第二作者感谢卡内基梅隆大学计算机科学系研究生奖学金的支持。引用[1] Thomas A.亨辛格混合自动机理论。在第11届IEEE计算机科学逻辑研讨会（LICS 1996）上，278-292.[2] R. 巴尔角Courcoubetis，N.Halbwachs，T.A.Henzinger，P.H.Ho，X.Nicollin，A.Olivero，J.西法基斯，S.尤文混杂系统的算法分析。理论计算机科学，138（1995），第3 -34页。[3] Thomas A. Henzinger，Peter W. Kopke，Anuj Puri，and Pravin Varaiya. 混合自动机的可决定性是什么？计算机与系统科学杂志，57：94-124，1998。[4] Thomas A.放大图片作者：Henzinger，Pei-Hsin Ho，Howard Wong-Toi.非线性混杂系统的数学分析。IEEE自动控制学报，1998，第540 -554页。[5] 放大图片创作者：Alessandro Cimatti，Edmund M.放大图片作者：Ofer Strichman，Yunshan Zhu.有界模型检验《计算机进展》，第58卷，学术出版社，2003年。[6] 马丁·弗兰兹克里斯蒂安·赫尔德混合系统有界模型检测的高效证明引擎。《理论计算机科学电子笔记》，2004年第89卷第4期。[7] 吉勒·奥德马德，马可·博扎诺，亚历山德罗·西马蒂，