理论计算机科学电子笔记138（2005）101-115www.elsevier.com/locate/entcs（ω-）正则模型检验Ahmed BouajjaniLIAFA法国巴黎第七大学Axel Legay，Pierre Wolper阿克塞尔·勒盖皮埃尔·沃尔珀2，3，4Institut MonteFioreUniversit′edeLi`ege，Li`ege，Belgium摘要自从几年前这个话题出现以来，常规模型检查的工作主要致力于状态可达性和安全性的验证。虽然人们知道，活性属性也可以在这个框架内检查，很少有人做了相应的细节，并实验评估的方法。本文解决了这些问题的背景下，定期模型检查的基础上编码的状态，有限或无限的话。它计算出了在这两种情况下要使用的确切结构，并解决了由于无界配置的无限计算可能永远不会包含两次相同的配置这一事实而导致的问题，从而使循环检测成为问题。几个实验表明，该方法的适用性成功地进行。保留字：（ω−）正则模型检验，活性。1 电子邮件地址：abou@liafa.jussieu.fr2电子邮件：legay@montefiore.ulg.ac.be3 阿克塞尔·莱盖得到了F.R.I.A.的资助。4 电子邮件地址：pw@montefiore.ulg.ac.be1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.061102A. Bouajjani等人理论计算机科学电子笔记138（2005）1011介绍常规模型检查[3，5，6，9，14]是分析有限状态系统的一般方法，其中状态由单词表示，转换关系由有限状态转换器表示，可达状态通过在适当的加速技术的帮助下迭代此转换器来计算。考虑到框架的表达能力，这些加速技术不可能是完全通用和精确的，但在许多有意义的情况下，它们能够计算无限状态系统的可达状态的正则表示（或近似）。然而，计算可达状态并不完全是模型检查。对于安全属性，模型检查可以简化为状态可达性问题，但是对于包含活性成分的属性，可以做的最好的事情是将（线性时间）模型del-che-chinggproblem简化为Bu？hi自动机[10]的目标，这意味着检查重复可达性而不是可达性。如[3，16]所示，在常规模型检查的上下文中，这在概念上是可能的（当所考虑的转换器表示有限词的长度保持变换时），但到目前为止，相应的细节和语用学尚未得到充分解决。这样做是本文的目标之一。本文的另一个目标是提供一个通用的规范框架和通用的分析技术，涵盖了有限字配置的情况（对应于各种模型，如下推系统，FIFO通道系统，参数网络的相同过程，甚至整数计数器系统）以及无限字配置的情况（例如，允许推理操作实值变量的定时或混合系统）。对于一个无限状态系统，其状态是由有限（甚至是有限[6]）个词表示的为了定义这种计算的属性，人们可以选择在配置内（水平）或配置之间（垂直）移动。因此，人们自然会想到一个二维逻辑来描述这种计算的性质。然而，我们并没有把重点放在定义属性的逻辑的精细点上，而是选择集中在验证的计算方面，并使用有限（或无限）词自动机作为定义计算属性的基础。在我们正在考虑的计算中，单词自动机要么水平移动，要么垂直移动，显然两者都需要定义有意义的属性。人们可以考虑在两个方向之间任意交替，但在实践中，一个交替就足够了。虽然推广是可能的，但我们因此将我们的研究限制在根据垂直特性定义的水平特性上，这对于参数系统是有意义的，其中垂直切片对应于以下计算：A. Bouajjani等人理论计算机科学电子笔记138（2005）101103系统的一个组件;以及根据水平属性定义的垂直属性，这对于使用单词来编码队列内容或整数值的系统是有意义的[5，6]。对于这两种情况，我们充分地研究了如何增加表示系统转换的转换器，以使系统与属性相结合而产生的Bu？hi自动机具有一旦得到了布希自动机h的转换关系，通过计算这个关系的迭代闭包，找到配置之间的非平凡循环，并最终检查出现在这些循环中的配置的可达性，来检查自动机的非空当处理的系统，其配置是有限的话，其transitinelatio n ionislength-hurving，一个cepting计算ationg的heBuuchi自动机将始终包含相同的配置两次，因此一个可识别的循环。然而，当处理其长度可以增长或无限的配置时，很可能存在一个接受的布希自动机计算，其中相同的配置n可以同时应用。为了解决这个问题，我们寻找不一定相同的配置，但是在一个可能的计算也可能从另一个我们使用的限定的确切概念为此，我们象征性地计算出系统配置的仿真关系有趣的是，模拟关系的符号表示的计算实际上是一系列有限状态换能器的极限的计算，在常规模型检查的背景下引入的加速技术也可以用于计算。然而，在我们已经考虑过的几种情况下，这种计算在有限步之后收敛，这具有额外的优点，即保证了导出的模拟等价关系将配置集划分为有限个类，因此必须找到现有的接受计算，当模拟等价类的数量是无限时，情况可能不是这样最后，我们进行了一些实验，以确定在常规模型检查的纯自动机理论框架中自动验证无限状态系统的活性特性的可行性。参数系统的活性特性，使用整数变量的程序，和混合动力系统成功地检查。相关工作：有各种各样的早期工作对无限状态系统的活性性质的验证在[8，7，17]中，提出了基于结合抽象技术和有限状态模型检查的方法来验证参数网络的活性特性，104A. Bouajjani等人理论计算机科学电子笔记138（2005）101流程. 与这些方法相比，我们的方法不限于参数网络的情况下。最近，Abdulla et al.独立开发了一种类似于我们的方法，基于结合S1S和线性时间时序逻辑的特定逻辑[1]。然而，他们提出的技术是不同的，只适用于参数系统的情况事实上，他们发展的逻辑只能表达参数系统的性质，而不能表达例如计数器系统等无限状态系统的全局性质（例4.2给出了这样的性质的例子）。此外，他们的技术假设长度保持系统，并且他们既没有解决非长度保持系统的情况（例如下推系统，FIFO通道系统，计数器系统等），也没有解决ω-正则模型检查的情况，因此他们不能像我们一样处理例如定时或混合系统。在文献中的其他结果是基于自动技术的排名功能的合成。这些结果主要解决了某些类（无限状态）程序/扩展自动机的终止性检查问题[11、12]。所提出的技术利用了所考虑的数据域的特定性质，这些数据域主要是数值数据域，例如具有线性测试和更新的整数变量。虽然这些方法在特定情况下可能更有效，但我们工作的目的是提供通用技术，无论使用的变量和数据结构的类型如何，这些技术都适用。2预赛在这一节中，我们简要回顾一下本文将使用的基本自动机理论定义有限词上的有限状态自动机是一个元组A=（，Q，q0，δ，F），其中是一个有限字母表，Q是一组状态，q0∈Q是一个初始状态，δ：Q×→ 2Q是一个转移函数（如果自动机是确定性的，则δ：Q×→Q），FQ是一组接受状态。一个三元组（s，a，SJ）使得SJ∈δ（s，a）称为一个由a标记的变迁。 一个有限序列（词）w = a1a2.如果存在一个状态序列s0. .s k使得<$1 ≤i≤k：si∈δ（s i−1，a i）（对于确定性自动机，s i= δ（s i−1，a i）），s0 = q0，且sk∈F。集合被A接受的语言称为A接受的语言，记为L（A）。字母表上的无限词（或ω-词）w是从自然数到字母表的映射。ver的无穷多个词的集合表示为ω。一个Buüchi自动机在语法上与一个限定词自动机相同A的游程πA. Bouajjani等人理论计算机科学电子笔记138（2005）101105Bu-hi自动机A=（n，Q，q0 ，δ， F）onnω-w ordw是映射π：N→Q使得π（0）=q0，且对所有i≥0，π（i+1）∈δ（π（i），w（i））（非确定自动机）或π（i+ 1）=δ（π（i），w（i））（确定自动机）.设inf（π）表示在运行π中无限频繁出现的状态集合。如果inf（π）< $F<$f，则称游程π是可接受的。一个ω字w被接受如果一个不连续的广告在一个连续的运行中被删除，在W。 语言Lω（A）是由一个布赫自动机A所生成的，它是它所接受的ω-词的集合一个语言Lω是ω-正则的，如果它能被一个Bu？chi自动机接受. 通过布希自动机的并和不分，可以有效地计算，求补运算需要复杂的算法，不仅是最坏情况下的指数，而且也难以实现和优化。因此，我们将把自己限制在弱自动机[15]。对于一个布吕克型自动机A=（Q，q 0，δ，F），若A=（Q，q 0，δ， F），A =（Q，Q 0，δ，F），A =（Q，Q0，δ，F）.，Q m，使得对于每个的Q i，或者Q i<$F，或者Q i<$F =<$，并且在集合Q1，.上存在偏序≤。，Q m使得对于每个q∈Qi和QJ∈Qj，其中对于某个a∈ φ，QJ∈δ（q，a）（在确定性情况下QJ=δ（q，a）），Qj≤Qi.弱自动机是指一个连续的强自动机其图的组件仅包含接受状态或仅包含不接受状态。虽然不是所有的omega正则语言都能被弱确定性的Buechi自动机所接受，但它们在处理许多应用时是足够特别是，它们与整数和实数的一阶线性算术一样有表现力[4]，这允许处理例如时间自动机，线性混合自动机等模型，以及它们的整数计数器扩展[6]。此外，弱自动机在算法上也有优势：弱确定性自动机可以通过反转其接受和非接受状态直接得到补充;弱自动机存在一个简单的确定过程，从而产生具有确定性但一般不弱的Bu？chi自动机然而，如果所表示的语言可以被弱确定自动机接受，则确定过程的结果可以容易地转换为弱自动机[4]。3 系统模型，正则和ω-正则模型检验在本节中，我们介绍了本文中使用的基于自动机的系统编码我们采用常规模型检查的概念（[3]），用有限或无限（见[6]）的词来表示系统配置准确地说，106A. Bouajjani等人理论计算机科学电子笔记138（2005）101定义为三元组M=（φ，φI，R），其中• [1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19• φI是一组初始配置，由环上的有限（ω-）自动机表示;• R是一个转换关系，它由一个有限态（ω-）自动机在π× π上表示，它将被称为π上的转换器请注意，有了转换器的这个定义，长度保持的执行的配置。这是可能出现的较少限制，因为初始配置总是可以任意填充，并且可以使用一组初始配置包含所有可能的填充;然而，这种编码技术对活性属性的验证有影响（见第6节）。在有限字的情况下，系统的执行是在N上的相同长度的有限字的无限序列该模型通常用于表示参数系统[3]或具有整数变量的系统（[5]）。例3.1让我们考虑一个简单的例子，参数网络的相同进程实现令牌传递算法。每个进程可以处于两个状态T（具有令牌）或N（不具有令牌）中的一个，并且从左到右传递令牌的动作可以使用正则关系（（T，T）+（N，N））<$（T，N）（N，T）（（T，T）+（N，N））<$.在无限词的情况下（ω-正则模型检查[6]），系统的执行是一个无限词的无限序列该模型可用于包含整数和实数变量的系统，如混合系统。当处理无限词构形时，我们将限制转换器为确定性的Bu？hi自动机，如[6]所做的那样。到目前为止，（ω−）正则模型检验的工作主要集中在两个问题上：计算关系R的传递闭包R<$，以及计算给定初始状态集φ的像R<$（φ）。在这里，我们将假设我们有一种计算R和R（φ）的技术（参见[3，5，6，9]的例子这些技术），我们将展示如何验证活性属性可以减少到这些问题。4系统属性在本节中，我们考虑我们想要验证的属性的定义。我们考虑两类性质。第一节课研究全局系统的计算。此类属性可用于表示A. Bouajjani等人理论计算机科学电子笔记138（2005）101107属性的配置系统，如下推系统，FIFO通道系统，计数器系统，混合系统等第二类是面向参数系统，并首先检查系统的各个过程的计算也可以考虑两类性质中的性质的布尔组合这些组合通常用于在公平条件下表达活性属性4.1全局系统属性如果把配置看作一个整体--当它们表示实例数（整数或实数）、堆栈或队列内容等时，这是唯一合理的可能性--那么根据配置的属性来定义执行的属性是有意义的。定义4.1设M=（φ，φI，R）是一个系统，一个构形性质是一个集合copφ（分别为当考虑到在有限的话）。给定一组配置属性COP ={cop1，. ，copk}，全局系统性质是集合gsp_n（2 COP）ω，即COP的子集的无限序列的集合。执行σ = w0，w1，w2，w3. 满足全局系统性质gsp，σ| = gsp，if cop（w0）cop（w1）. ∈gsp，其中cop（w）={cop i∈COP|W| = cop i}。我们将讨论由Bu？chi自动机定义的全局系统性质和由有限字自动机表示的配置性质这个模型捕获了所有在线性时间时序逻辑中可表达的属性，使用配置属性作为命题。例4.2考虑一个处理两个整数变量x和y的系统。下面的性质Q[（x >0）（y=5）]是全局系统性质。4.2面向本地的系统属性这些属性只能在参数系统上检查，它们被用来表示这些系统的各个过程的活性属性在我们的模型中，参数系统的计算由相同长度的有限字的无限序列表示这些单词中的每个位置对应于一个过程，而执行中位置相同的字母的无限序列因此，我们使用以下符号和定义。定义4.3考虑执行σ = w0，w1，w2，w3... 系统M=（φ，φI，R）的解。第j个局部投影<$j（σ）是无限词w0（j）w1（j）w2（j）.. . ，其中w（j）表示作品w的第j个字母。108A. Bouajjani等人理论计算机科学电子笔记138（2005）101定义4.4局部执行属性是一个集合lepω。 局部执行性质lep由位置j处的执行σ满足，|= lep，如果σ_j（σ）∈lep.局部执行属性可以通过使用线性时态逻辑自然地定义，但我们将假设逻辑表达的属性已被转换为自动机[10]。定义4.5给定一组局部执行属性LEP ={lep1，. lep k}，面向局部的系统属性是一个集合losp k（2 LEP）k，即一组LEP子集的有限序列。一个执行σ满足一个面向局部的系统属性losp，如果lep（1（σ））lep（2（σ））. lep（n（σ））∈losp，其中n是σ中单词的公共长度，lep（i（σ））={lepi ∈LEP|i（σ）|=lep i}。例4.6考虑例3.1中定义的参数系统。当一个进程处于状态N时，它最终会移动到状态T（线性时间时序逻辑中的Q（NT）），这是一个局部执行属性。这个属性对每个进程都适用，这就是一个面向局部的系统属性。4.3局部系统与全局系统性质的布尔组合系统的活性特性有时需要表示为面向局部/全局系统特性的布尔组合通常，在参数系统中，这是对应于模式的属性的情况：在某些公平性条件下，某些活性要求必须成立。在其他类型的系统的情况下，例如操纵顺序数据结构（下推系统、FIFO通道系统、具有链表的程序、数组等）或数值变量（整数计数器、实值时钟、秒表等）的系统，公平性条件和活性要求都是全局系统属性，因为面向局部的属性在这些情况下没有意义5保长系统的检验性质在本节中，我们将描述如何在长度保持系统上验证全局和面向局部的由于篇幅限制，布尔组合的验证仅在论文的完整版本中描述[13]。A. Bouajjani等人理论计算机科学电子笔记138（2005）101109一一5.1检查全局系统属性为了检查长度保持系统M=（k，I，R）满足在一组配置属性COP=上定义的全局系统属性gsp{警察1，. cop k}，我们检查不存在M的执 行 ，满足一般服务条款。 这是通过在这样的情况下增加过渡系统M来它的执行只是那些定义AGSP的自动机的运行。增广变迁系统被定义为Ma=（Ia，Ia，Ra）。Ma是通过在初始系统M和自动机A <$gsp之间取一个“特殊”乘积而得到的这个结构中有很多技术要点，由于空间限制，我们将其推迟到完整版本（[13]）。在构造Ma之后，下一个步骤是检查是否存在为自动机A<$gsp接受的转移系统Ma的运行。这是通过检查是否存在一个接受配置（即，自动机A<$gsp处于接受状态的配置），从自身可到达的，以及从初始配置可到达的这个条件-这确实是必要和充分的，因为系统是长度保持的，这意味着人们无法找到一条永远不会访问同一配置两次的无限路径检查上述条件的计算可以组织如下。设accept是接受配置的集合（即，其中Agsp处于接受状态的增广系统的配置），设R+是Ra的非自相关传递闭包，Id是恒等关系。则存在非平凡环的增广构形是在R+R_Id的域中的增广构形（其中R+=R_H_R）。这种可达到的接受配置因此，R（Ia）接受域（R+Id），a a如果这个属性是空的，那么这个属性就被满足了5.2检查面向本地的系统属性检查系统M =（lep，I，R）满足在一组本地执行属性LEP ={lep1，.上定义的面向本地的系统属性。lep k}，通过搜索满足否定的系统的执行来完成财产的损失我们通过将系统M扩充为系统M，Ma=（Ra，Ia，Ra）.设TR=（S× R，SR，s0R，δR，FR）是定义M的转移关系R的有限自动机，A<$losp=（2LEP，S<$losp，s0 <$losp，δ<$losp，F<$losp）是接受不满足losp的有限序列的有限词自动机，Alepi =（S，Sle pi，s0le pi，δle pi，Fle pi）对 于 1≤i≤kbe是完全的（但不是110A. Bouajjani等人理论计算机科学电子笔记138（2005）101我需要一个确定性的）Bu？c有限阶自动机来定义局部执行性质，并且A？lepi=（，S？lepi，S？lepi，δ？lepi，F？lepi）是用于否定这些性质的一个自组织数据后者是需要的，因为自动机类似于非确定性，在接收计算中具有y的情况并不表示相应的属性不成立。因为，先验地，我们不知道哪个局部执行属性将被自动机Alepi的构造的两个位置所满足， 和每个位置都必须运行一个程序。所以，我们需要扩大我们的行动范围以这种方式，配置中的每个位置也由Alepi和A<$lepi的状态标记。此外，对于配置中的每个位置，eachpp ppi∈LEPmightatatied（Alepi hanaceptingrun），或mig htnotasatifiedd（A<$le pi 有一个接收运行）。我们还通过用2LEP的元素标记每个位置来表示这些事实，对应于-这就是我所追求的幸福。此标签将在配置之间保持不变，并使我们能够运行自动机A<$losp.下一步骤是检查是否存在传输系统Ma t i 的 运 行 ， 该 传 输 系 统 MatiisaceptingforsuitableatomataAle pi和A<$le pi。确切地说，在配置中的给定位置j处，自动机Ale pih的运行是接收iflepi∈lep j，并且A <$le pih的运行是接收if lep i/∈ lepj，其中lepj是标记该位置的2个LEP的元素。我们面对的是一个没有问题的移动设备，但服务器是布吕奇条件，即， 一个推广的dBu？c？hi条件。为此，我们利用了这样一个事实，即一个给定的Buchiatomaton具有一个接收运行xactly，而in具有一个顺序通过每个接收集的接收运行。我们现在定义Ma增广字母表是a=1≤i≤kSlepi×1≤i≤kS<$lep× 2 LEP× 2 LEP× {reset，noreset}。在字母表中引入了LEP的两个子集：第二个子集用于记住检查属性lepi（或<$lepi）的合适自动机是否已经看到接受状态;标记的最后一个组件指示是否这些子集中的第二个刚刚被重置为非。增强型换能器，TRa，canbe定义为follows。• 它的字母表是a×a• 它的成立和接收成立分别为SRa=SR和FRa=它的初始状态是s0Ra=s0R。A. Bouajjani等人理论计算机科学电子笔记138（2005）101111阿阿阿阿阿阿• 转换关系定义为（假设非确定性自动机）sJ∈δ（s，（（a，s，...，s，s，...，S，lep，lep，ρ），RaRa111岁K1第11章¬Æepk11F11（a2，s12，.， sepk 2，sep12，.， s<$pk 2，lep2，lepF 2，ρ2）我的· sJR∈δR（sR，（a1，a2））和slep2∈δlep（slep1，a1），s<$lep2∈δ<$lep（s<$lep1，a1），对于1≤i≤k，· lep1= lep2，· 若lepF1= LEP，则lepF2=零且ρ2 =复位，或lepF2=lepF1且ρ2=不复位，否 则 ， lepF2=lepF1<${lepi∈lep1|slepi1∈Flepi} <${lepi/∈lep1|s<$lepi1∈F<$le pi}和ρ2=noreset.请注意，在一个给定的位置，当所有必需的接受条件都已满足时，是否重置的选择是不确定的。• 接受态的集合是FR。Ma的初始构型的集合是以下形式的那些（a1，s0lep1，.，s0lep k，s0<$lep1，.，s0<$lep k，lep1，sl，noreset）（a2，s0lep1，.，s0lep k，s0<$lep1，.，s0<$lep k，lep2，，noreset）...（a n，s0lep1，. ，s0lep k，s0<$lep1，. ，s0<$lep k，lepn，lep，noreset），其中w = a1a2a3.. . a n是I中的一个词，lep1lep2. lepn.瘦的，瘦的|=<$losp.如果我们将接受配置定义为对于每个位置标签的最后部分ρ被重置的配置6，则可以通过检查是否R（Ia）接受域（R+Id），a a为空.在这种情况下，财产是满意的，否则不是。6非保长系统和无穷词在本节中，我们考虑检查非长度保持的有限字系统和无限字系统的全局系统性质的问题。5这样就可以等到每个位置满足所需的验收条件，然后在所有位置同时重置112A. Bouajjani等人理论计算机科学电子笔记138（2005）1016，这意味着所有相关的自动机都看到了自上次“重置”以来的接受状态。A. Bouajjani等人理论计算机科学电子笔记138（2005）101113系统.如第3节所述，为了计算可达配置，非长度保持系统可以通过使用填充来处理为长度保持系统因此，我们仍然可以使用5.1节的构造来获得检查全局系统性质的增广系统Ma然而，无限计算将总是重复访问相同的配置不再是真的，我们必须调整5.1节中给出的标准。用有限的话来说，情况是类似的：结构基本上保持不变，尽管我们必须处理一些额外的技术困难，因为构形是有限的（详见[13]），我们还必须适应检查循环的标准。由于我们不能将决定Ma是否具有无限接受计算的问题简化为找到可达接受循环的问题，因此我们的方法是搜索可达配置c，从该配置c可以非平凡地到达某个配置cJ，使得（1）从c到cJ访问A<$gsp的重复状态，并且（2）cJ具有至少相同的计算，路径为C。为了检验条件（2），我们实际上检验了一个更强的条件，即cJ必须模拟c。在下文中，我们将只考虑有限的话，但这些结果可以很容易地转换为限定词格定义6.1Ma的构形上的最大模拟关系与集合COP中的配置属性相容的是关系S，其被定义为以下关系的递减序列的极限，其中w|表示单词w∈S0={（w1，w2）∈<$ω×<$ω|ω）= ω p（ω2|）}|Σ)}a aSk+1={（w1，w2）∈ Sk：<$WJ. （（w1，WJ）∈ RaWJ. （w2，wJ）∈Ra<$（wJ，wJ）∈Sk）}1 1 2 2 1 2Ma上与之相容的最大模拟等价COP是r<$S<$=S<$S−1。首先，我们有以下结果：命题6.2设accept是所有增广构形的集合，其中自动机A<$gsp处于某种接受状态。然后，可以看出，如果以下条件成立，则M a具有可接受的无限计算：(1)R<$（Ia）<$整环[（（R<$$>（<$ω×accept））<$R+）<$S]<$a a a a现在的问题是计算关系S。 注意，S0可以被直接定义为正则关系，并且Sk+1，对于每个 k≥0，用布尔运算和投影（对应于存在量化）根据关系Ra和Sk因此，给定表示Ra和Sk的换能器，可以有效地计算a114A. Bouajjani等人理论计算机科学电子笔记138（2005）101表示Sk+1的换能器。主要问题是S的迭代计算是否终止。如果计算终止，则S具有有限指数模拟，即，有限个等价类。这意味着系统的每一条无限路径必须无限频繁地访问一些等价类。因此，我们得到了以下结果（在完整版本中有详细说明[13]）。定理6.3假设系统M a有一个有限指数模拟。然后，M a有一个可接受的无限计算，当且仅当条件（1）成立。在Ma没有有限指数模拟的情况下，我们可以使用S的近似。让我们首先考虑上近似的情况。命题6.4如果存在k≥0，使得R<$（Ia）<$Domain[（（R<$$>（<$ω×accept））<$R+）<$Sk]=<$a a a则系统Ma没有无限接受计算，这意味着M A满足属性GSP。较低的近似也可以用于确定系统是否不满足某个属性。命题6.5让LS。检查所R<$（Ia）<$整环[（（R<$$>（<$ω×accept））<$R+）<$L]/=<$a a a允许我们推导出系统M a具有无限可接受计算，这意味着M a不满足性质gsp。为了计算S的下近似，我们进行如下：不是计算关系（Si）i≥0的递减序列，而是计算它们的否定（<$Si）i≥0的递增序列。这样做的好处是，我们可以在迭代计算扩展技术的每一步应用像[6]中定义的那些，它允许我们加速定点计算，在许多情况下，使其终止。然后，计算关系序列实际上是ω-正则关系（Ui）i≥0的递增序列，使得对于每个i≥0，Ui<$$>Si，因此，该序列U的极限一般是<$S的ω-正则上近似。这意味着集合<$U是S的下近似。请注意，[5，6]提供了（足够的）条件，允许我们检查计算集是否精确。7实验结果本文提出的技术和算法已在几个例子中进行了测试，涵盖不同类别的系统和属性。细节A. Bouajjani等人理论计算机科学电子笔记138（2005）101115关于所考虑的模型和相应的实验报告在完整版（[13]）。我们在下文中给出这些结果的简要概要首先，我们考虑了参数网络的几个例子，对应于互斥协议，包括面包店算法和令牌环协议。对于这些系统，我们已经能够自动检查livelock自由属性。接下来，我们已经能够检查操作整数变量的（多循环）程序的终止性或非终止性最后，我们解决了验证一个系统操纵计数器以及（连续时间）时钟的活性属性的问题。我们考虑的一个例子是IEEE 1394根竞争协议的简化模型引用[1] P. A. Abdulla和B. Jonsson和M. Nilsson和J. d'Orso和M. Saksena，S1S + LTL。[2] A. Bouajjani和A. Collomb-Annichini和Y. Lakhnech和M. Sighireanu[3] A. Bouajjani 和 B. Jonsson 和 M. Nilsson 和 Tayssir Touili ， Regular Model Checking ，Proceedings of the 12th International Conference on Computer-Aided Verification（CAV[4] B. Boigelot和S. Jodogne和P. Wolper[5] B. Boigelot和A.Legay和P.Wolper，Iterating Transducers in the Large，Proc.第15届计算机辅助验证国际会议，美国博尔德，计算机科学讲义，2003年第2725卷，第223[6] B. Boigelot和A.Legay和P.Wolper，Omega-Regular Model Checking，Proc.第十届国际Conf. on Tools and techniques ，Barcelona ， Spain ， Lecture Notes in Computer Science ，volume 2988，year 2004，pages 561[7] Y. Fang和N.Piterman和A.Pnueli和L.Zuck，Liveness with Incomprehensive Ranking，Proc.10th Int. Conf. on Tools and Techniques，Barcelona，Spain，Lecture Notes in ComputerScience，volume2988，year，pages 482[8] K. Baukus和Y.Lakhnech和K.Stahl，《参数化网络的通用性质》，FTRTFT[9] D. Dams 和 Y. Lakhnech 和 M. Ste Escheren ， Iterating Transducers ， Proceedings 13thInternational Conference on Computer Aided Verification （ CAV ） ， Lecture Notes inComputer Science，2001年第2102卷，第286[10] M. Y. Vardi 和 P. Wolper ， Automata-TheoreticTechniquesfor ModalLogicsofPrograms，Journal of Computer and System Science，第32卷，第2期，第183-221页，1986年[11] M. Colon和H.证明程序终止性的实用方法。第14届国际计算机辅助验证会议，哥本哈根，丹麦，计算机科学讲义，2404卷，2002年，442-454。116A. Bouajjani等人理论计算机科学电子笔记138（2005）101[12] D.Dams和R.Gerth和O.Grumberg ， 用 于 自 动 生 成 排 名 函 数 的 启 发 式 算 法 ， WAVe00 会 议 录 ， URL ：citeseer.nj.nec.com/article/dams00heuristic.html。[13] A.Bouajjani andA.LegayandP.Wolper ， HandlingLivenessPropertiesin （ ω- ）RegularModelChecking：Fullversion，TechnicalReport，URL：http://www.montefiore.ulg.ac.be/ legay/WWW/papers/infinity04.ps.[14] Y. Kesten和O.Maler和M.Marcus和A.Pnueli和E.Shahar，Symbolic Model Checking withRich Assertional Languages，Proceedings of 9th International Conference on Computer-Aided Verification（CAV[15] D. E. Muller和A. Saoudi和P.E.李文，《自动机理论与应用》，北京大学出版社，1986年。[16] A. Pnueli和E. Shahar[17] A. Pnueli和J.Xu和L.Zuck，Liveness with（0，1，in finite）-Counter Abstraction，Proc.第14届国际计算机辅助验证会议，哥本哈根，丹麦，计算机科学讲义，2404卷，2002年，107-122。
我的内容管理
展开
