简化线性时间逻辑公式生成小型布希自动机的在线技术及其性能对比

145《理论计算机科学电子札记》66卷第2期（2002）网址：http://www.elsevier.nl/locate/entcs/volume66.html15页从LTLF或Mulas到Bu？chi自动机的Xavier Thirioux1IRIT-LIMA，2 rue Camichel，31071 Toulouse，France，Xavier. enseeiht.fr摘要我们提出了一系列简单的在线技术来从线性时间逻辑公式中生成小型的Bu？hi这些技术主要涉及公式的语法特征，但允许高效的计算。因此，严重依赖于这样的证明理论问题，我们可以省略经典公式的预简化步骤，以及基于模拟的后简化步骤（又名模型理论问题）。虽然与同一主题的其他类似的最新作品密切相关，但我们的想法已经导致了一个实现，其性能明显优于一些最好的可用工具，如Wring或LTL2BA。我们比较了我们的工具BAOM（主要工作：线性时间逻辑. 布希自动机。基于表格的方法。公式的句法特征介绍本文介绍了几种实现线性时间逻辑（LTL）规范到布希自动机高效转换的新技术。我们的主要动机是实现一个新的基于符号BDD的2模型-checker[2009 +92]基于同步程序的线性时间逻辑规范，特别是那些用Esterel编写的程序。这项工作扩展了Xeve模型检查器[Bou97]上以前的工作。在我们的符号框架中，实现这一目标的一个众所周知的解决方案是首先将任何给定的LTL公式（的否定）转换为插入到我们想要检查的原始设计中的观察者（有限状态机）。然后，通过乘积系统的符号正像计算，1这项工作得到了法国SYNTEL RNRT项目的部分支持2 BDD是Binary Decision Diagram的缩写。2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。特希里乌146满足公式所规定的公平性条件的执行，即所谓的Bu？chi条件。虽然该原理相当简单，但在将公式转换为观察者期间避免指数爆破的有效实现是难以实现的。近年来，一些有前途的新算法被发现来降低自动机的规模。由此产生的工具，即LTL2BA、Wring和EqLTL（分别参见 [GO01，SB00，EH00]）似乎优于SPIN [Hol97]。我们的主要贡献是提供一个新的实现（称为BAOM），线性行为（在空间和时间）的公式（ES-特别是公式包含公平性约束），以前的算法表现出指数爆破。此外，我们得到的自动机平均比任何其他方法都要小。我们的原型直接从一个线性模拟逻辑构造出一个广义布希自动机，而不需要中间数据结构。为了效率起见，我们的跃迁被标记为BDD，而不是单原子命题。此外，我们的自动机是广义的混合意义上，即我们有公平条件的状态以及过渡，这取决于形状的公式。注意，我们的思想主要关注基于公式之间的语法关系的在线优化。我们还引入了一个概念，尽管如此，我们的算法广泛借鉴了最近的tableaux方法，从最近的技术交替自动机，也从公式之间的语法关系的想法。实际上，我们在表格生成过程中将[SB00]的语法简化规则包括在表格中，并以这种方式将[DGV99]和[GO01]的类似规则泛化。这些规则中的一些在我们的例子中，这种简化可能会对转换引入新的公平性约束，如[GO01]。相关的工作有很多种，但主要涉及[VW94]和[GPVW95]中描述的tableau方法的改进。 在[EH00]中，作者提出了一种分三步的算法：首先是重写步骤，然后是标准翻译，最后是基于模拟的优化。在[SB00]中，应用了相同类型的技术，但具有完全不同的重写规则和可以更有效地计算的模拟关系。 在[GO01]中，作者还重用了与[SB00]中相同的重写规则集，并考虑了非常简单的在线简化规则，这些规则避免了基于模拟的方法中必要的定点计算。简化过程虽然简单，但由于基于交替自动机的特定转换，其中公平性约束仅涉及转换，因此仍然是有效的。最后，所有这些工作都指出了在某些情况下简化特希里乌147B∈ B →→× B × FB组⊆|→- 所生成的自动机的SCC3的公平性约束，例如通过递归去除不公平的终端SCC。路线图：第1节介绍了初步的概念，并提醒原来的tableaux方法。第2节介绍了我们的新的重新访问tableaux算法，建立了一个布希自动机的第一个版本，从一个LTL的穆拉。该算法分为四个部分：(i) 使用修改后的表格规则生成基本自动机（第2.1节）;(ii) 规范和简化过渡（第2.2节）;(iii) 检测不公平的SCC并简化自动机（第2.3节）;(iv) 合并过渡等价状态（第2.4节）。此后，第3节提出了一个经典的后简化阶段，以减少状态的数量。最后，我们在第4节中展示了我们的原型的一些有希望的结果，并将它们与其他类似的工具进行了比较，然后我们在第5节中总结。1预赛我们定义了一种在状态和转移边上具有多个接受条件的Buéchi自动机，也称为广义Buéchi自动机.标签位于转换边，并且是从一组原子命题AP（4）构建的布尔公式（以下表示为（AP））。我们使用一个数据结构来表示边（从而取代传统的δ函数），因为我们实际上需要区分具有不同公平约束和兼容标签的不同过渡边。请注意，我们统一处理状态公平性和转换公平性。定义1.1GBA是一个五元组：A=AP，Q，Q0，E，F其中AP是原子命题的集合，Q是状态的有限集合，是初始状态的集合，EQ（AP）Q是边的集合，并且（Q E）是验收条件的集合，表示为逻辑约束。（广义）转移函数δ（AP）2Q2 Q可以从E恢复为：δ（p，qs）={qJ|<$q，l，qJ.q∈qs<$$>q，l，qJ<$$> ∈E<$|=p→l}由于p和l被编码为BDD，因此我们可以容易地决定是否保持或不。A的游程是无穷序列σ=<$q0，i0，t0<$;<$q1，i1，t1<$;. 哪里qk∈Q，tk∈E且ik<$AP ，使得对于allk≥0：tk= qk，lk，qk+1ik|= lkSCC是Strongly Connected Component的4对于X是一组基项，B（X）表示它的布尔闭包。特希里乌148∈FⓍ运行σ是可接受的，如果对于每个F，我们有无限多个ktk，qk+1|= F最后，自动机A接受输入事件的无限词i=i0，i1，. 在（2 AP）ω上，只要存在A的可接受游程：σ=<$q0，i0，t0<$;<$q1，i1，t1<$;.它的语言L（A）是它接受的无限词的集合。多个初始状态和多个接受条件不是强制性的，但在这里仅为了方便而考虑关于发生转换步骤的整个模型检查过程。定义1.2线性时间逻辑（LTL）是从命题逻辑中通过添加时态运算符构建的，产生以下语法：LTL：：=AP| B (LTL)|LTLU|LR LTL|LTL是“下一次”操作符，U是（强）“直到”操作符，R是“释放”操作符。 R和U是彼此的对偶。通常的“总是”和“最终”运算符被定义为“R φ = False R φ”和“U φ = True Uφ”。我们在这里简要回顾标准tableaux方法[VW94，GPVW95]，因为我们使用它作为我们自己扩展的基础自动机的每个状态表示和标识负范式的LTL公式，即否定已经被推下公式的解析树。然后，从一个给定的状态，转移函数计算的语义扩展规则。这些规则包括通过扩展函数Exp从左到右将以下等式应用于状态公式：Exp（prop）=propExp（φ）=φExp（φ）=Exp（φ）<$Exp（φ）Exp（φ）=Exp（φ）<$Exp（φ）Exp（φU）=Exp（（φU））Exp（φR）=Exp（（φR））因此，从一个公式φ开始，我们首先展开它，然后把它变成析取范式。每一个合取项= 12. 将成为下一个国家。根据上述规则，每个命题都是一个原子命题，特希里乌149M F的|或下一次公式θi。因此，π-态将被标记为公式θ1<$θ2. 而从φ-态到φ-态的过渡边将由命题公式ap1→ap2.标记。. .像往常一样，标记为不可满足的命题的转换被删除，从而也删除了不可到达的状态。初始状态是从根公式的扩展中构建的。如果初始公式不展开，则可以避免多个初始状态。这可能会增加或减少状态的数量，这取决于公式（见定理2.13）。最后，对于Bu¨chi的接受条件，对于每个chφUo在状态公式中发生，存在一个接受公式FairφUon指出：一般φU={q∈Q|φU∈q}然后，对于这种特殊的状态公式，运行被接受的条件归结为以下陈述：对于每个集合FairφU，我们有无穷多个q k，|=一般φU。2表法再探在剩余部分中，我们提出了不同的步骤，旨在减少自动机的大小。所有这些改进都是相对于普适自动机而言的=AP，Q，Q0，E，假设在每一步是先前变换的结果。为了便于描述我们的方法，我们定义了一个集合上的替换概念：.（S\{e}）<${eJ}如果e∈SS [e] J|e]=其他2.1展开表格规则在设计这个新算法时，我们的主要目标是从标准的基于表格的方法中获得小的确定性自动机我们现在定义一个LTL公式的时间近似，由一个正整数驱动，表示为φd。这个近似是一个公式，它精确地表示由φ标识的无限个词的有限个d前缀。定义2.1对于任意φ∈LTL，在负正规形下且d≥0，我们特希里乌150的|定义函数[φ|d如下所示：[美联社|D= AP[φ]|d=[φ|d[]|d[φ]|d=[φ|d[]|D[φU]|d=[（φ（φU））|d[φR]|d=[ （ φ （ φR ） ） |d[φ]|0= T rue[φ|d+1= φ [φ|D引理2.2对于一个yφ∈LTL且任意d≥0，我们有：φ∈[φ|d，而且φφ（[<$φ|d优惠证明（略）通过对φ的结构归纳法证明了该蕴涵。然后是等价性。我们现在可以修改扩展规则，考虑到这个有限近似。实际上，给定任意整数d，我们可以对U和R使用以下新规则，其中<$r和<$φ被置于负正规形式：Exp（φU）=Exp（（φ（[|d（φU）Exp（φR）=Exp（φ（[<$φ|d（φR）定理2.3对任意φ ∈LTL和任意d ≥ 0，设Md是用修正的展开规则产生的自动机，则L（M）= L（Md）.证明（草图）自动机是根据语义扩展规则产生的，以便它们完全接受由状态公式表示的然后利用引理2.2将修正公式转化为标准公式，证明了M和Md接受相同的语言.对于我们的特定用法，使用较大的d值可能会增加不同状态的数量，因为。d运算符生成新的下一次子公式。然而，由于预固定公式引入的对转换的额外约束，这也可能增加所得到的自动机的确定性，也就是说，我们在早期阶段获得了更多的不相容转换，稍后我们经过一些结论性的实验表明，状态的平均数量往往会随着d的增加而增加，我们决定暂时将我们的选择限制为d= 0，从而在较小的开销和更好的整体性能之间取得良好的平衡。 例如，使用以下形式i=1. Npi，将N作为参数，我们的方法可以相对于Wring工具保存指数数量的状态，或者进行前处理。比LTL2BA工具更快（我们在特希里乌151≤∈≤φ1{φ1srcDSTDST本案5）。我们现在假设每个状态表示一组合取解释的公式，而不是单个合取公式。设φ是两个公式之间的一个句法蕴涵关系，类似于[SB 00]和[DGV99]中的关系这种关系将极大地帮助我们减少自动机的规模。注意，这个关系定义2.4对于任何φ，φ LTL，我们将关系φ φ定义为以下规则的最小定点：假≤φ≤真φ1φ2≤φ1 ≤φ2 ≤φ≤12 φ ≤1 2 φ ≤ 1 2φ ≤1 φ≤ 2 φ1 φ2 ≤φ1≤φ2≤φ1Rφ2 ≤φ 2 ≤φ≤1U 2φ≤ 2φ1Rφ2≤1 R2φ1≤1φ2≤2φ1 Uφ2≤1 U2φ1≤1φ2≤2这个定义使我们能够从状态中去掉弱公式，从而在许多情况下减少不同状态的数量，通过下面的定理。定理2.5设q={φ1，φ2，.，φ n}∈Q是满足φ1≤φ2 的 状 态。表示集合{φ2， . ，φn}。则L（M）=L（MJ），其中自动机MJ=AP，QJ，QJ0，E J，FJ定义如下：• Q J= Q [q J|q]• QJ0=Q0[qJ|q]• E J={qsr c，l，qds t[qJ|[q]q|<$qsr c，l，qds t<$∈E}空气φ[qJ|q]|Fairφ∈F}ifφ1/=U•FJ=F[FairφJ1|Fairφ1]else，withFai rJ =Fair[qJ|q]<$（<$q Jq，l， q <$∈E|qq}）由于我们的蕴涵关系很容易被证明是合理的，这两个自动机接受相同的语言，而不考虑公平性约束。在被移除的公式φ1是一个直到公式并且因此涉及到接受条件的改变的情况下，我们将φ1的公平性报告给状态qJ的所有传入转移边缘。因此，我们模仿标准情况，公平性在状态Q上。5如第4节中的测试用例所示特希里乌152∈F∈ F∈M|F|2.2规范化变迁一旦建立了来自给定状态的传出转换边，我们就进行归一化步骤，在该步骤中我们对转换进行因子化。这种因式分解是可能的（并且简单），因为我们使用BDD来表示转换标签。定义2.6假设φ LTL满足空气φ和q，qJQ，我们定义了两个状态之间的以下全局公平（和不公平）标签函数：lφ（q，qJ）={l |t =<$q，l，qJ<$$>∈ E <$t，qJ|= F空气φ}lunfair（q，qJ）={l|t=∈EFairφ∈F.t，qJ|=F空气φ}有了这些函数，我们可以定义我们的标准化步骤。定理2.7L让我们定义自动机MJ=AP，Q，Q0，E J，FJ：• E J={q，l，qJ|l=lφ（q，qJ）{l=lunfai r（q，qJ）}• FJ={FairφJ|F空气φ∈F}，F空气φJ= {t<$qJ|t=<$q，l，qJ<$$> ∈E J<$l=lφ（q，qJ）}则L（M）=L（MJ）。证明（草图）这种归一化可以减少两个状态6之间的过渡边的数量，但对的语言没有影响，因为我们相对于公平性约束对边进行了分解。我们必须注意的唯一情况是，当给定的过渡边对于至少两个不同的约束是公平的然后，我们必须将它分成（至少）两个具有相同标签的不同边，每个边只满足一个公平约束。但是对于任何被接受的词，如果M的一条原始边被无限频繁地触发，那么MJ的结果边也可以被无限频繁地触发，每个边依次被触发。反之亦然。 所以最终L（M）=L（MJ）。注意，在上面的定理中，我们确实可以很容易地简化公平性约束，以便只保持转换公平性。实际上，定义：F空气φJ={t|t=<$q，l，qJ<$$> ∈E J<$l=lφ（q，qJ）}也会产生同样的结果。但是我们决定保留这两种公平性信息，因为这允许在我们的原型中实现更简单的算法。下一个步骤是尝试从任何给定的状态确定转换，即修改它们的标签，使它们的成对交集变为空。这通常会导致更少数量的（更小的）过渡边，并允许在实践中进一步简化（见定理2.13）。此外，自动机的结构也更容易被有效的模型检测算法所检验.实际上，自动机的确定性是一个6 在此操作之后，在任何两个状态之间总是存在小于+1的不同过渡边缘特希里乌153∈∈这是符号模型检测中的一个显著特征，因为它对例如分区状态空间探索算法的效率有很大的影响。定义2.8我们经典地将公式之间的蕴涵概念扩展到状态之间的蕴涵。 对于任何q，qJ∈ Q，我们定义：q≤ qJ=<$φJ∈ qJ. φ∈q.φ ≤φJ定理2.9设t1=<$q，l1，q1<$∈ E，t2=<$q，l2，q2<$∈ E.现在假设q1≤q2，l1<$l2/=假，并且：<$F空气φ∈ F.t1，q1|= F空气φt2，q2|= F空气φ则自动机MJ=AP，Q，Q0，E J，FJ定义如下：• E J= E[t J1 |t1]，其中t J1 =<$q，l1<$$>l2，q1<$• FJ=F使得L（M）=L（MJ）。 我们从Ej中去掉新的变换tj，并设FJ={Fairφ[False|[tJ1]|如果l1l2=F alse成立。根据定义2.4和2.8，q1≤q2意味着L（q1）<$L（q2）。因此，我们可以安全地从t1中删除与t2相同的输入事件。不需要改变公平性约束公平性约束，以及l1<$l2=（l1<$$>l2）<$l2。因此，如果我们有一个被接受的词从q通过l1<$l2传递到q1，我们知道它也会通过q2被接受。2.3检测不公平SCC我们的最后一步可以简化状态的公平性约束，通过早期检测某些不公平的SCC，即至少有一个公平性约束永远不会满足任何状态的SCCs，或瞬态SCC，即只有一个状态且没有自循环的SCC。此外，我们定义了一个句法下近似的不公平和短暂的SCC。定义2.10对于q Q，我们定义以下FairLoop和 Unstable同品种器械7：Unstable（q）=φ∈q.φ/=True<$FairLoop（φ，q）FairLoop（φ，q）==1R2∈q.φ=φ2引理2.11对于任何qQ，使得不稳定（q），则q的SCC是瞬时的或不公平的。[7]对于任何公式φ和φ，φ表示子项关系，但对于否定的原子。也就是说，对于p是一个原子命题，我们有p/<$p。特希里乌154≺--⟨ ⟩ ∈ ⟨ ⟩ ∈反证法（Proof）。假设q的SCC是公平的。然后，按照展开规则，每个非R公式φ必须由R公式的右侧循环（传递）因此，因为我们因此，不稳定（q）不成立。 总之，一个被接受的运行不能停留在不稳定状态的SCC中。定理2.12设q是一个不稳定状态，我们通过定义自动机MJ=AP，Q，Q0，E，FJ来改变公平性约束：• FJ={Fairφ[F alse|q]|F空气φ∈F}那么我们有L（M）=L（MJ）。我们可以安全地删除与不稳定状态及其传入的过渡边缘相关的公平信息，因为接受的词不能无限频繁地访问它，如引理2.11所示。所以，L（M）=L（MJ）。2.4合并状态最后但并非最不重要的是，我们定义了合并状态的概念它是将具有相同标签和公平性约束的一些转换的一些目标状态合并，形成复合状态。这也适用于可以合并为一个状态的初始状态。定理2.13设t1=q，l1，q1E，t2=q，l2，q2E. 现在假设我们有l1= l2（8）并且：<$F空气φ∈ F.t1，q1|= Fair φ惠t2，q2|= F空气φ则自动机MJ=AP，QJ，Q0，E J，FJ定义如下：• QJ=Q{q12}• EJ=（E\{t1，t2}）<${t12}，其中t12=<$q，l1，q12<$• FJ={Fairφ[F alse|{t1，t2}]F空气φ[t12<$q12|[t1q1]|F空气φ∈F}使得L（M）=L（MJ）。由于我们确保了转换和目标状态对公平性有相同的影响，因此我们可以在不修改已接受单词集的情况下合并它们。请注意，原始目标状态不会被删除，但如果它们变得不可访问。 则L（M）=L（MJ）。合并状态被定义为它的组件的集合。在定理2.13中，我们有q12=q1，q2。普通状态也可以定义为单例集。所以从现在开始，我们上升一个层次，断言一个状态确实代表一组公式。8这些标签在BDD标准化之前是相同的特希里乌155M通过同一标签可访问的状态似乎有一些共同点，并且可能值得尝试识别它们。我们只考虑相同的标签，就好像我们会考虑一个更宽松的约束（例如具有非空交集的标签），这可能会创建指数级更多的新状态。在实践中，似乎大多数时候，有趣的复合状态被创建，并且不是太多。然而，自动机中的某些合并状态可能会发生被其组成部分所包含，作为国家独立存在。然后合并状态是超连续的，可以安全地删除。初始状态，放在DNF中，也可以扮演合并状态的角色。根据以下定理，它可以被分裂为任何其他真实的合并状态，以减少状态的总数。为了将合并的状态分割回来，我们必须定义包容的概念。定义2.14对于任何公式集合的集合（不一定是一个实际状态）S，我们用下面的谓词定义被包含在的状态中意味着什么：包含（S）q∈Q.S=q已包含（S1<$S2）已包含（S1）已包含（S2）定理2.15我们考虑q = q1. <$q n∈ Q。 假设包含（q）保持。则自动机MJ=AP，QJ，QJ0，E J，FJ定义如下：• QJ=Q\{q}（Q0\{q}） . n{qn}如果q∈Q0Q0else• E J=E\{<$qsrc，l，q<$∈E}• FJ={Fairφ[F alse|q]|F空气φ∈F}使得L（M）=L（MJ）。证明（草图）我们移除一个状态q，它被定义2.14中所述的其他状态完全包含，并将其传入的边重定向到它的组件，这些组件一起识别与q相同的语言。H（M）= L（MJ）。这个定理可以在自动机完全建立后立即应用。我们选择尽快使用它，以减少简化后阶段的复杂性，但它可能值得推迟使用，以便一劳永逸地处理所有合并状态。目前也在试验中间选择。• QJ0=特希里乌156M F3简化后至于自动机后简化阶段，我们删除（除了一个）相同的状态，这是所有相关工作中的相关步骤。事实上，我们定理3.1考虑两个状态q1，q2∈ Q，具有相同的输出跃迁边，即 使得对于任意n =1，2和n = 3 − n：n=<$qn，ln，qJ<$∈E. n=<$qn，ln，qJ<$∈E.ln=lnFairφ∈F. tn，qJ|=Fairφ惠tn，qJ|=F空气φ在不失一般性的情况下，我们假设只要q1或q2中至少有一个是初始的，那么它就是q1。 那么自动机J= AP，QJ，QJ0，EJ，J定义如下：• QJ=Q\{q2}• QJ0=Q0\{q2}• E J={qsr c，l，qdJs t|<$qsr c，l，qds t<$$> ∈E<$qdJst=qds t[q1|q2]}• FJ={F空气φ[fq1，l，qds t f]|<$q2，l，qds t<$∈E][q1|q2]|F空气φ∈F}9使得L（M）=L（MJ）。这是自动机理论中的一个经典操作。4实验下面的例子都是在400 MHz的bi-pentiumII PC上用256 Mo测试的。我们首先包括从[EH00，GO01]中进行的一些测试（见图1），显示了Wring、LTL2BA和BAOM的相对性能。为了简单起见，我们决定只呈现最好的可用工具的结果，因为它们总是优于其他工具，例如SPIN。同样，大部分时间没有显示所用时间，因为所有这些工具通常在5秒内完成翻译，这在很大程度上是可以接受的。然而，存在病态公式，使得时间消耗是显式的。在这种情况下，我们精确地显示经过的时间或指示崩溃已发生或超时（10小时）已过期（†）。然后，我们展示了用LTL2AUT、Wring和BAOM处理的3组1000个随机生成公式的一些结果。时态和布尔运算符的概率相同（见图2）。最后，为了（松散地）比较BAOM和LTL2BA，尽管我们只能通过网页有限地访问LTL2BA工具，但我们使用了一个测试台9在一个双向定理中，|∈E]表示对所有∈E都进行替换。特希里乌157我们的工具与[GO01]中提供的LTL2BA的类似测试平台具有相同的假设（见图3）。我们随机抽取了1000个生成的公式，其中包含10个节点和3个原子。我们的原型完全是用OCaML [DU]编写的，因此，由于实现语言（和计算机）的极端多样性，与类似作品中发布的其他工具的时间比较几乎没 有 意 义 。 例 如 ， SPIN 工 具 [Hol97] 以 及 LTL2BA 工 具 [GO01] 和LTL2AUT工具[DGV99]都是用C编写的，而EqLTL工具[EH00]是用ML编写的，Wring工具[SB00]是用Perl编写的。请注意，由于测量方法的不实用性，这里没有提到瞬时内存要求。此外，因为我们的转换几乎都是在后台应用的，所以在我们的例子中，内存消耗与结果自动机的大小线性相关。LTL公式状态（以秒为单位的时间）拧LTL2BA BAOM示例来自[EH00]pU（qr）pU（q（r Us））pU（q（r（s（t（uv）（p（p（q阿罗普·阿罗克n（p→qUr）（pi=1. 5米长（pU（qUr））<$（qU（rUp））（pU（qUr））<$（qU（rUp））<$（rU（pUq））（p→qU（3225331377322644533433322955三十一（一百九十五）11452472444示例来自[GO01]（ i=1.. . 10pi）→（q→r））†2（36000）二（四十四）<$（p1U（p2U（. Up8）.. . ）†八（一千二百）8Fig. 1.示例摘自[EH00，GO01]。特希里乌15810个节点3个原子15个节点3个原子20个节点5个原子方法国时间国时间国时间LTL2AUT 6698 127s 11086 453s 25528 2740s拧4043 203s4830 534s 7748 1973年代BAOM3026 3.45s 3318 6.5s472340s图二、LTL2AUT、Wring和BAOM之间的比较方法公式avg. 时间 最大时间avg. 国最大国LTL2BA2000的情况。010的情况。04四、5139BAOM10000的情况。0030的情况。093 .第三章。0616图三. LTL2BA和BAOM之间的松散比较。5结论我们已经成功地设计了一个有效的算法，基于语法的考虑，与技术设计用于上的，可移植的。这表明，仔细检查公式的解析树可以得到与基于后验模拟的方法相似或更好的结果。在实际应用中，效率也是由于在我们的数据结构中大量使用了BDD，但是由于原子命题的数量很少，这种优势在我们的测试用例中并没有真正表现出来。与其他类似工具相比，改进的主要原始因素是在我们修订的扩展规则中引入了有限d前缀，以及我们结合公式之间的句法含义开发的公平范式。然而，显然应该对d的值、公式的形状和产生的自动机的大小之间的关系进行更仔细的研究。至于合并状态技术，它似乎在准冗余或不相容的子公式的情况下有影响（这通常是随机生成的公式的情况），但请注意，我们的工具的当前实现应该开发更有效的技术，如哈希缓存（如BDD算法中使用的），以处理非常大的公式的解析树。事实上，目前还没有明确地计算出更复杂的语法算法（正在审查中）和实际效率之间的良好比率，更重要的是，因为以前的工作主要集中在模型理论方法上。然而，我们主张，句法层面可以特希里乌159更多的信息，以合理的成本。我们进行的基准测试倾向于支持这一说法，尽管这些测试主要涉及随机公式。为了获得有趣的基准，我们只想测试确认作者衷心感谢Robert de Simone富有成效的讨论和合作。引用[BCM+92] JerryR.作者：Edmund M.作者：Kenneth L.作者声明：David L. Dill和L. 黄哲伦符号模型检验：10e20状态及以上。信息与计算，98（2）：142[Bou97] Amar Bouali. Xeve：一个esterel验证环境（版本v1.3）。技术报告RT-0214，INRIA Sophia-Antipolis，1997年12月[DGV99] Marco Daniele，Fausto Giunchiglia和Moshe Y.瓦迪改进的线性时序逻辑自动机生成。计算机辅助验证国际会议，第249-260页，1999年[DU] 文 档和 用户 。目 标 caml系 统3.02版 。[EH00]Kousha Etessami 和Gerard J. 霍尔茨曼优化Buchi自动机。在并发理论上，第153-167页，2000.[GO01] Paul Gastin和Denis Oddoux。快速ltl到bchi自动机翻译，2001。[GPVW95] Rob Gerth，Doron Peled，Moshe Vardi和Pierre Wolper。线性时态逻辑的简单的自动验证。在方案规范测试和验证中，第3-18页，波兰华沙，1995年。查普曼大厅。[Hol97] GerardJ. Holzmann.模型检查器SPIN。软件工程，23（5）：279[SB00] Fabio Somenzi和Roderick Bloem。由ltl公式构造的高效bchi自动机。计算机辅助验证国际会议，第53-65页，2000年[VW94] Moshe Y.瓦迪和皮埃尔·沃尔珀关于无限计算的推理。信息与计算，115（1）：1