密集实时系统的谓词抽象及其验证方法

218《理论计算机科学电子札记》65卷第6期（2002）网址：http://www.elsevier.nl/locate/entcs/volume65.html20页密集实时系统的谓词抽象M. 奥利维尔·Mollera，HaraldRueb和MariaSoreab;1a金砖国家，奥胡斯大学，计算机科学系，Ny Munkekee，Building 540，8000 Arhus C，Denmarkomoeller@brics.dk2bSRI国际，计算机科学实验室，333 Ravenswood Avenue，Menlo Park，CA 94025，USA邮箱：soreag@csl.sri.com摘要我们提出谓词抽象作为一种手段，用于验证密集的实时系统的安全性和活性属性丰富的类首先，我们定义了一个时间系统的限制语义，它在观察上等价于标准语义，因为它验证了同一组演算公式，而无需下一步运算符。然后，我们重铸的模型检测问题Sj ='为时间自动机S和演算公式'的谓词抽象。 每当一组抽象谓词形成所谓的基础时，所得到的抽象在S验证“i相应的nite抽象为mula验证此”的意义上是强保留的。现在，抽象的系统可以使用熟悉的- 演算模型检查。与时间自动机的区域图构造一样，时间自动机的谓词抽象算法通常是昂贵的。在许多情况下，只使用抽象谓词的基的子集来计算Nite双模拟的近似值是可行的。从一些粗糙的抽象开始，我们定义了一个收敛到强保持抽象的有限抽象序列。在每个步骤中，新的抽象谓词是从 夜间基础。 失败的反例演算模型检查尝试可以用于以启发式方式选择一小组新的抽象谓词来重新定义抽象。？ 这项研究得到了美国国家科学基金会的资助CCR-00- 82560和CCR-00-86096，以及NASA兰利研究中心与霍尼韦尔明尼阿波利斯公司的合同B 09060051和合作协议NCC-1-399的支持。这项研究的大部分是在第一作者于2001年7月/8月 访问SRI国际时进行的。1 也与德国乌尔姆大学合作2 计算机科学基础研究，由丹麦国家研究基金会资助。c2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。MoLler，Rue，Sorea2191介绍时间自动机[2]是一种扩充了nite集的状态转移图 实值时钟 时钟以统一的速率进行，并限制可能发生转换的时间。给定一个时间自动机和一个用时间逻辑（如TCTL[1]或T[11]）表示的属性，模型检验回答了时间自动机是否满足给定公式的问题。基本的图论模型检测算法由Alberr，Courcoubetis和Dill[1]构造了一个nite商，所谓的区域图，在nite状态图。然而，直接基于这种分区的显式构造的算法在实践中不太可能有效地执行，因为区域图的状态的等价类的数量随着最大时间常数和用于指定时序约束的时钟的数量呈指数增长。例如，Yovine [20]给出了以符号方式表示区域的数据结构以及用于验证实时系统的算法和工具的最新概述。基于时间自动机的节点抽象计算、模型检测和抽象的连续恢复，提出了一种新的时间自动机安全性和活性性质的验证算法.该算法不需要牺牲完备性，通常不需要计算完备区域图来判定模型检测问题。在最坏的情况下，它以强保持给定模型检验问题时间系统的nite近似的计算是基于抽象解释的概念[5]，特别是谓词抽象的概念[10]。给定一个转移系统和一组谓词，该方法确定一个抽象，其中抽象状态空间的每个状态都是对抽象谓词的真值赋值。抽象是保守的，在这个意义上，命题演算公式对具体系统成立，如果它对谓词抽象系统成立[17]。由于反向陈述一般不成立，谓词抽象到目前为止主要用于证明安全性而不是活性性质。一般来说，应用谓词抽象的主要问题是提出一组适当的抽象谓词。在定时自动机的情况抽象定义的主要技术问题是保证抽象模型的公平性，即防止延迟步骤抽象为抽象系统的自循环。Uribe[19]区分了文献中用于将公平性构建到抽象中的三种不同方法：第一，通过向抽象系统添加新的公平性约束，第二，通过将公平性纳入逻辑，第三，通过修改nite-state模型检查器。我们提出了第四种方法，MoLler，Rue，Sorea220这个问题通过引入一定的限制延迟步骤，我们表明，相应的限制语义的时间自动机是等价的时间进展语义的意义上，这些不同的解释验证同一套命题演算公式（没有下一步操作）。总之，我们的谓词抽象算法确定了一个判定过程，用于检查时间自动机是否满足给定的演算公式。计算一个强抽象所需的抽象谓词集，即所谓的基，仍然可能非常大。从一个平凡的过度近似开始失败的模型检查尝试的反例用于指导选择。反例引导修正的思想已经被许多研究者使用过，最近的工作包括[4，7，14]。 与这些方法相比，我们使用的反例只作为一个启发式选择良好的枢轴谓词从固定的，预定的抽象谓词池，以加快收敛的近似过程。此外，基于谓词抽象[10，3，17]的初始状态系统的验证技术通常是不完整的。然而，我们的时间系统的抽象方法是完整的，因为在极限下，我们构造了一个满足与原始时间系统相同的公式集的nite system- tem。Dill和Wong-Toi[8]也使用时间自动机的可达状态集的过近似和欠近似的迭代，但他们的技术仅限于证明不变量。基于谓词抽象的技术，Namjoshi和Kurshan的算法[16]计算一个nite bisimulation，只要它存在。因此，原则上，他们的算法可以应用于计算时间自动机的nite互模拟。然而，目前尚不清楚他们的方法是否适用于实践。Tripakis和Yovine[18]展示了如何抽象密集实时，以获得时间抽象的，-nite互模拟。当需要计算较粗的抽象时，我们希望通过谓词抽象和谓词抽象的再执行来获得更小的转换系统。本文件的结构如下。在第2节中，我们回顾了时间自动机的基本我们还定义了限制延迟步骤的概念，并表明这种限制语义的时间自动机是观察等价的自然语义。 限制语义用于定义在第3节中，我们讨论了时间系统的过近似和欠近似。在第二节中，在第四章中，我们引入了基的概念，它是一组抽象谓词，表达能力足以区分任何两个不同的时钟区域，并且我们证明了对于以基为抽象谓词的谓词抽象，近似对于下一个自由演算是精确的。然后，在第5节中，我们定义了一个终止算法，用于迭代地重复抽象，直到给定的属性被证明或反驳。最后，第6MoLler，Rue，Sorea221l0y1x：=0x：=0y > xL1X >yL20y：= 0Fig. 1.一个定时系统的例子。载有一些结论性意见。由于缺乏空间，我们通常省略证明，但详细的证明可以找到在本文的扩展版本中[15]。2定时系统我们回顾一些基本概念的过渡系统和定时系统。此外，我们引入了时间推进系统的概念，并表明，在这些系统中的延迟步骤是不可观察的，在一个版本的proposi-tional演算没有下一步操作。这些结果为证明第5节中的抽象技术的完备性奠定了基础。下面所定义的时间系统模型是由Alberr，Courcoubetis和Dill [1]引入的时间自动机模型驱动的。3用于测量时间的时钟被编码为变量，这些变量在非负实数IR+上进行解释。时间系统的变迁通常受到时间约束的约束。定义2.1 [定时约束]给定一组时钟C，定时（或时钟）约束Constr的集合包括true，x。d，和x y。d，其中x; y 2 C，d 2 IN，./ 2f;<;=;>; g. 集合Inv是Constr的子集，其中。 选自f; g和d2f0; ：;c g.定义2.2 [时间系统]给定命题符号A的集合，时间系统S是元组hL; P;C; T; l0; Ii，其中L是位置的非空nite集合，P：L！}（A）将每个位置映射到一组命题符号，C是 Nite组的时钟，不L }（Constr） }（C）L是一个过渡关系，l0 L是初始位置，3 为了简单起见，我们不考虑时间自动机的（同步）网络。 然而，本文的结果，可以扩展到这样的网络。MoLler，Rue，Sorea2220I（l）成立。 状态转换步骤（1）！（l; ）ocurs如果存在我：L！}（Inv）为每个位置l分配一组向下闭合的时钟约束; I（l）的元素是位置l的不变量g;r我们写l！L对于hl;g;r;l0i2T. 发射过渡弹不仅会改变当前位置，而且还将R中的时钟重置为0。如果定时约束（转变的保护）g相对于时钟的当前值保持，并且如果目标位置的不变量相对于时钟的修改值被满足，则转变可以仅是红色的例2.3图1显示了一个具有三个位置l 0、l 1、l 2和两个时钟x、y的定时系统。 初始位置为l 0，转换使用时序约束和时钟重置（如x：= 0）进行修饰。位置l0的不变量是y 1。为真的定时约束将被省略。一个函数：C！IR+是一个时钟评估，时钟评估集是在VC 中 收 集 的。时钟值（+k）是通过将k加到中的每个时钟的值而获得的。对于X C，[X：=0]表示将每个时钟x 2 X更新为零并保持所有其他时钟值不变的时钟评估。通过将g中的时钟x代入相应的值（x）来获得关于时钟评估的时钟约束g的值g。如果g简化为真值，满足g，我们写jg。一个时钟求值集XVC满足g 2 Constr，记为Xjg，当且仅当jg对所有2 X .一 对（l;）2 L V C称为时间构形，如果它满足不变量I（l）;形式上，对于每个不变量g2 I（l），j I（l）i j g.Alberr、Courcoubetis和Dill[1]引入了时钟区域的基本概念，它将时间自动机的可能时钟评估空间划分为许多区域。定义2.4 [时钟区域]设S是具有时钟C和在S的任何定时约束中出现的最大常数c的定时系统。时钟区域是时钟评估的集合XVC，使得对于所有定时约束g 2 Constr（c）和对于任何两个1;2 2 X，情况是1jg当且仅当2jg。在这种情况下，我们写1S2。定时步骤或者是延迟步骤，其中时间以某个正实值时间推进，或者是瞬时状态转换步骤。定义2.5 [定时步骤]设S是具有时钟集合C和转移关系T的定时系统。如果n>0，我们可以说定时配置（l;+n）是通过延迟步骤（li）从（li）获得！Æ（l;+n），如果ivariant约束g;r0 0g;ral！L2 T，和jg，0 =[r：=0]，0jI（l0）. 德尔·阿·伊联盟状态转移步骤定义了定时系统S的定时转移关系。现在，路径（或轨迹）是一个集合s0）s1）：的内部序列。00MoLler，Rue，Sorea223（l0;（1：2）（10;：01：2）（10;：0：12）（11;：0：12）l0X1x= 1L1图二. 示例2.6的定时系统。定时系统，如上所述，允许在不超过某个给定界限的情况下的延迟步骤的nite序列。序列1个=2个1=41=8（1;x=0）=）（1;x=1=2）=）（1;x=3=4）=）（1;x=7=8）（）下一页例如永远不会到达时间点1。具有迹线的系统，使得在有界时间范围内可能发生无限数量的步骤，被称为zeno。这种行为通常通过将可能的行为限制为nonzeno来排除。为了保留由状态转换步骤的inite序列引起的错误行为，我们使用比nonzenoness稍微弱一点的假设。我们只考虑满足以下假设的路径假设1（时间不收敛）在每一个延迟步骤的无限序列中，每个时钟的评估最终都会超过每个界限。在续集中，我们建立时间抽象，不区分状态转换步骤和延迟步骤。定义这种抽象的主要困难是防止延迟步骤被抽象成抽象系统上的自循环。例2.6考虑图2中的计时系统。在不收敛的假设下，该系统满足位置l1总是可到达的性质。例如，下面的序列是这个系统的可能轨迹的前x。1个=2个1=41=4true;;（10; x=0）=）（10; x=1=2）=）（10; x=3=4）=）（10; x=1）=）（11; x=1）我们使用三个抽象pre-icates从图2中抽象出计时系统0return 0;1x1，且2x = 1. 在抽象系统上，定时系统的单个状态转换步骤根据这些谓词是否成立而被分割。例如，在初始抽象配置中，只有0和1有效，因为在初始具体状态下时钟的值为零。现在，对应于延迟小于1的延迟步骤，存在到仅1成立的状态的抽象转换。使用足够小的延迟步长，一个保持在该状态，或者一个达到仅保持2的状态，即时钟值正好是1。下面给出了所得到的抽象转换系统的一个片段请注意在配置（l0;：01：2）时的自循环，它还没有出现MoLler，Rue，Sorea224在具体的制度中。由于这个循环的存在，对于抽象系统，在每一条可能的路径上， 最终达到L1为了避免这种无关的自我循环，非收敛性的概念必须以某种方式纳入抽象系统。然而，这种限制不能用抽象系统中的时滞来定义，原因很简单，因为没有时间或时滞的概念在这个层面上。在我们的方法中，我们强制执行的非收敛性假设明确限制定时系统的模型延迟的步骤，迫使时钟的步骤时，所有的分数时钟值不为零的整数界限。通过这种方式，上面的trace（）的第二个和第三个延迟步骤被明确排除。定义2.7 [受限延迟步长]对于具有时钟集C的定时系统并且最大常数c，限制的延迟步长是delaystep（l;）！对所有的立场，真正的价值观，这样的，（l;+l）（1）9x2C：9k2f0; ：;cg：（x） =k_（（x）k^（x） +k）：状态转移步和限制延迟步的结合产生关系式R（L;VC）（L;VC）。 现在，一个严格路径是一个连续序列的配置s0）Rs1）R： 。或者，实际上，情况是）R是）的子关系。然而，上述延迟步骤的限制不一定强制执行进展时间，如示例2.3中的系统的以下受限路径所示。（l0;x = y =0）true;？=）（l1; x=y=0）tru e;？=）（l0; x=y=0）tru e;？=）（l1; x=y=0）注意，为了防止时钟x和y超过时钟值0，需要状态转换步骤的循环。对应于不收敛的定时跟踪和限制延迟步骤的假设，我们关联两个语义的定时系统的过渡系统。自然语义M包括在时间不收敛假设下的任意延迟步骤，而限制语义MR仅包括如定义2.7中的限制延迟步骤。定义2.8 [时间系统的语义]设S = hL; P; C; T;10; Ii是一个时间系统.我们将S与两个转移系统M：=hLVC;P;（））;（10;0）iMR：=hLVC;P;（）R）;（10;0）i符号0表示时钟评估，将每个时钟映射为0。M称为自然语义，MR称为S的限制语义我们证明了延迟步骤的限制并不改变模型的可能观测值，相对于无下一步操作的微积分公式。MoLler，Rue，Sorea225######[[：']]M：=Sn[[']]M#2.1 Next-Free的定义 - 微积分演算[13]是一种分支时间时态逻辑，其中公式由原子命题、布尔连接词、最小x点运算符和下一步运算符'构建，它表示存在满足'的后继运算符。我们对恢复下一步操作符的主要兴趣源于这样一个事实，即我们不想区分一个持续时间为1的延迟步骤和两个持续时间为2=5和3=5的后续延迟步骤，因为这些迹线被认为是观测等效的。Dams[6]、Tripakis和Yovine[18]也考虑了没有显式下一步运算符的逻辑。定义2.9 [下一个自由演算]设A是一组原子谓词，Var是一组变量;然后，对于p2A和Z 2Var，下一个自由演算公式的集合L由文法'：：=ttjp j'^' j：' j9（'U'） j8（'U'） jZ jZ：'公式被假定为语法单调的，也就是说，每个变量被假定出现在偶数个否定下，以保证所考虑的x点的存在性。句子是一个没有自由变量的公式。因此，对于模9（“1U”2）的存在直到在某些变换s中成立，i“1在 从 s 开 始 的 某 条 路 径 上 成 立 直到”2成立. 类似地 ， 对于mula8（“1U”2），如果这个条件对于从s开始的所有路径都成立，则在s中成立一个泛直到。在转移系统M=hS;P;）R;s0i中，下一个自由演算序列的语义由公式成 立的时间构形集[[]]M给出. 包含自由变量Z 2 Var的子公式使用赋值函数处理#：Var！ }（S）. 更新符号#[Z：= s]表示在除Z之外的所有变量上与#一致的赋值#0，其中#0（Z）=sS。定义2.10 [下一个自由演算的语义]给定一个转移系统M=hS;P;）R;s0在时 间 配 置 集S=LVC上，以及一个赋值#：Var！ }（S ）的结构上归纳地定义了对公式“2 L”关于φ进行验证的构造集[ [“] ] M。[[tt]]M：=S[[p]]M：=f（l;）2Sjp2P（l） g[['1^'2]]M：=[['1]]M\[['2]]M我的天第一百一十二章[[9（'1U'2）]]M：=fs2Sj forsomepath=（s0）s1）：）其中s0=s;对于某些i0;si2[['2]]M和sj2[['1]]M，对于0jigMoLler，Rue，Sorea226######[[8（'1U'2）]]M：=fs2Sj foreverypath=（s0）s1）：）其中s0=s;对于某些i0;si2[['2]]M和sj2[['1]]M，对于0jig[[Z]]M：=#（Z）[[Z：']]M：=\fESj[[']]ME g##[Z：=E]我们写M;s; #j='来表示s2[[']]M。省略下标#whenever是一个句子。两个构形s和s0被称为不可区分的，如果它们满足相同的L个句子的集合。定义2.11 [-等价性]对于一个转移系统M，两个条件s;s0是-等价的，记为ysMs0，如果对于每一个条件'2L：s2[[']]M当且仅当s02[[']]M.二元关系M实际上是关于时钟评估的等价关系。此外，-等价性表征时钟区域，在这个意义上，两个时钟评估是在相同的时钟区域，当且仅当它们是-等价的。因此，等价性是一个nite指标。引理2.12设S是具有时钟集C和最大常数c的定时系统，并且设M是相应的自然跃迁系统。那么对于所有的l 2 L和时钟评估当S0时 ，时间构形（l;）和（l; 0）是-等价的，即（l;）M（l; 0）.文章的写作是通过对“。 本文证明了在下一个自由演算中，时间系统的自然语义和限制语义是不可区分的。直觉上，L中的句子不能区分时钟的数量值，因此所有具有相同控制位置的配置，- 等效时钟评估满足相同的L个句子集合。定理2.13设S是具有时钟C、最大常数c、自然语义M和限制语义MR的赋时系统。在M的不收敛假设下，对于每个句子“2 L：[[']]M 为[[']]MR是的。再一次，的过程是通过归纳得出的。 唯一有趣的情况是那些为until为mulas。 因此，考虑形式9（“1U”2）。根据定义2.10，s2[[9（'1U'2）]]Mi存在路径开始-这样做，（2）si2[['2]]M对于某些i0;并且对于所有0ji，sj2[['1]]M第一百一十二章由于限制语义中的每条路径也是自然语义中的一条路径，因此可以证明，对于自然语义中验证（2）的每条路径，存在限制语义中也验证（2）的路径。首先，我们认为，在）n）R中的一个删除步骤不会跨越MoLler，Rue，Sorea227####其中si2[['2]]M和81j yg的过近似和欠近似初始状态由（l0;：）描述，因为在初始位置，时钟x和y的值为零，因此保持x y。转换是根据定义3.2建立的。例如，在过近似中从（l 1;：）到（l 0;）的转变在欠近似中不存在，因为对于具有（x）= 0和（y）= 0以及（l 1;）2（l 1;：）的评估，不存在具有（l0;0）2（l0;）的评估0，使得（l1;））（l0;0）。MoLler，Rue，Sorea229l2;：l2;：0#M0M近似M= hSA;Pi）; SA i of M.然后，谓词抽象[[：']]M：=SAn[[']]M##以及相应的过近似和欠近似M+，Ml0;l0;：l1;l1;：l2;l0;l0;：l1;l1;：l2;a：过度近似b：欠近似图三.图1中的定时系统的近似值，x > y。F或转换关系）和）+wede ne（）），分别（）+）如下：（））：=f（（l;）;（l0;0））2SCj9b;b0：（l;b））（l0;b0）^（l;）2（l;b）^（l0;0）2（l0;b0）g（）+）：=f（（l;）;（l0;0））2SCj9b;b0：（l;b））+（l0;b0）^（l;）2（l;b）^（l0;0）2（l0;b0）g下一个陈述直接从定义3.3得出。引理3.5对于一个（具体的）转移系统M，其转移重具有各自的过渡关系）+，）情况是，（i）（））（）+），以及（ii）（））+。定义3.6[谓词抽象]设M=hSC;P;）;sC是一个迁移系统，是一组抽象谓词。考虑到，在在定义3.3中，上近似M+=hSA;P+）+;sAi，以及下近似M+ = h SA ;P+）0Msemantics[[']]#，其中是+或，对于一个公式“2L，并且nite转移系统M被定义在相互感应的方式。符号用于切换符号。[[]]M：=SATT编号[[p]]M：=（l;b）2SAjp2P（l）[['1^'2]] M：=[['1]]\[['2]]第一百一十二章[[9（''）]]M：=fs2SAj forsomepath=（s）s）： ）1个U 201号#MoLler，Rue，Sorea230M其中s0=s;forsomei0;si2[['2]]#M和sj2[['1]]#对于0jigMoLler，Rue，Sorea2310FGMMFGFG如果系统处于位置L2，则该位置为真。根据定义3.6，[[8（'对于每个路径，M：=fs2SAj=（s）s）：）1个U 201号M其中s0=s;forsomei0;si2[['2]]#M和sj2[['1]]#对于0jigM[[Z]]# ：=#（Z）[[Z：']]M：=\fESAj[[']]MEg##[Z：=E]我们也写M;（l;b）; #j=A'，以表示（l;b）2[[']]M。#定理3.7（抽象的合理性）设M=hSC;P;）;sCi是一个变迁系统，一组抽象谓词，M+，M是上-M关于的近似和欠近似 则对于任何句子'2 L，以下成立（表示关于的具体化函数）：（[[']]M）[[']]M（[[']]M+）证据 这个证明是通过对'的结构进行归纳得出的，并利用了引理3.5。2例3.8考虑我们在图1中运行的例子，我们想验证位置l2永远不会到达。此属性由- 演算公式：= 9（tt Uatl2），其中在l2 2A是（boo）亲po-M的抽象态集其中“validate”由下式给出：[2019 -09-19]第10话（tt U在l2 ）]]fg[001 pdf1st-31files]=SA n [[9]（tt U在l2+）]]fg==f（l0;）;（l0;：）;（l1;：）gM关于抽象谓词的过逼近（x > y）的情况如图3所示。 由于M的初始状态（l 0;：）为包含在集合[[：9（tt Uatl2）]]中Mf，g，公式在抽象上成立过渡制度因此，M;（l 0; b 0）j= A'成立。根据定理3.7，性质也适用于具体的转移系统M;（10;0）j=“。M M+这个例子的一个有趣之处在于[[]]FG =[[']]fg。 我们现在给出一个基于区域概念的抽象谓词集的判定准则，该准则对于保证一般的过近似和欠近似的收敛性是足够的。MoLler，Rue，Sorea2324基础基础是一组抽象谓词，其表达能力足以区分两个时钟区域。如果一个基用于谓词抽象，那么近似对于下一个自由演算是精确的MoLler，Rue，Sorea233定义4.1 [基础]设S是具有时钟集C的定时系统，设是一组抽象谓词。Then是所有时钟评估1; 2 2 V C的S i基准（8）2：1J ，2j）暗示1S二、例如，对于具有时钟集合C和最大常数c的定时系统S，时钟约束Constr的（nite）集合、不变约束Inv的（nite）集合、时钟约束Constr（c）的（nite）集合以及商VC模S的隶属谓词的（nite）集合都是基集合。由于谓词Constr（c）的集合是nite，因此每个时间自动机都有一个nite基。然而，请注意，这个基础不一定是最小的。示例4.2集合 ：=fx= 0; y = 0; x1; x1; y1; y1; x > y; xyg<是图1中的定时系统的基础。定理4.3设S是具有最大常数c和时钟集C的定时系统，M是相应的变迁系统。设是关于S的基，M，M+ M关于. 然后，对于任何句子'2L，[[']]M=[[']]M+ .是的。 由于它必须表明（l; b）+，我们假 定 两个条件（l;b）和（l0;b0）都必须表明（l;b））+（l0;b0）.根据定义3.3，存在;02 V C使得（l;）2（l; b）和（l 0; 0）2（l 0; b 0）使得（l;））（l0;0）。首先，在由于状态转换步骤而保持（l;））（l0;0）的情况下，g;rg的一些过渡l！L对当前的时钟评估感到满意，是，j G.以来 是所有时钟计算的基础，约为2 VC，（l; ~）2 （l; b）由定义4.1得出S~，因此由定义2.4得出~jg。g;rtransition l！L是可能. 因此，对于所有~2 VC，（l; ~）2 （l; b）存在02VC，其中（l0;0）2（l0;b0）suchthat（l;~））（l0;0）。根据定义3.3它遵循（l;b））（l0;b0）。其次，如果（l;））（l0;0）由于一个delay步长而成立，则l=l0且0jl（l），对于（l;0）2 （l;b 0）。 由于I（l）2 Inv，并且Inv是基础，通过定义4.1，因此，对于所有时钟评估，约2 VC，（l; ~）2 （l; b），S~，因此根据定义2.4，~jI（l）. 由于（l;））（l;0），根据延迟步长的限制（定义2.7）和0不在同一区域。因此，在位置l处，对于具有（l; 0）2（l; b）的所有~2VC，存在到具有（l;0）2（l; b0）的某个02VC同样，根据定义3.3，得出（l;b））（l0;b0）。2推论4.4（基完备性）设S = hL; P; C; T; l0;I i是一个时间系统，M=hLVC;P;）;（l0;0）i是相应的转移系统，设因此，对于满足上述条件的所有时钟评估，00MoLler，Rue，Sorea234MM+M是S的基，并且令（l 0; b 0）=（l 0; 0）。 那么对于任何句子“2 L：（I; b）2[[']]M ，（I; b）2[[']]M+0 0 0 0 0 0这直接由定理3.7和4.3得出。5抽象的回复给定一个赋时系统的具体模型M，初始状态为s0，抽象谓词的nite基和一个求M的公式，我们给出了一个计算M的过逼近的算法，该算法足以证明或反驳模型判定问题Mj=“. 这种过度近似基于基本谓词的子集，并且使用逐步保留来计算。图4中显示了抽象-重新排列算法。变量new和act分别存储当前未使用和已使用的抽象pred。最初act包含来自basis的谓词的子集0，new包含剩余的谓词（图4）。 首先，如果s02（[[']]act）通过调用nite-state来检查，calculusmodelc he c ker. 如果实际上欠近似满足，则通过推论4.4，M也满足，并且算法返回真（行（5））。接下来，我们检查是否为062（[[']]act）。如果超出预期的最大值满足“，则也由推论4.4，M不满足”和算法返回false（第（6）行）。否则（第（7）行），即s062（[[']]act）和M+s02（[[']]act），-calculus模型delc hecker返回一个coun的例子，抽象路的形式（见[12]）q0）+q1）+）+qn，其中q0是M +的初始状态。如果对于抽象路径，在具体的变迁系统中存在对应的路径，则我们得到具体模型检验问题的一个反例（第（8）-（10）行）。在这种情况下，算法返回false。这种检查需要一个现成的满足能力检查器，用于线性算术约束的布尔组合，如ICS [9]。在抽象反例是伪的情况下，存在最小索引k和具体路径y0））yk，其中y0是M的初始位置，并且对于所有i2f0; kg;yi2（qi），使得不存在从yk到yk +1的（具体）过渡，其中yk +12（qk +1）（行（11）-（14））。 我们选择一个最小集合从new中提取新的抽象谓词，使得从q k到q k+1的转换被消除（行（15）-（18））。这组新的抽象谓词是以这样一种方式选择的，9y1;y22SC：y12（qk）^y22（qk+1）^y1;y2保持。注意，具体化函数实际上依赖于抽象谓词的当前集合行为定理5.1（终止性、可靠性和完备性）设M是一个具有相应的 有限基的转移系统，L中的一个句子。然后图4中的算法总是终止。此外，如果它以真终止，则Mj=“”，并且如果结果为假，则M6j=“”。MoLler，Rue，Sorea235法fx= 0g算法：抽象和抽象输入：M，初始状态s0，'，基础？输出：模型检查查询Mj='的答案(1)选择0=f1;：;ig from;（2）新的：=n0;（3）act：=0;(4)回路（五）如果s02（[[']]act）然后返回trueM+（六）elseifs062（[[']]然后返回false(7)否则设（q0）+q1）+qn）是M+中的一个连续例子(8)如果存在路径=（y0）y1）yn）(9)使得y0=s0和yi2 （qi）对于所有0我n(10)返回false(11)否则，设k满足9apath=（y0）y1）yk）(12)其中y0 = s0，(13)yi 2 （qi）对于所有0我k和（14）8yk+12（qk+1）：yk;yk+1;（15）从new中选择最小0=f1;：;i g，使得（16）8y12（qk）;y22 2（qk+1）：y1;y2;(17)行动：=[f0g;(18)新的：=新n0(19)endif(20)endif(21) endloop见图4。 迭代抽象-重排序算法。证据 直接从 基础的完备性和定理4.3和3.7。2例5.2再次考虑图1中的定时系统，公式“= 9（tt Uatl2）”描述了永远不会到达l2的原理。 该系统的给定基为： 1; x 1; y 1; y 1; x > y; x yg.带有单个抽象谓词x = 0的初始过近似的转换系统如图5所示。转移系统M上公式的模型检验返回false，因为s0=（l0; x=y=0）62（[[']]Mfx=0g）。 该算法返回MMoLler，Rue，Sorea236例如（10;0））+（11;0））+（11;：0））+（12;：0），在图5中使用粗体线来强调。国家的具体化MoLler，Rue，Sorea237l2;0f;g01l0;0l1;0l0;：0l1;：0l2;：0图五. 图1中的定时系统的过度近似，0x = 0。这条抽象的道路如下。为了简化符号，我们表示配置的集合，例如f（l i）j l = l 1^（x）= 0 ^（y）0g由（l1; x = 0^ y 0）。（q0）= （l0;0）=（10; x = 0^ y 0个）（q1）= （l1;0）=（l1; x = 0^ y 0个）（q2）=（l1;：0）=（l1; x > 0^ y 0）（q3）=（l2;：0）=（l2; x > 0^ y 0）现在我们要检查在具体的转移系统上是否有一个对应的反例，即是否存在一条路径y0）y1）y2）y3，其中y 0; y1; y2; y32SC，使得y 02（q 0）; y12（q1）; y22（q2）; y32（q3），并且y 0 = s 0.如果公式F1：= 9 y0; y1; y2; y3 2 SC：y0 2（q0）^y1 2（q1）^y2 2（q2）^y32（q3）^y0）y1^y1）y2^y2）y3^y0=s0是有效的。在我们的例子中，F1是不满足的，因为在具体的转移系统上，在y