LTL中可满足性测试的Tableau工具的实施和实验分析

理论计算机科学电子笔记262（2010）113-125www.elsevier.com/locate/entcs用于LTL中可满足性测试的Tableau工具：实施和实验分析Valentin Goranko1丹麦技术大学千克 林比安杰洛·基里洛夫2 德米特里·什卡托夫3南非约翰内斯堡威特沃特斯兰德大学计算机科学学院摘要我们报告的实施和实验分析的增量多通表为基础的pr ocepalaWol per的线性时间项poral逻辑LTL，基于广度优先搜索策略的测试的满意度。我们描述了实现和讨论的几个系列的模式公式，以及一些随机测试集上的工具的性能，并比较其性能与S chwendimann的一次通过tableaux由Widmann和Go r ′ e的实现的几个代表tati v e系列的模式公式，包括可能性和安全模式。我们的实验已经建立，Schwendimann的算法一致，有时显着，优于增量tableaux，尽管事实上，理论上最坏情况下的上限Schwendimann的算法，2EXPTIME，是比沃尔珀的算法，这是EXPTIME。这再次表明，理论上建立的最坏情况复杂性结果并不总是真实地反映实际效率，至少在比较决策过程时是这样。关键词：LTL，满意度检查，增量表，实现，一遍表。1介绍用于命题线性时间逻辑LTL的多遍增量式基于表的决策过程在[17]中首次发表;该过程建立在最初由Pratt在[11]中为命题动态逻辑 PDL大约在同一时间，1电子邮件：vfgo@imm.dtu.dk2电子邮件：angelo@cs.wits.ac.za3电子邮件：dmitry@cs.wits.ac.za1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.04.009114诉Goranko等人理论计算机科学电子笔记262（2010）113Ben-Ari，Manna，and Pnueli [2].随后，开发了一些基于增量tableau技术的其他决策程序，包括我们最近关于具有公共和分布式知识的多代理epis-temic逻辑的工作[5，8]，关于时间认知逻辑[6，7]和战略能力逻辑[4]。一次通过tableau程序首先由Schwendimann在[13，14]中为LTL开发，最近由Abate，Gor′e和Widmann在[1]中应用于CTL众所周知，LTL的最坏情况复杂度是PSPACE [16]。然而，除非应用基于时间的修剪，否则增量表在EXPTIME中工作，而Schwendimann方法的最坏情况复杂度在本文中，我们报告的实施和初步的实验分析的增量table-based的prooceptia `la-wolp 为 LTL 。该 实 施 方 式 可 在 www.example.com 在 线 获 得http://msit.wits.ac.za/ltltableau。我们描述了该工具的实现，讨论了它在几个模 式 公式 系 列 和一 些 随 机 测试 集 上 的性 能 ， 并 将它 与 Widmann 和 Go r ′ e 的Schwendimann的one-pass tableau在几个典型模式系列上的性能进行了比较。我们的实验表明，Schwendimann算法始终，有时显着，优于形式 Schwendimann在合理的时间内产生相应的自动机，我们的基于多遍表格的工具也无法建立非有效性。我们注意到，这里比较的两个实现都没有任何特殊的优化技术的帮助;因此，我们基本上比较了两个算法的“纯”形式。特别是，我们的工具实现了[ 17 ]中算法的标准版本，基于广度优先搜索策略，因此在检查其中是否存在开放分支之前构建了整个tableau。此外，应该考虑到我们的工具是用Python编程语言编写的，而R。 去r'e和F。Widmann的工具是用OCaml语言编写的，众所周知， 比Python快100，在比较两个实现的运行时时应该考虑到这一点。众所周知，例如，从描述逻辑的研究，有时算法理论上计算困难的问题可以解决大多数实际上重要的问题有效，特别是当与优化技术增强。显然，在LTL的情况下，我们也面临着类似的现象，这证实了在确定算法的实际效用时，理论上的最坏情况复杂度结果应该持保留态度本文作为一个系统的描述，只报道了上述两种表法的实验性能比较。对结果的深入理论分析将在后续工作中提出诉Goranko等人理论计算机科学电子笔记262（2010）113115不不PTP00不0不UTT2LTL的增量多通道表的说明在这一节中，我们简要地勾勒出增量tableau过程的LTL，其实现报告在本文中。我们假设读者熟悉LTL的语法和语义（否则，参见例如，[17]或[3]）。简而言之，用于测试LTL公式的增量Tableau程序满足性θ试图构造一个图θ，称为表，表示θ的许多Hintikka结构，如果任何Hintikka结构满足θ，那么至少有一个由θ表示的结构满足该公式。θ的Hintikka结构本质上是θ模型的有限部分表示。不难证明LTL公式在模型中是满意的，如果它在Hintikka结构中是满意的（有关详细信息，请参见，例如，[6]）。因此，如果θ的过程成功，则LTL公式θ是满足的画面程序包括两个主要阶段：构造和消除，后者又包括前状态消除和状态消除。在构造阶段，生成一个有向图θ-，称为θ-的预表它的节点集包含了tableau的节点集θ 这个过程最终要建立的。 节点θ 是 LTL公式的集合，其中一些--被称为状态--表示Hintikka结构的状态（因此，也是模型的状态），而另一些--被称为前状态--完全扮演了一个技术角色，特别是帮助保持Pθ有限。在前状态消除阶段，较小的图Tθ 而生产出来Pθ-被称为θ -的初始画面，通过消除所有的前状态，Pθ，因为它们已经完成了它们的作用，并重新定向边缘。最后，在状态消除阶段，所有的，如果有的话，状态θ被删除在Hintikka结构中不能满足的，出于以下原因之一：要么它们明显不一致，即，包含一对互补的公式，或包含不可实现的可能性（即，公式的形式，使得沿着包含来自所讨论的状态的N的状态不能到达包含N的状态），或者不具有任何后继（这违反LTL语义），例如，因为它们的所有后继可能已经被更早地消除请注意，删除整个过程的结果是θ的一个（可能是空的）子图θ，称为θ的最终表。 那么，如果存在某种状态Δ，含θθ，则该过程宣告θ是满意的;否则，则宣告θ是不满意的。完备性证明展示了如何从一个非空的最终画面中构建一个Hintikka结构，从而构建一个模型，而可靠性证明则展示了任何不满足的公式的最终画面将永远是空的。我们将在下一节中简要描述上述三个阶段，同时描述实现。在此之前，我们需要介绍一些标准的术语和符号，稍后将使用。下表列出了分类为α（连词）的LTL公式类型116诉Goranko等人理论计算机科学电子笔记262（2010）113X∈∈∈ ∈ ∈∈∧ ∨ →¬和βαα1α2ββ1β2¬¬ϕϕϕ（¬ϕ¬ψϕ∧ψ（Xϕ¬ϕX¬ϕψ¬ψX¬ϕϕ∨ψ（U）（ϕψ¬ψ ∧¬ϕψϕ∧X(ϕ Uψ)<$<$X（ U）Gϕ公司简介G¬ϕXG所有其他的公式（命题参数和常数，以及形式为“”的公式）都被称为本原。与α公式和β公式的情况不同，它们在模型状态下的真值不能被简化为在相同状态下的更简单公式的真值。一组LTL公式α被称为向下饱和的，如果，首先，α这意味着α1 α 1和α2第二，如果β暗示要么是β1β要么是β2β一组公式Δ是集合Γ的最大向下饱和扩张，如果，首先，Δ是向下饱和的，其次，不存在向下饱和的ΔJ使得Γ<$ ΔJ<$ Δ。3执行情况说明3.1语法该算法将待测试的公式（由字符串表示）作为输入，如果发现公式是可满足的，则返回字符串"satisfiable“，否则返回”not satisfiable“。 该实现支持所有常见的布尔和时态连接词。它们是A，O，I，N，U，F，G，X，F，X，公式归纳定义如下：(i) 每一个命题变量，在这里用小写拉丁字母后跟小数编码，比如a12，都是一个公式。(ii) 如果n是一个公式，那么Nn，Xn，Fn和Gn都是公式。(iii) 如果A和B是公式，则（AA）、（BO）、（BI）和（BU）是公式，是公式。3.2数据结构这个表是一个有向图，由状态和预状态组成。通用术语节点将用于指状态或前状态，当区分两者并不重要时。 图被实现为节点列表。 每个 node是包含以下字段的记录id：节点的唯一整数标识符。parents：一个整数列表，包含节点的父节点的id。children：包含节点子节点id的整数列表。诉Goranko等人理论计算机科学电子笔记262（2010）113117−→⇒--−→{|X∈ }type：指定节点类型的字符串。 可能的值为pre、proto和状态。formulas：一个字符串列表，包含在给定节点上为真的所有公式marked：用于检查可能性的布尔标记。suckMarked：显示是否标记后继节点的布尔标记3.2.1施工阶段如前所述，构造阶段生成一个包含两种节点的图，即状态和预状态。从技术上讲，状态与预状态不同，需要向下饱和（见上文）。该图还包含两种边。一种边将预状态连接到状态，在这里用双箭头表示.另一种边将状态连接到预状态，在这里用单个箭头表示（上面提到的原状态是实现的一部分，但在过程的高级描述中没有出现;本质上，它们是公式θ的构造过程始于创建一个单一的预状态θ。之后，该过程在使用下面陈述的规则SR从预状态创建状态和使用下面陈述的规则PR从状态创建预状态之间交替，直到我们达到饱和。SR给定一个尚未应用SR的预状态Γ，执行以下操作：(i) 把所有不明显不一致的Γ的最大向下饱和扩张加到预表中作为状态;(ii) 对于每个新添加的状态Δ，如果Δ不包含形成X，将XT加到J上，称结果为ΔJ;(iii) 对于每一个这样创建的Δ，将Γ ΔJ;J(iv) 然而，如果到目前为止构造的预表部分已经包含Δ，则不要创建ΔJ的新副本，而只需将Γ ΔJ。PR给定一个尚未应用PR的状态Δ，执行以下操作：(i) 将形式为Γ =π πΔ的集合作为预状态添加到预表中，只要它不是明显不一致的;(ii) 对于每个这样创建的r，输入Δ r;(iii) 然而，如果预表已经包含了Γ，那么就不要再创建一个新的Γ的拷贝，而只需将Δ−→Γ。在实现中，构造算法通过创建tableau的初始节点开始。这是用输入公式标记的预状态。这两个构造规则将持续应用，直到没有新节点添加为止。对应于上述规则的两个构造方法称为alphaBetaRules和nextTimeRule。alphaBetaRules方法通过向下饱和的过程从预状态（中间结果称为原始状态）创建状态，nextTime方法从状态创建预状态118诉Goranko等人理论计算机科学电子笔记262（2010）113−→⇒3.2.2消除相消除阶段开始于移除所有前状态和所有边缘并相应地重定向边缘。结果称为初始画面。在此之后，我们开始消除“坏”状态。 回想一下，这些是不一致的状态，包含未实现的可能性的状态，以及没有继承者的状态。 去除预状态和不一致状态是微不足道的。一种简单的检查可能性是否已经被填充的方法可能会导致算法运行很长时间，因此一个更有效的排名过程，称为removeEventualities，用于检测未填充的可能性。它首先在画面中找到所有可能发生的事情，并将它们存储在一个列表中。 对于列表中的每个可能性，算法执行以下操作：(i) 对于每个状态，设置标记为false。(ii) 找到所有满足这种可能性的状态，并将它们标记为真。(iii) 标记其继任者被标记的所有州(iv) 重复步骤（iii），直到没有更多的状态可以被标记。(v) 删除所有包含可能性且尚未标记的状态removeNonSuccessors 过 程 查 找 没 有 后 继 的 状 态 并 将 其 删 除 。 重 复 应 用removeEventualities和removeNonSuccessors过程，直到无法从工作表中移除更多状态为止其结果是最终的画面结构。最后一步是检查最终画面是打开的还是关闭的。要做到这一点，我们检查画面是否包含任何初始状态。这些是包含输入公式的状态。如果发现表是打开的，则算法返回“satisfiable”，否则返回“not satisfiable”。3.3Tableau算法如上所述，主要的tableau算法如下图1所示4测试和分析4.1正确性测试生成了大量随机公式，用于对实施的 这些都是在我们和其他可用的工具上测试的，特别是在R上。 去r'e和F。 Widmann对Sch wendi-mann的一次通过表的实现，也被选择用于性能比较。在移除了早期版本中的错误之后，这两个工具在所有测试中都返回了一致的结果运行时间的比较在本文的其余部分。所有测试均在Intel Xeon 8核架构、8 GB RAM和Mac OS X v10.5操作系统上进行。我们的工具是用Python编程语言编写的，而R。 去r'e和F。维德曼诉Goranko等人理论计算机科学电子笔记262（2010）113119Test（公式）{tableau = constructPretableau（formula）tableau = removepre-states（tableau）tableau = removeInconsistent（tableau）while（True）{return current;tableau = removeEventualities（tableau）tableau = removeNonSuccessors（tableau）if（current== tableau）{}}return isOpen（tableau）}Fig. 1. LTL公式语言。四、 在所有测试过程中，都仔细监控了这两个工具的内存使用情况，以确保它不会耗尽。这将导致计算机开始使用虚拟内存，并大大增加运行时间。在下面报告的任何测试中均未使用虚拟内存另一种测试实现正确性的方法是生成和测试我们知道是满意的公式和我们知道是不满意的公式的大集合。特别地，我们已经使用了由M生成的这样的公式的集合。Montali [10]，其中一个在程序的早期版本中发现了一个错误4.2图案组进行的第一组测试是关于模式系列的。我们使用的模式取自Rozier和Vardi的论文[12]，用于测试性能基于自动机的工具，用于测试LTL公式的满足性本节中的图表显示了这两个Tableau工具的运行时间 在不同的模式上，我们将在下文中称为“Wolper表”和“Schwendimann表”，因为这两种实现都忠实地表示了各自的算法，没有任何可能减慢或加速的特殊功能在特定情况下的表现对于基于自动机的工具在下面呈现的模式上的运行时间，读者可以参考Rozier和Vardi [12]。稍后，我们将简要讨论基于自动机的工具和这里介绍的Tableau工具之间的性能比较。第一个模式是E公式模式，是一个偶然性的结合4两种语言的性能速度之间的精确比率无法确定，因此，比率取决于特定的计算任务，但众所周知，Ocaml可以比Python快100倍，在比较两种实现的运行时时应该考虑到这一点120诉Goranko等人理论计算机科学电子笔记262（2010）113F FFGGB.G.U UU形式为p1p2pn.该模式在n = 1至n = 10的输入大小上进行了测试。运行时间如图2所示。150 0，00013113 0，0001075 0，0000738 0，0000301 2 3 4 5 6 7 8 9 10沃尔珀01 2 3 4 5 6 7 8 9 10施文迪曼图二. E公式的运行时间Wolper当输入超过n=7时，我们看到运行时间呈指数级急剧增加。这种增加是由于检查可能性是否实现的程序造成的。例如，当n=10时，程序在画面中生成超过120 000个节点，并且必须检查10个可能性。另一方面，Schwendimann的表的运行时间下一个测试的模式是S-公式模式，其形式为p1p 2...pn. 在这个公式模式中没有任何可能性，所以我们应该期待与E公式模式相比，效果要好得多。事实上，图3中的图表证实了这一预期。50，00，150037，5 0，112525.0 0.075012.5 0.037501100200300400500600700800900 1000沃尔珀011002003004005006007008009001000施文迪曼图3.第三章。S公式的运行时间这两种算法都在二次时间内对这个模式系列执行，因为这些公式不涉及分支和偶然性。Wolper表的运行时间主要取决于去除预状态的过程，这是一个代价高昂的过程，特别是在高度连通的图中。然而，两种算法的运行时间之间的差异只是一个常数。接下来的两个模式涉及嵌套的Until运算符。其中第一个，U1-公式模式，嵌套在第一个参数中：（（（p1p2）p3）... pn）。两种算法的运行时间如图4所示。同样，Wolper这是因为，对于一个大小为n的公式，有n个可能性需要检查。秒秒诉Goranko等人理论计算机科学电子笔记262（2010）113121U UUGF公司简介40 0001130 0，0000820 0，0000610 0，0000302 3 4 5 6沃尔珀02 3 4 5 6施文迪曼见图4。 U1公式的运行时间此外，对于n=7，程序生成超过68000个节点。再一次，SchwendimannU2-formulas 模 式 在 Until 的 第 二 个 参 数 上 有 嵌 套 ， 形 式 为 （ p1（ p2 ）（p3）... pn））。 这种模式的公式也包含n种可能性，但与U 1 -公式模式相比，Wolper这就是为什么该算法能够验证更大的输入公式。运行时间见图5。Schwendimann50 003038 002325 0，0015十三万零八02102030405060708090100沃尔珀02102030405060708090100施文迪曼图五.U2公式的运行时间最后的模式集是所谓的C公式模式.它们由形式为π的子公式组成。 模式C1是这些子式的析取， 并且C2是这些子式的合取。 算法的运行时间C1-公式如图6所示。Wolper 少量的状态允许程序在合理的时间内检查所有n个可能性。 运行时间SchwendimannC2句型是一个连词，其形式为p1p 2......这是什么？pn.算法在C2公式上的运行时间如图7所示。Wolper的tableau的运行时间需要检查是否秒秒122诉Goranko等人理论计算机科学电子笔记262（2010）113500 0.04375 0.03250 0.02一百二十五点零一分02 100 200 300 400500沃尔珀02 100 200 300 400 500施文迪曼见图6。C1公式的运行时间500 0，00020375 0，00015250 0，00010125 0，0000501 2 3 4 5 6 78沃尔珀01 2 3 4 5 6 7 8施文迪曼见图7。C2公式的运行时间许多可能性被填满，加上大量的状态，导致性能不佳。Schwendimann用于比较沃尔珀表和施文迪曼表的其他模式系列是由M。蒙塔利[10]。 这些模式使用两个参数n，d，在图8和9的图表的横坐标上示出，其中运行时间 这两种工具都有。第一个参数是命题变量的数量，第二个参数是时间模式的嵌套深度。例如，在其中一个系列中，公式F（a1<$X F（a1<$XFa1））具有参数（1， 2），这意味着它包含1个变量，而模式XF具有嵌套深度2。关于其他模式的描述和更多细节，请参见[9]。10000,001000,00100,0010,001,000,100,010,000,000,001,11.4二，二2.5三，三4.1四四五，二五，五六、三7.1七四八、二八点五9，3 10，1 10，4 11，2 11，5 12，3 13，1施文迪曼·沃尔珀图八、Montali满意公式的运行时间秒秒诉Goranko等人理论计算机科学电子笔记262（2010）11312310000,001000,00100,0010,001,000,100,010,000,000,001,11,42,22,53,34,14,45,25,56,37,17,48,28.5 9.310,110,411,211,512,3施文迪曼·沃尔珀图第九章Montali不可满足公式的运行时间1000.0000100.000010.00001.00000.10000.01000.00100.00010.0000施文迪曼·沃尔珀图10. 随机公式的运行时间4.3随机公式使用随机公式生成器生成不同尺寸的随机试验公式。 使用的参数是：ndWolper的tableau能够在非常合理的时间内验证嵌套深度较低的公式。 当深度增加到5及以后，算法开始挣扎。正如我们从图10中所看到的，该图显示了两个变量的随机公式，嵌套深度为5，某些公式远远超过0.5秒。 这些都是图中，其中一些达到超过100秒的时间。对于超过6个命题变量和嵌套深度超过5的随机公式，Wolper4.4与基于自动机的工具的性能比较在他们的论文中，Rozier和Vardi测试了基于显式和符号自动机的LTL满足性检查工具。Wolper的tableau的实现与显式工具相当，但不如符号工具有效。 对另一方面，Schwendimann秒124诉Goranko等人理论计算机科学电子笔记262（2010）1134.5结果总结本文 中报告 的实验 分析的 目的是 验证实现 的正确 性，测 试性能 ，并将 其与Schwendimann的tableaux的性能进行比较。性能测试的结果可用于确定该工具在工业应用中的适用性，至少对于特定的公式模式。正确性得到了成功的验证，因为Wolper tableau的最新版本的实现至于性能，对于没有可能性的公式模式， Wolper的tableau和Schwendimann的tableaux的运行时间以相同的速率增长，通常Schwendimann的tableau的运行时间的增长具有低得多的常数因子。然而，对于上面描述的导致生成许多节点并且存在许多可能性的公式模式，Wolper的tableau的运行时间5结论意见和今后的工作在未来的工作中，我们打算从理论上分析和比较增量多遍，和一遍tableau方法，并提供后者的优越性能的理论解释，同时确定优越性能的范围，并指出多遍tableaux执行更好的情况。我们还计划研究这两种方法的优化技术。特别是，我们打算基于深度优先而不是广度优先的搜索策略实现Wolper al-tax的修改版本研究这种优化技术的最终目标是设计一个6致谢这项工作是基于第二作者（A。Kyrilov），由其他两位作者监督。它得到了南非国家研究基金会的部分支持。我们感谢RajeevGor′e和FlorianWidmann为我们提供了Schwendimann的一次通过过程的实现，并对其优点进行了许多讨论-本文可以被视为，除其他外，Rajeev的持续辩护，但模态逻辑社区在很大程度上耸耸肩关于Schwendimann的一次通过表方法的优越的实用性能。我们也感谢Marco Montali在早期的测试中发现了一个bug。诉Goranko等人理论计算机科学电子笔记262（2010）113125版本的工具，并为我们提供了他的基准公式系列。最后，我们感谢匿名推荐人的建设性和令人鼓舞的评论。引用[1] 彼 得 罗 · 阿 巴 特 ， R ajeevGo r'e ， 和 弗洛 里安 · 威德 曼。 计 算树逻辑的一 次 通 过 表 格 。 在 NachumDershowitz和Andrei Voronkov编辑的Proceedings of LPAR 07，卷4790 of Lecture Notes in ComputerScience，第32-46页中。Springer-Verlag，2007.[2] M. Ben-Ari，A. Pnueli和Z.吗哪分支时间的时间逻辑。在Proc.8th ACM Symposium on Principles ofProgramming Languages中，也出现在Acta Informatica，20（1983），207-226，第164-176页[3] E. 艾 伦 · 爱 默 生 时 态 和 模 态 逻 辑 。 在 J. van Leeuwen ， 编 辑 ， Handbook of Theoretical ComputerScience，卷B，第995麻省理工学院出版社，1990年。[4] 瓦伦丁·戈兰科和德米特里·什卡托夫多智能体系统中策略能力逻辑的基于表格的决策程序。发表在ACMTransactionsonComputationalLogic上。可在www.example.com上http://tocl.acm.org/accepted.html。[5] 瓦伦丁·戈兰科和德米特里·什卡托夫基于表的决策过程的多智能体认知逻辑与运营商的共同和分布式知识。在 Antonio Cerone 和 Stefan Gunter ， 编 辑 ， 第 六 届 IEEE 软 件 工 程 和 形 式 方 法 会 议 论 文 集 （ SEFM2008），第237IEEE Computer Society Press，2008.[6] 瓦伦丁·戈兰科和德米特里·什卡托夫线性时间的完全联盟多智能体时间认知逻辑的基于表格的决策过程。在Decker，Sichman，Sierra，and Castelfranchi，editors，Proc.第八届国际自主代理和多代理系统会议（AAMAS 2009），2009年5月，匈牙利布达佩斯。[7] 瓦伦丁·戈兰科和德米特里·什卡托夫分支时间的完全联盟多智能体时间认知逻辑的基于表格的决策过程。在出现在：Proc.的研讨会正式方法多智能体系统FAMAS[8] 瓦伦丁·戈兰科和德米特里·什卡托夫 在完全联盟多智能体认知逻辑中确定满足性的基于表格的过程。在Sergei Artemov 和 Anil Nerode 编 辑 的Proc. of the Symposium on Logical Foundations of ComputerScience （ LFCS 2009 ） ， 第 5407 卷 Lecture Notes in Computer Science ， 第 197-213 页 中 Springer-Verlag，2009.[9] M. Montali，P. Torroni，M. Alberti，F. Chesani，E. Lamma和P. Mello。 溯因逻辑程序设计作为一种有效的技术，用于声明性业务流程的静态验证。 J.算法在认知，信息学和逻辑，页面出现，2009年。[10] 马可·蒙塔利 个人交流2009年[11] 沃恩河普拉特一种近似最优的动作推理方法。Journal of Computer and System Sciences，20：231[12] 启彦Rozier和M.Y.瓦迪LTL满足性检查。在第14届模型检查软件研讨会（SPINSpringer-Verlag，2007.[13] S. S CHWENDIMAN。 作为计算逻辑的一部分。 博士论文，瑞士伯尔尼大学，1998年。[14] 斯特凡·施文迪曼 一个新的pltl一遍表演算。 In H. de Swart，编辑，ProceedingsTABLEAUX'98的第1397卷，Lecture Notes in Arti Ficial Intelligence，第277-291页。Springer-Verlag，1998.[15] Roberto Rumintiani，Stefano Tonetta，and Moshe Y.瓦迪符号系统，显式属性：关于ltl符号模型检验的混合方法。在Kousha Etessami和Sriram K. Rajamani，编辑，CAV，计算机科学讲义第3576卷，第350Springer，2005.[16] A. Prasad Sistla和Edmund M.克拉克命题线性时态逻辑的复杂性在STOC，第159-168页。 ACM，1982年。[17] 皮埃尔·沃尔珀时态逻辑的tableau方法：综述。Logique et Analyse，28（110