量化离散持续时间演算QDDC的符号自动机翻译与模型检查的应用

理论计算机科学电子笔记153（2006）3-18www.elsevier.com/locate/entcs从离散持续时间演算到符号自动机Laure Gonnord2 Nicolas Halbwachs3 Pascal Raymond4V'erimagGrenoble，France1摘要本文的目的是翻译（片段）量化离散持续时间演算QDDC，提出了P。Pandya，转化为带有计数器的符号接受器接受器是用同步编程语言Lustre编写的，以便将可用的符号验证工具（模型检查器，抽象解释器）应用于QDDC中表达的属性。我们表明，QDDC的重要结构需要非确定性的接受者，以便用有限数量的计数器进行翻译，并且逻辑的表达片段被识别和翻译。然后，我们考虑一个更严格的片段，它只需要确定性受体。关键词：持续时间演算，QDDC，同步观测器，非确定性观测器，光泽1介绍表示时态逻辑的可判定性的经典方法（例如，[22，2]）是与逻辑的每个公式相关联的有限自动机，它完全接受公式的模型。这种方法也允许研究决策问题的理论复杂性。此外，由此产生的自动机可以用于模型检查程序：为了验证，1VerimagajointlaboratoryoniveritoeJosephForier，CNRSandINPGasso t i t on a t or i t or y e J osephForier，CNRS and IN P G a ss o t i t o n at o r it o r ye J os eph F o r i er，CNRS andIN P G ass o t on a t o r i t o r y e I i t o n a t o r i2电子邮件：Laure. imag.fr3电 子 邮件：Nicolas. imag.fr4Email：Pascal.Raymon d@ ima g. fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.02.0224L. Gonnord等人/理论计算机科学电子笔记153（2006）3一个程序满足一个公式，人们可以证明由程序的同步乘积（被认为是有限转换系统）与公式的否定的接受者（被用作属性检查器）。现在，对于实际的程序验证，应该重新审视这个经典的方法。首先，决策程序在实践中并不总是有趣的。一方面，它们的复杂性通常是禁止的，另一方面，精确的验证通常是无法实现的：程序不是有限状态或太复杂，所以它们必须被抽象[13，6]，因此它们的验证只是保守的（即，阴性结果是不确定的）。这意味着没有特别的理由将自己限制在具有有限状态接受者的逻辑中：如果我们有精确或保守验证无限状态系统的工具（例如，[7]、[16]、.）它们可以应用于具有无限状态属性检查器的无限状态程序的合成。此外，通常的方法将公式转换为显式自动机。虽然这些自动机的大小通常不是问题-因为简单的公式产生小自动机-但将它们编码为符号自动机可能是有用的，即，具有初始值的状态变量上的转移关系或函数一方面，如果应用符号模型检查技术[4，1]，则这种符号编码更方便另一方面，无限状态自动机的扩展是直接的，只需考虑状态变量的无限一个典型的例子是持续时间演算的许多版本，其中涉及持续时间的公式在接受器中产生有界计数器;这些计数器的可能值在显式自动机中枚举，而它们可以保持符号性并自然扩展到无界计数器。本文的主要目的是说明用符号自动机识别公式模型的思想，通过考虑无限状态受体来扩展表达能力，并通过抽象解释将结果用于保守验证[5，7]。我们考虑P.Pandya 5在[18，19，10]中引入的“量化离散持续时间演算”QDDC。我们将自己限制在安全属性上，这些属性可以通过检查可达状态（的上近似）来验证。我们首先注意到，QDDC的任何公式都不能被具有有限个计数器的确定性符号自动机识别。我们解决这个问题通过使用非确定性受体，被认为是非确定性自动机[17]，仍然可以被验证工具使用：目标验证工具继续通过证明拒绝状态是不可到达的。 当验证5看到也可访问www.tcs.tifr.res.in/~pandya/dcvalid.html。L. Gonnord等人/理论计算机科学电子笔记153（2006）351这只是保守的，这是我们能得到的唯一有意义的结果（因为判决是不确定的，否则）。因此，一个序列被认为是可接受的，如果它被自动机的所有运行接受（这是自动机的验收标准）。考虑到这个想法，我们确定了一个重要的QDDC片段，可以很容易地转换为符号受体。非确定性受体便于验证，但不能用于其他环境，如属性模拟和程序测试。这这就是为什么我们还要研究一个更受限制的逻辑片段，它可以被决定论的接受者所识别。本文的结构如下：第二节回顾了QDDC的语法和语义.在第3节中，我们定义了我们所考虑的符号接受者，这将在Lustre语言中描述，我们给出了（第4节）我们所考虑的翻译的直观性。第5节和第6节描述了非确定性片段和确定性片段的重新定位，以及到符号接受者的翻译和一些例子。2逻辑QDDCP.Pandya在[18，19，10]中提出了让我们使用brie brief回顾一下它的语法和语义：语法：设Prop（3p）是一个有限的命题符号集。这组比例公式的经典定义为：P：：= 0 |1 |p|欧元/英镑|PP|Pν PQDDC的公式归纳定义为：D：：=[P|0|[[P| |C/P opc|D1-D2|D|D型|D - D2|D-D2其中op∈ {≤，，=，>，≥}且c∈IN。语义：命题的模型是状态，即，从命题符号到{true，false}的函数。命题的意义是标准的。 公式的模型是状态的有限序列（σ= σ0σ1.σ n）。一个公式的意义首先由这样一个序列的整数v a l定义：anitervalσ[b，e]=σbσb+1. . σe由一对指数（b，e）定义，使得0≤b≤e≤n：6L. Gonnord等人/理论计算机科学电子笔记153（2006）3我112 1 21C-0个1 2D1→D2和<$D的语义是通常的。一个区间满足[P|如果它被还原为满足P的状态，则区间满足[[P|如果它的所有状态（除了最后一个）都满足P;一个区间满足η op c，如果它的长度η满足op与c的关系;如果满足P的状态数满足特定关系，则区间满足Popc;如果其每个状态σi可以改变为仅在p值上不同的状态σJ，则区间σ[b，e]满足D;最后，区间σ[b，e ]满足Dsatis ssD-D2如果它可以分成两个区间（共享一个连接状态），分别满足D1和D2。最后，一个有限序列σ = σ0σ1...σ n满足公式D（注σ |= D）当且仅当σ [0，n]|= D.派生运算符：像往常一样，提出了一些有用的导出算子：• 逻辑布尔运算符：true，false，fax，.def· [[P||中文（简体）|[P|（区间右闭）• QD def• QD<$$>Q <$D（总是D）• P→cPdef<$Q（（[[P||∧η≥c)-[¬P]0)(wheneverPhasbeencontinu-在c步骤中，P2为真）。这个逻辑在[18]中被证明是可判定的。在这里，由于我们• 常数c在诸如ηopc、ηPopc、P1→P2等• 通过参数上的条件来扩展这些命题（例如，c1≥c2）。3符号自动机我们的目标是定义公式的符号接受者。符号受体是符号自动机的特殊情况，我们现在精确地定义了它σ [b，e]|=[P |0我的b = e和σ b|= Pσ [b，e]|=[[P|我的b< e和σ i，b ≤ i< e，σ i|= Pσ [b，e]|= η op c我的（e-b）执行部分cσ [b，e]|= P op c我的卡{i |b ≤ i “运算符的第一个参数下面是一些定义的例子，我们将在本文的其余部分使用（其他例子可以在附录中找到）：• 让我们在p之后定义一个输出，如果p为真或在过去为真，则该输出为真：after p = p or（false->pre（after p））• 现在，我们希望输出nb q since p是自上次p为真以来q为真的次数：nb q since p = if p then（if q then 1 else 0）else if after p then（pre（nb q since p））+（if q then 1else 0）else 0我们经常使用这些程序的函数式版本，因此在（p）和nb since（q，p）之后编写，以便将它们应用于各种参数（这是Lustre中节点的概念所允许的）。现在，符号接受器是一个符号自动机，只有一个布尔值，8L. Gonnord等人/理论计算机科学电子笔记153（2006）3C输出变量，比如a。一般来说，输入变量是布尔型的，表示原子命题的值。式D的受体将使得（i0，i1，.，i n）|= D当且仅当输出序列（a0，a1，.，a n）由自动机响应于输入（i0，i1，. ，i n），使得an=true。4用符号接受器识别公式模型在这一节中，我们将说明我们想要执行的转换类型以及我们打算使用它的方式，我们将为每个公式关联一个接受者，接受原子命题的值作为输入，当考虑逻辑的扩展版本时，可能是数值参数，以及一个附加的布尔输入，比如b，它在感兴趣的区间的开始处为真。当b为真的最后一步之后经过的时间间隔满足公式时，接受器的输出为真（按照惯例，它在b第一次出现之前也为真）。我们首先考虑一些这样的翻译的例子。4.1一些示例(i) 让我们考虑公式[p||.接受器输出必须在b第一次出现之前为真，只要b为真就取p的值，只要p为真就保持为真：a =不在（b）之后或（如果b则p，否则（p和pre（a）(ii)公式D=p→q指出，只要p已经被在C步骤中为真直觉上，这个公式的接受者应该管理一个计数器（一个整数状态变量），比如x，当p为假时设置为0，每当p为真时递增，当b为真时重置（间隔的开始）。然后，当计数器大于或等于c且q不成立时，输出变为false;只有当新的间隔开始时，它才能返回true：a =不在（b）之后或（（b或（true->pre（a））和（age pc或q）;age p = if p then（if b then 1 else（0->pre（age p）+1））else0;<重要的一点是，在这个自动机中，计数器是一个整数变量，延迟c可以是符号的。要将其扩展为显式自动机，需要c的值是固定的和已知的，并且计数器要扩展为c个显式状态。但如果我们用一个验证工具L. Gonnord等人/理论计算机科学电子笔记153（2006）39有了数字，自动机可以保持符号性，我们甚至可以尝试证明由c参数化的属性。(iii) 现在，考虑公式Q（（η > c）<$（<$p≥d）），说明p在任何大于c的区间内至少出现d次。我们可以像上面一样使用计数器来测量间隔的长度，并计算p.问题在于，至少在每次出现p之后，应该创建新的计数器（因为可以容易地看到，出现p之后的每个步骤可以开始公式的因此，标准方法需要d对计数器，如果d是符号的，则不起作用。为了解决这一问题，对这类公式，我们将使用非决定性的接受子.这样的接受者不使用无限数量的计数器，而是自由地选择开始观察（在上面的特定情况下，这种选择可以限制在初始步骤和每次出现p之后的步骤，但是这种限制对于验证是无用的）。现在的语义是，如果接受者接受输入，则满足公式，无论输入它的非确定性选择（它可以被看作是一个随机自动机[17]）。4.2非确定性受体我们的符号接受器是确定性的，但是我们可以通过添加辅助输入来将它们用作非确定性接受器：输入集合I被分成J+K，其中J中的变量是经典输入，而K中的变量是称为“神谕”的附加布尔输入。现在，输入序列（j0，j1， . . . ，jn）（jl∈ValJ）将是一个ceptedifandonlyifn，对于任意序列（k0，k1，.，k n）（k l∈ValK），输出序列（a0，a1，.，an n），由自动机响应于输入（[j0，k0]，[j1，k1]，.，[j n，k n]），使得a n= true。回到前面的例子，公式的接受者Q（（η> c）（ηp≥d））由以下代码给出，其中k是oracle：length = nb since（true，k）; nb p = nbsince（p，k）;a =不在（b）或b之后或（（true->pre（a））且（长度c或nb p≥d））;<当然，在有限状态的情况下，确定性接受者具有与非确定性接受者相同的表达能力，但如果我们想让它们保持符号化，非确定性自动机就不能被确定。因此，虽然确定性受体可以很容易地被补充（简单地通过否定它们的输出），但非确定性受体的情况并非10L. Gonnord等人/理论计算机科学电子笔记153（2006）3ACCProgC（一）aaK（b）第（1）款Fig. 1.在程序验证4.3用于验证我们考虑的验证工具（例如，那些专用于Lustre程序的程序：Lesar [21]或NBac [16]）专门用于安全属性：它们考虑程序的同步组合和属性的接受者（如图1.a所示），并探索该组合的可达状态集（或该可达集的上近似），以表明不能到达坏状态。换句话说，他们试图表明，无论输入是什么，输出总是正确的。在这个框架中，可以很容易地使用非确定性的接受者：神谕只是额外的自由输入（图1.b），只要神谕被普遍量化，验证工具就会像以前一样工作。例如：让我们考虑下面的QDDC公式，它显然atautolog y：.p→c q<$d≥c<$d（p→d q）的证明该性质的一种方法是将下面的接受器-其中我们使用第4.1节中给出的p→q的接受器，并且其中oracleb表示感兴趣的区间的开始-提交给验证工具(here，没有程序来验证），目的是表明输出总是为真：a1 =不在（b）或（（b或（true->pre（a1））和（age pc或q））之后; a2 =不在（b）或（（b或（true->pre（a2））和（age pd或q））之后; age p = if p then（if b then 1 else（0-ACCProgL. Gonnord等人/理论计算机科学电子笔记153（2006）311>pre（age p）+1））else 0;<，≥}，c是整数常数或参数。因为第二类公式将产生存在性量化的预言：E：：=N|E1和E2|E1和E2|埃因霍温|E-E2最后，性质是：C：：=<$E5.2翻译成非确定性接受者我们的目标是将每个公式C关联到一个接受者AC，作为输入I的是命题公式的值的序列J、指示感兴趣的区间的开始的布尔b以及一组神谕K。输出被认为是一个函数a=AC（b，J，K）。重要的是要假设受体只被触发一次，因为它不是可重入的。所以用于开始公式的神谕将被转换为启动符：启动符是仅为真一次的布尔值建议：我 们 首 先 定 义 （ 在 相 对 的 表中）命题的接受者AP，如果命题在步骤l为真，则在步骤l返回真。公式N：我们首先介绍一些有用的运算符（它们都在附录中给出• always since（P，Q）返回true，如果P自上次oc以来一直为true。PAP（ I）ppPJP1∧ P2P1∧ P2不是APJ（I）AP1（I）和AP2（I）AP1（I）或AP2（I）L. Gonnord等人/理论计算机科学电子笔记153（2006）31312Q的电流;• nb since（P，Q）返回自Q上次出现以来P出现的次数;• strict after（P）返回true，如果P在严格的过去为true。• starter（b）将oracleb转换为starter：starter（b）= b，在（b）之后不严格。那么受主AN由下表归纳定义NAN（b，I）[P |0AP（I）和b[[P|严格的after（b）和pre（alwayssince（AP（I），b））ηop cnb since（true，b）op cC/P opcnbsince（AP（I），b） opc<$NJ不是ANJ（b，I）公式E：公式E的接受者区分真实输入（J）和神谕（K）。AN（b，J，K）=AN（b，J<$K）AE1<$E2（b，J，K）=AE1（b，J，K）<$AE2（b，J，K）AE1<$E2（b，J，K）=AE1（b，J，K）<$AE2（b，J，K）ApE（b，J，K {p}）=AE（b，J{p}，K）AE-E（b，J，K {bJ}）=AE2（starter（bJ）<$AE1（b，J，K），J{bJ}，K）配方C：最后，一个公式C=<$E的受体恰好是：而不是AE（b，J，K）。顶级验收：回想一下，序列满足QDDC公式σ = σ0σ1.σ n定义为σ| = D i <$σ [0，n]|= D因此，公式C的顶级接受者是AC（true->false，J，K），因为“在[11]中，这个翻译被证明是正确的，即：σ|=D，|σ|=n惠K，AD（b，J，K）=truen，where• b= true。（false）n−1，则在初始instant时，该表达式为真;• J是σ对集合J的变量施加的值。14L. Gonnord等人/理论计算机科学电子笔记153（2006）35.3示例让我们首先考虑一下这个问题（[p|-[[q|）. 根据我们的规定，我们• A[p|-[[q|（b，p，q，bJ）=A[[q|（a）（b）（j）（a）（b）（B）（J）（a）（b）（b）（c）（b）（b）（c）（b）（c）（c）（d）（c）（c）（d）（c）（d）（b）（c）（d）（d）（c）（d）（d）（e）（d）（d）（e）（d）（e）（e）（d）（e）（e）（d）（e）（e）（|（b，p，q），p，q，bJ）• A[p|（b，p，q）=strictaf ter（b）andpr e（alwayssince（p，b））• A[q|（b，J，p，q，b，J）=在（b”）之后的严格t和在（q，b”）之后的严格p（其中bJJ=starter（bJ）A[[p|（b、p、q））因此（为了清楚起见，引入a =不是e;e = strict after（bb作为另一个例子，我们已经考虑了激发引入非确定性受体的公式Q（（η > c）<$（ηp≥d））。转换为基本QDDC，该公式变为<$（true-（η>cpd）-true）落入我们的碎片中 其翻译（简化后）给出a =不是e;e = starter（<其中B最后，[ 18 ]中给出的“矿井泵”的整个例子6一个决定性的片段通过用编程语言（如Lustre）编写的接受器来表达安全属性的公认优点是，这些接受器可以被执行：它们可以用不同的输入序列进行测试，以检查它们是否很好地表达了初始直觉;它们也可以与程序一起运行，用于测试或“运行时验证”[ 15 ]目的。 现在，这不是我们的非确定性受体的情况，它只能与验证工具结合使用。这就是为什么寻找一个可以被翻译成确定性接受者的逻辑片段也很有趣。这就是本节的目的。首先，我们必须回到QDDC中的非确定性的来源。如果我们忘记了构造函数dipD（它是完全不确定的），L. Gonnord等人/理论计算机科学电子笔记153（2006）315.我们只剩下现在，在现实的具体化中，“印章”似乎经常被确定性地使用： 例如在[P|-[Q|0，则输入值被分裂成其自身和其最后状态。BASIC我们的确定性片段的想法是限制，称为现在，最大区间的概念只能处理D1的某种公式：我们将限制自己的公式只能从真到假时，间隔增加。我们首先定义这些公式，注意G。6.1语法和语义命题P和以前一样。片段G：正如所宣布的，公式G只能在时间流逝时变为假G：：= begin（P）|[[P ||η ≤ c |P ≤ c|年龄（P）≤ c |G1和G2|G1和G2唯一的新构造是begin（P）-它告诉我们区间的第一个状态满足P-和age（P）≤c-告诉我们P在少于c步的时间内连续为真：σ[b，e]|= begin（P） i <$ σ b|= P σ[b，e]|=年龄（P）≤ c ie − m ≤c其中m =max{i|b≤i≤e，σ i|=<$P} if <$P occurred in [b，e]b − 1否则完整片段：我们的确定性片段的公式被称为F：F：：= G|结束（P）|G然后F |F1和F2|€F新算子定义如下：σ [b，e]|= end（P）i <$σ e|= Pσ [b，e]|= G then Fi≠m，b ≤ m pre（age pb））+1 else 0公式F的接受者由对立表归纳地定义，其中“first（b，p）“代表“在（b）之后，p和pre（总是因为（不是p，b））“，并且在b之后第一次出现p时为真。6.3示例让我们展示一些使用“chop”运算符的公式的例子• [[P|-[Q|0isequivalenttoo[[P| 末端（Q）• p→c q可以重新表示为Q（（ag e（p）≤c）<$q），这意味着对于mula，满足当且仅当接受者真的7结论这项工作并不打算是一个理论。当然，只要我们考虑用无限计数器扩展的自动机，表达能力是最大的，我们可以编码涉及有限内存的任何类型的属性然而，这种编码几乎没有实际意义。我们希望将同步程序通常通过同步观察器指定的方式与TCS社区中更知名的形式主义联系起来。这就是为什么我们选择将属于广泛社区的逻辑（持续时间演算家族[8]），或者至少是有用的片段，翻译成我们的观察者。我们最初的灵感来自[20]，这是将理性表达式转换为Lustre受体的非常有效的翻译。很快，同样的技术似乎不能应用于具有计数器的自动机：在[20]中执行的翻译是通过可重入受体获得的FA、F（b、 I）结束（P）在（b）和AP（I）G然后 FAF（first（notAG（b，I），I））F1和F2AF1（b，I）和AF2（b，I）L. Gonnord等人/理论计算机科学电子笔记153（2006）317(the在运行时，受体的相同组件可以被激活若干次）。这对于扩展自动机是不可能的。这就是为什么目前的工作与[20]有很大的不同，特别是因为我们必须考虑带有预言机的非确定性自动机。我们还想捍卫这样一个观点，即在实践中，没有必要把自己限制在可判定的逻辑中，也没有必要限制在有限的状态接受者中。抽象和近似通常用于处理程序，没有理由不将其应用于属性。特别地，用计数器扩展的自动机是极其强大和有用的，并且提出了越来越多的技术来处理它们（例如，[3]、[9]、[16]、[12]、.）的。确认我们感谢Paritosh Pandya发起这项工作，并进行了许多有益的讨论。引用[1] J.R. Burch，E.M. Clarke，K.L. McMillan，D.L. Dill和J. Hwang。符号模型检查：1020个状态及以上。第五届IEEE计算机科学逻辑研讨会，费城，第428-439页[2] O. Bernholtz，M. Vardi和P. Wolper。分支时间模型检验的自动机理论方法。In D. Dill，编辑，第六届计算机辅助验证国际会议，CAV[3] B. Boigelot和P. Wolper。用周期集进行符号验证。在CAV1994. LNCS 818，Springer Verlag。[4] O.库德特角Berthet和J.C.妈妈使用布尔函数向量验证时序机。在洛J. M. Claesen，编辑，Formal VLSI Correctness Verification。北荷兰，1989年11月。[5] P. Cousot和R.库索抽象解释：一种统一的格模型，用于通过构造或近似定点来静态分析程序第四届ACM程序设计语言原理研讨会[6] E. M. Clarke，O. Grumberg和D. E.久了模型检查和抽象。ACM TOPLAS，16（5）：1512[7] P. Cousot和N.哈布瓦克斯。自动发现程序变量之间的线性约束。第五届ACM程序设计语言原理研讨会，POPL[8] Z.超辰，C.A.R.霍尔和A.P.拉文。持续时间的计算。信息处理快报，40（5），1991年。[9] H. Comon和Y.尤斯基多计数器自动机、安全性分析与presburger算法。在CAV1998. LNCS1427，施普林格出版社。[10] G. Chakravarty和P.K.潘迪亚数字化间隔持续时间逻辑。CAV 2003，科罗拉多州博尔德，2003年7月。18L. Gonnord等人/理论计算机科学电子笔记153（2006）3[11] L.唐托尼-贡诺德你可以把它当作你的礼物。 Masterthe sis，Universersit'esPar isVI/V II，2003年6月。http://www-verimag.imag.fr/dea.ps.[12] A. 芬克·埃勒和G。 真的。一个简单的算法可以减少2-Dreset/transfervass的最小值。第25集Int.Symp. 数学Found. Comp. Sci. （MFCS'2000），斯洛伐克布拉迪斯拉发，2000年8月。LNCS1893，Springer Verlag。[13] S. Graf和C.卢瓦索一种符号程序验证和抽象的工具。1993年7月在希腊伊罗达举行的第五次计算机辅助核查会议上LNCS 697，Springer Verlag。[14] N. Halbwachs ， P.Caspi ， P.Raymond 和 D. 皮 劳 同 步 数 据 流 程 序 设 计 语 言 LUSTRE 。Proceedings of the IEEE，79（9）：1305[15] K. Havelund和G.罗苏安全性能综合监控器。2002年4月，在法国格勒诺布尔举行的关于系统构建和分析的工具和算法的国际会议（TACAS[16] B. Jeannet，N. Halbwachs和P. Raymond。数值问题分析中的动态划分。 InA. C或t esin d G.Fil'e，editors，StaticAnalysisSymposium，SASLNCS 1694，Springer Verlag。[17] Z. Manna和A.普努埃利并发程序的规范化与验证--基于自动机。第14届ACM程序设计语言原理研讨会，POPL'87，慕尼黑，1987年1月。[18] P.K. 潘迪亚使用dcvalid确定量化的离散时间持续时间演算公式实时工具，RTTOOLS'2001，奥尔堡，2001年8月[19] P.K. 潘迪亚区间持续时间逻辑：表达性和可判定性。2002年TPTS“计时系统理论与实践讲习班，格勒诺布尔，2002年4月[20] P·雷蒙德利用数据流网络识别正则表达式。第23届自动机、语言和编程国际学术讨论会（ICALPLNCS 1099，Springer Verlag，1996年7月。[21] C. Ratel，N. Halbwachs和P. Raymond。用同步数据流程序设计语言LUSTRE对关键系统进行编程和验证.在ACM-SIGSOFT[22] M. Y. Vardi和P. Wolper。自动程序验证的自动机理论方法。在计算机科学中的逻辑研讨会，1986年6月。附录：Lustre在（p）之后在p之后或第一次出现时返回true后（p）=如果p则为真else（false-> pre（after（p）;在（p）之后严格在第一次出现p之后严格返回truestrict after（p）=if（false-> pre（p））then trueelse（false->pre（strict after（p）;L. Gonnord等人/理论计算机科学电子笔记153（2006）319起动器（b）将b转化为单一事件启动器启动器（b）=b和（b）后不严格总是因为（p，b）如果p自上次出现b以来一直为真，则返回true;在第一次出现 b第一（p，b）在第一次出现时返回trueb发生后的pFIRST（p，b）= p且从不p;从不p =如果最佳则为真else if（false->pre（p））thenfalse else（false->pre（neverp））nb since（p，b）计算自上次出现b以来 p出现的次数;在第一次出现 b总是因为（p，b）=if b then p如果在（b）之后，则（p and pre（always since（p，b）））else true年龄（p，b）计算从b（假设是唯一的）和非p的age（p，b）=如果在（b）之后且p则（0-> pre（age（p，b）+1其他0nb因为（p，b）=if b then（if p then 1 else0）else if after（b）then（pre（nb since（p，b）+如果p则1否则0其他0