线性时态逻辑(LTL)现今已被广泛运用于计算机科学领域(CS)。它常作为描述系统行为的性质语言,用在程序验证、程序综合与人工智能(AI)等研究方向。比方说,为了验证给定的系统是否满足其对应的性质规范(通常是用LTL来书写的),模型检测技术会将该性质的否定转成与其等价的Buchi自动机,把它与系统模型求交得到新的自动机,并在这新的自动机上检查其接收的语言是否为空,从而可以判定系统是否满足该性质。从LTL在CS中的应用场景我们可以抽取出LTL的两个基本研究问题：一是从LTL公式到与其等价的Buchi自动机的转换算法,这个算法要被频繁的应用于程序验证、程序综合等方向；还有一个就是LTL公式的可满足性检查问题-这是因为在实际的应用场景中不可满足的公式是没有意义的。本文因此就以上两个问题展开,提出一些新的算法与解决方案。我们首先探索从LTL公式到其等价的Buchi自动机的转换问题,并提出一种新的转换算法(第三章)。和其他方法相比,我们的方案避免了中间自动机的生成,这就潜在的可以加快构造的进程。我们实现了该算法并与SPOT工具作了比较-SPOT是目前为止公认度较高的最好的LTL到Buchi自动机的转换器。实验表明我们工具生成的结果可以和那些从SPOT中得来的结果相媲美,在特定情况下还好于对方。由于SPOT已经被持续开发和维护了超过十年的时间,而我们的工具还只是一个原型,这就较好的说明了我们算法的有效性。更重要的是,我们从上述转换算法中得到一个新的LTL推理框架,并将它成功的应用在了LTL的可满足性检查上面(第四章)。该方法的出发点是：在我们提出的框架下存在一个明显的优化技术,可以极大的加速LTL可满足性检查的过程。通过使用我们定义的LTL公式的“义务集合”的概念,我们可以快速的判定公式的可满足性。我们将该算法与基于BDD-模型检查的算法进行了比较,实验表明我们的算法要优于对方。除此之外,我们还建立了一个综合性的比较：将现有的所有LTL可满足性检查的算法放在一起进行性能测试。初步结果表明没有一种单独的方法能够打败其他的所有方案。为了构造一个性能更优的LTL可满足性检查工具,我们采用了两种方式：一是开发一个组合式的(portfolio)LTL可满足性检查器Polsat(第七章),它集成了已知的所有LTL可满足性检查工具,并且被设计成给定一个输入公式,Polsat返回的都是这些集成工具中最好的结果。使用这种方式,我们成功的得到了一种可以为任意公式给出其最优的可满足性检查结果的工具；另一种方式是将我们的框架编码归约到SAT框架下,使得我们的算法能够充分利用当今SAT求解器的优秀性能(第五章)。实验表明这种新方法在所有已知的方法中能够得到最多的最优检查结果,并且从总的性能上来说也是最优的。为了扩展我们方法的应用场景,我们还将其调整用于LTLf的可满足性检查(第六章)。LTLf是LTL的一个变种,它的语义是解释在有限序列上的。它更多的是被用于人工智能(AD方向。已知的LTLf可满足性检查方案是将其转换到LTL可满足性检查框架下进行求解。然而检查LTL的可满足性需要去寻找一个可被接收的环(fair cycle)-这对于LTLf马来说却是不必要的。因此,用检查LTL可满足的方法来检查LTLf先天上就可能造成潜在的浪费。而我们的贡献就在于找到了一种直接在LTLf层面上进行可满足性检查的方案,且这种方案还是基于我们之前提出的框架下实现的-这就使得我们的LTLf可满足性检查的方法继承了之前框架下的所有优点,但却要比之前的方案更加简单。实验证明了我们的猜想,我们的新方法明显要优于将LTLf可满足性检查归约到LTL下求解的方案。