时态逻辑性质检验：tableau构造在模型检查及自动机理论中的应用

网址：http://www.elsevie r. n l/l oc ate/en tcs/vol um e55. ht ml 19页关于时态逻辑性质M.C.W. Geilen1电气工程系信息通信系统科埃因霍温理工大学荷兰埃因霍温摘要时态逻辑是描述反应式程序正确性的重要工具随着时态逻辑模型检查器的出现，它已成为并发和反应式系统验证的重要辅助工具。在模型检查中，时序逻辑属性是针对工具的建模语言中表达的模型进行验证的此外，模型检查技术可用于测试实际实现或验证系统的模型，这些模型过于详细，无法通过模型检查器进行分析，例如通过模拟。tableau构造是一种算法，它将时态逻辑公式转换为nite-state自动机，该自动机精确地接受公式的所有模型。 它是检验公式是否满足的关键因素，也是自动机理论模型检验方法的关键因素。tableau构造的效率的一个改进是on-the-y版本的开发在本文中，我们提出了一个特定的tableau结构的增量分析过程中的执行痕迹测试，模拟或模型检查。自动机构成了监测器的基础，该监测器检测特定种类的好的和坏的压力，即那些对被调查的财产有信息的压力。我们详细介绍了监控器的结构，并证明了它的正确性。1引言在[11]中引入的时态逻辑是一种流行的形式主义，用于表达反应和并发系统的动态特性。当系统的抽象是nite-state时，模型检验过程可以自动地验证其正确性。tableau构造是一种将时态逻辑公式转换为nite状态自动机（可能在nite中打开）1 电子邮件：M.C.W. tue.nlc2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2单词），它精确地接受公式的所有模型。模型检测的自动机理论方法（[10，13]）依赖于tableau算法将时态公式转换为模型行为的观察者。在实际需求的驱动下，tableau构造正在不断改进和重新实现（例如[7，3，5]）。其中一个改进是开发了画面结构的y版本。一般来说，这意味着Tableau自动机是以一种懒惰的方式构造的，根据需要生成状态和转换。模型检测在自动验证真实系统（模型）的正确性方面获得了声誉。与此同时，人们认识到，类似的技术也可以以其他方式应用。人们不仅可以使用它们来验证正式的抽象模型，还可以用于实际的软件实现或详细的仿真模型，并分析它们在运行时的行为，以获得所需的正确性。这样做的一个特殊原因是为了对抗状态空间爆炸的影响，这使得传统的验证技术不能很好地扩展。传统模型检查器的一个重要方面是通过系统的状态空间进行系统搜索。在运行系统的验证过程中，这种对状态空间探索的控制是不可用的。回溯是不可能的，或者代价极高。因此，用于分析运行系统所暴露的行为的监视器必须能够增量地和确定性地分析行为。此外，由于周期未被发现，因此无法直接推断夜间痕迹的性质。由于这个原因，运行时模型检查需要修改验证方法。本文讨论了这种修改。本文件在本文中，我们提出了（自动）建设的运行时监控器的线性时序逻辑表示的属性。这些监视器允许（同时）检测（信息）好的和坏的执行的prexes，因此可以用来监视时间逻辑属性递增和确定性在运行时。我们证明了在nite状态序列上属于一个tableau自动机的转移系统，信息好的prexes的nite状态自动机和信息坏的prexes的nite状态自动机（几乎）重合。自动机Der只在验收条件下，我们展示了如何将它们组合成一个单一的监视器。相关工作这项工作建立在Kupferman和Vardi的工作基础上[9]。鉴于他们的主要目标是使用交替自动机简化安全特性的模型检查过程，我们研究了使用他们的信息索引概念来构建tableau自动机和运行时监视器，3特别的。我们的重点是构造nite状态，并最终确定nite状态自动机。”[9]又说：“前。xes和复杂性的结果。其他相关的工作包括论文[2，8]，其中给出了一个更务实的处理运行时时态逻辑验证。文[2]使用了构造表自动机的基本展开原理，其主要缺点是在模拟时直接操纵公式，效率不高。同样在[8]中，讨论了在System-C描述的模拟中LTL性质的观察。公式解释nite状态序列，并给出了一个三值的解释。关于y轴上的画面构造的工作包括[7，4，3]。论文综述本文件的结构如下。第二节介绍了一些常用的词典，并特别介绍了一些信息词典。在第3节中，我们讨论了一个范式，基于信息量的概念，这将形成tableau结构的核心。第4节讨论了画面的构造。如何从这些表格中生成运行时监视器是第5节的主题，在那里它也被证明是正确的。第6节结束。2有 限 的 和 不 完 整的词一个字母表上的单词w= 012：n1（长度为n）是一个符号序列，来自：word）w=012：在字母表上是来自的符号的不间断序列;w（k）表示k和wk指的是到尾部kk+1k+2：. 我们使用后一种符号来表示其他类型的序列也是。一个字符串的连接 nite单词w1和a 夜间或在nite字中，w2表示为w1w2。 一个nite字w1被称为一个prex一个nite或nite字w2，如果有一些字w3，使w2=w1w3。对于一个集合w，j wj表示该集合中的集合的数量。 F或一个无穷维函数，在f（w）中表示该函数在无穷维中的符号。一组单词被称为语言。有限状态自动机让字母表是一组符号。一个标号迁移系统L =hQ;Q0;V;Q0由一个迁移集Q，一个初始位置集Q0Q，一个映射V：Q！2用字母表中的一组符号和一组边的集合来标记每个位置。 管路描述通过转换系统的路径。它通过记录位置的顺序来提供过渡系统在任何时刻的位置。一个标记转移的游程S_L=hQ;Q0;V;V_i是位置q（k）2 Q的（nite或in nite）序列q，使得 对 于 所 有 k 0 （ 如 果 q 是 nite ， 则 k< j qj1 ） ， 存 在 边 （ q（ k ） ;q（k+1））2n。 在这种情况下，我们还可以说q是从位置q（0）开始的游程，或者简称为q（0）-游程。 如果q（0）2 Q 0，则称游程q为初始游程.4一个字w 运行Q 长度相等，q 是一个运行为w (orW 匹配q）如果2对所有k 0，w（k）2 V（q（k））.一个nite状态自动机A=hQ;Q0;V;n; fiov由一个标记的转移系统和一组nal位置组成。自动机A接受一个nite字w（长度为n），如果它有一个初始运行q的w结束在一个nall ocation（q（n1）2f）。A（基因）Buchi自动机A=hQ;Q0;V; Fiover另一方面是一个在nite上的自动机，它由一个在上的标号转移系统和一个接受集fQ的集合F组成。A广义Buchi自动机Aac接受一个initewordw，如果它有一个初始运行Q 对于w因此，对于每一个f2F，在f（q）\f6 =？. 或夜间状态自动机或Buc在自动机A中，A的语言L（A）是它接受的所有单词的 集合 。线性时序逻辑我们使用线性时态逻辑的标准定义，并假设存在原子命题的集合Prop。LTL的语法由以下文法（p 2 Prop）给出：：：= true j p j：j1_2JJ1U2：我们让"，“0，”0，1，“1，2，”2等的范围超过LTL。 我们用cl（'）表示'的子模闭包。在其余部分中，我们使用运算符w.r.t. 否定（假=：真，'1^'2=：（（：'1）_（：'2））和'1V'2=：（（：'1）U（：'2），以将否定推向内部，直到它们只出现在原子命题前面，并以正范式编写公式。我们将把公式与相应的公式用正式正规形式3. 而且如果是一组公式，我们写V 来表示这些公式的结合，我们写j=以表示j= V。满足"for mula“的状态序列的语言P”称为用“yLTLfor mula”表示的p p语言。某些属性可以被定性为安全属性（声明“某些不好的事情永远不会发生”）或活性属性（声明“某些好的事情最终会发生”）。一个性质P是一个活性性质，如果对于每个尼特状态序列存在一些非稳态序列0，使得02 P（尽管其他定义也是可能的[1，12]）。财产是一个安全性，如果每个在夜间状态序列2=P，有一个前x0这样00 02=P对每个状态序列0 0. 后一种前x称为坏的前X ;前X对于属性P，如果没有状态序列0，使得02P。另一方面，一个属性P的好的prex是一个prex，这样，对于每个0、02P [9]。2 由于位置是用符号集标记的，因此单个游程通常对应于一组单词。53 使用cl（：）=：cl（）而不是cl（：）=：[cl（）使cl对公式的表示不敏感。6定义2.1 [9]一个nite词u2被称为语言L的好前缀x！ 我为每一个在nite字w2！，uw2L.类似地，对于语言L i，u被称为b ad p re x，对 于 每个nitewordw2！，uw2=L. 2本文讨论了用LTL公式表示的安全特性的验证问题，但并不是所有的安全公式都是相同的。文献[9]根据安全公式的性质，将安全拥有. 如果一个前x故事”[9]为什么公式适用于每一个在夜间状态序列，这是一个前x。 这一点在下文中作了明确说明。 有意安全的公式是对于其中非常坏的PREX是信息的多个用户（例如， 2p），一个意外安全公式是一个并非有意安全的安全公式，但它的所有违反它的状态序列确实有一些信息坏前缀x（例如2（p_（q^：q）。对于mula的病理安全的ty是对于具有违反它的计算而没有任何信息性坏前缀x的mula（例如（（2（q_23p））^（2（r_23：p）））_2q_2r，来自[9]的示例）。如果一组公式是“信息性的”，即该组公式中的每一个复合公式都得到一个或多个直接子公式的支持，则称该组公式是局部信息性的。这些公式一起构成了一个解释，为什么一个要求是成立的。 如果一个集合包含公式“1^”2，那么它也必须包含"1“和”2“来证明这一点。 类似地，如果一个集合包含“1U”2，那么它也必须包含“1”或“2"（这仅适用于当前状态，不包含”2“会导致对下一时刻成立的形式的额外约束）。 在本文的其余部分，我们让范围超过套LTL公式。定义2.2一套公式的局部信息，如果return2;如果“% 1_”%2% 2，则“%1% 2或”%2%2 ;如果“% 1^”%2，则“%1%2和”%2% 2;如果“1U”22，则“12或”22;如果“1V”22，则“22。局部信息性约束了需要对特定状态序列保持的公式然而，在Until或Release操作符的情况下，可能还需要对状态序列的其余部分施加约束（例如，如果集合包含'1U'2和'1，但不包含'2）。 如果一个Until或Release公式的真值直接从集合中的其他公式得出，那么这样一个集合对于那个Until或Release公式来说被称为平凡的（如果集合包含both'1U'2和'2，或者bot'1V'2和'1 ）。否则，它被称为非平凡的。（非）平凡集将发挥重要作用的tableau建设，因为它们构成的状态序列的其余部分的约束，从而确定“时间信息的继任者”。7定义2.3一套公式的值对于如果"1U"22和“22='1U'2;，letNext（'1U'2）=对于mula'1V'2的释放，如果'1V'22且'12=，则令Next（'1V'2）='1V'2;对于mula'，如果'2，让Next（'）='。2公式集合0是公式集合的时间信息后继者，如果对于每个公式，使得对于，0是非平凡的，则0包含Next（）。另一种表述时间信息性的方法是，对于要成为的时间信息后继者的0，它必须至少包含由确定的某些公式。 这是由以下定义捕获的。定义2.4设为一组公式。然后，时间信息性约束的集合Next（）是以下集合：fNext（）j2使得对g来说是不平凡的：0是的时间信息后继者 if Next（）0的情况。 这表示为 ！0的情况。2在一些证明中，我们使用Next（1;2）表示fNext（）j 22，则1[2]是非平凡的f或g。例如，我们已经知道，！ fpUq;q g和fpUq;qg！什么？但不是fpUq;pg！ fp g而不是fqg！ fp g. 我们现在可以定义信息好（坏）前x的概念。[9]第四节：如何使用是 尼特状态序列。为"i存在一个长度为n +1 j j + 1的模集合的集合的集合序列IS2（2LTL）'2IS（0）;IS（n）=？;对于所有0在和2 IS（i），如果是一个原子命题p，则p2（i）;如果是一个平衡的原子位置：p，则p2=（i）;IS（i）是本地信息;IS（i +1）是IS（i）的时间信息后继者。2我们称这样的序列为信息序列。 如果这样一个信息序列存在，它告诉我们为什么'对pre x.......................................................................It的任何扩展都成立指出了什么公式在前x的什么时刻成立以及为什么成立。由于IS（i）在某个点为空，这个推理是完整的，因此适用于pre x的任何扩张。例如，如果1_2、（一）、（二）、84 我们根据我们的局部和时间非信息性的概念重新表述[9]的定义。9信息性要求，12 IS（i）或22 IS（i），它告诉我们，1_2对i的任何扩展（从状态i到结尾的部分）都 成 立 ， 因为至少有一个1和2对于i的任何扩展都成立。如果1U22 IS（i），12IS（i），且22=IS（i），则根据时间信息，1U22 IS（i + 1）. 这意味着，1U2必须持有任何延长因为1对i的任何扩张成立，1U2对i + 1的任何扩张成立。 因为IS（n）=？这样的推理不 依赖于状态序列中超过位置n的部分。它是完整的 ， “ 讲 述 了 整 个 故 事 ”[9] 。 因 此 ， 对 于“if it is informativelyfor”，是信息好前缀x，并且对于“ifitisinformativelyfor：”，是信息坏前缀x。3信息范式线性时态逻辑的（On-the- Y）表结构通常使用重写过程引入，该过程将公式重写为“析取时态范式”，以便将对当前状态的约束与对状态序列的其余部分的约束分开[7，4，3]。在本文中，我们介绍了一种基于信息量的在y的tableau建设。注意，虽然这种结构并不完全相同，但它与这种结构非常相似。在对应于传统的上的y表结构的析取时间范式，我们定义了一个“信息范式”。定义3.1一个LTL公式集合的集合是信息范式，如果每个集合都是局部信息的。我们现在介绍一些重写规则，将任何集合转换为范式。在重写规则中，我们将公式集合的集合表示为公式集合的一对hNew ; Oldi（我们称它们为项）的集合，以便区分已经处理的公式（Old）和仍然需要处理的公式（New）。规则在图1中呈现，其解释如下。 考虑一组[fh]新[fg;旧[g]项。表中Caseeld与LTL公式的形状一致的行确定如何重写集合。定义3.2（信息性的）范式过程从一组公式开始它维护一个项hNew;Old i的集合n，该集合被初始化为0=fh;？IG. 然后，只要表1中的某个导出规则适用，则将规则应用于n以获得n+1。当对于某个k 0没有更多的归约规则应用于k时，该过程的结果是集合f旧j h？;Old i2k g.这是很容易表明，该程序终止，并在k中的所有条款，然后的形式h？;ii对于某组i的for mula。 根据从New中选择项和公式的顺序，可以获得不同的范式。在续集中，我们假设存在一个10情况[fhNew[fg;Oldig简化为：1= false2= true3 =p4 =：p5 =1_26 =1^27 =08 =1个U29 =1V2[fh新;旧[fgig[fh新;旧[fgig[fh新;旧[fgig[fh新[f1g;旧[fgi;h新[f2g;旧[fgig[fh新[f1;2g;旧[fgig[fh新;旧[fgig[fh新[f2g;旧[fgi;h新[f1g;旧[fgig[fh新[f1;2g;旧[fgi;h新[f2g;旧[fgig表1本地信息化程序一个确定性过程NF，它为任何给定的形式集计算特定的规范形式。 我们使用NF（'）来表示NF（f' g）。引理3.3设是一组LTL公式。然后，NF（）是信息范式，并且此外，如果是状态序列，使得j=，则存在集合02NF（），使得（i）j=0，（ii）1j=Next（0），(iii) 对于每个Until公式='1U'22使得j='2，'220.证据0是局部信息的事实可以通过集合n上的不变量来表示，该不变量声明n中的项hNew; Old i是局部信息的w.r.t.旧的公式。 (This意味着本地信息的被解释为：“false2=Old”和“if2Old，t h e n ：2Old [New”。当过程结束时，所有公式都在Old集合中，NF（）中的集合是局部信息。第二部分使用不变量证明存在项hNew; Oldi 2n使得（i）j=New[ Old，（ ii ） 1j=Next （ New;Old ） 和 （ iii ） 对 于 每 个 U ntil ， 对 于mula=“1U”22Old，使得j=“2，”220。2例如考虑公式3p=trueupp的L TL。 根据规范形式程序，真Up的重写过程如下进行（我们写1）2来表示2是通过程序中的一个或多个步骤从1获得的）。fhftrue U pg;？ig）fhfpg;ftrue U p; gi; hftrueg; ftrue U11pgig）fh？;ftrueUp;pgi;h？;ftrueUp;truegig12New：=NF（'），Q：=？，Q0新6=？做让2新新：=新nfgQ：=Q[fg对于每个02NF（下一个F：：=新，新（））做：=新的[：=f0？G1322新的=F[f（;0）g，如果02=Q，则NewododFig. 1. Y轴上表自动机的位置和边的构造算法正规形式表明有两种方法来证明真实的Up成立。要么证明p成立，要么证明真成立（triv- ial）并且（由于Next（ftrueU p; trueg）= ftrueUpg）真Up在下一时刻成立。复杂性我们可以证明，范式过程NF（）的最坏情况复杂度是O（2 n），其中n =Pj j.因为在每一步，PJ J在减少中，新的术语取代了hNew ; Oldi，并且它最多被两个新术语取代。如果我们进一步知道每个2是一个或多个矩阵的元素，则证明了NF的复杂度为O（2j'j2）. 在这种情况下，更好地选择用于约简的f（选择最大的用于最小值的f）将复杂度降低到O（2j，j）。这可以通过考虑在从初始项hNew; i到最终项h？对于mula2cl（“）的旧路径最多可以用于约简一次，因此这样一条路径的长度最多为j'j，并且所应用的约简的总次数为O（2j'j）。4Tableau构建144.1Tableau算法本文在前一节所介绍的规范形的基础上，构造了一个关于m ula的n L TL的表自动机。它的构造与[7]的构造密切相关。然而，接下来的公式是隐式而不是显式表示的。在正规形项的集合中可能出现的公式的数目被限制为“的有规子公式”。LTL公式的表自动机是按以下方式计算的。151p2图二、公式23p的表自动机示例定义4.1设为一个LTL。表自动机A'of'是字母表2Prop上的自动机hQ; Q0;V;Fi通过图1中描绘的程序计算1 〇阳离子（Q）、初始1 〇阳离子（Q0）和跃迁（Q 0）。 位置q2 Q是LTL公式的集合;V（q）=f22Propj8p2Propp2q）p2i：p2q）p2=G. 也就是说，用与q中的原子命题和被否定的原子命题一致的所有状态来标记位置q;对于每一个Un，F都是连续的，直到f或mula='1U'22cl（'），设f=fq2Qj2q）'22q g.例如如果我们假设公式23p=falseV（trueUp）并应用tableau算法，我们就得到了图2中表示的自动机。只描述了位置中的原子命题 位置1是集合f23p;3p;p g，位置2是集合f23p;3p;真g。 初始位置由一个小箭头表示，该小箭头不源自导致初始位置的任何位置。 只有一个接受集f3p，其中的l o阳离子用一个额外的圆围绕它们表示。复杂性由于该表的所有子集都是cl（i）的子集，因此最多有2个不同的子集。为了验证，对Next（）应用规范形式处理. 本条例草案显示为第3条第O（2j'j）款。因此，该算法的复杂度为2O（j'j）.4.2正确性在这里，我们给出一个证明画面结构是正确的简单草图，即. 对于m ula的nyLTL，表自动机“精确地接受满足”的那些状态序列。基于信息约束的算法与文献[7]的算法非常接近，证明也与文献[4，7，3]的证明类似。定理4.2设L是一个LTL公式，设A是自动机上的C或R关系表。 则对于每个状态s equen c e，A'aceptsij='。16这个定理是由下面的引理4.4和4.7所表示的构造的可靠性（每个状态序列被A'接受'）和完备性（每个状态序列满足'被A'接受'）得出的。在本节的剩余部分中，我们假设A'=hQ;Q0;V; Fi是formula'的表自动机。健全性我们证明了该自动机只接受满足“。 主要引理是以下翼，声称在一个特定的位置的一个新的穆拉是正确的处理。引理4.3设L是一个状态序列，设q是A'的一个游程，匹配令2q（0）。则j=。和证据通过归纳对结构。我们只给出了与联合国反演算法有关的情况。如果“1U”22q（0），则可以通过在范式表示中对“1U”2的约简以及 通 过 自 动 机 的 构 造 来 表 明 ， “1U”2 至 少 传 播 到 某 个 l 〇cationcontto“2（由于运行满足与f”1U“2相关的接受条件，因此最终到达这样的位置），通过局部信息，直到该点。10种阳离子包含1。因此，存在一定的k，例如22q（k），对于每0m 1，则rst符号与位置不匹配，这类似于第一例，或RST码元与该位置匹 配 ，但是不存在存在游程的后继位置。通过归纳，我们得到1是每个后继位置i的信息性坏前缀x，因此对于NF（Next（）），以及根据引理5.3，它是V Next（）的信息性坏前缀x。 从这一点这是一个信息量很大的错误。2下面的引理是证明相反情况的主要成分，即信息量差的前缀在tableau自动机上没有匹配的运行。引理5.5设2假设IS是一个信息序列，20：for. “不，不。