线性时态逻辑（Linear Temporal Logic, LTL）在系统验证中扮演着重要的角色，它被广泛的应用于复杂系统的时态推理与模型检查。本项目面向线性时态逻辑LTL的基础理论，研究LTL的可满足性的判定理论、算法以及潜在的应用。本项目力图深入挖掘线性时态逻辑的数学特征，探索新颖并具有高效性能的可满足性判断过程。本项目的研究目标包括如下三方面:1）研究可满足/不满足无限序列所具有的数学特征，如对于给定的LTL公式，一个无限序列满足/不满足该公式应该具内在特征以及与公式的关系;2）研究LTL可满足判定的新算法，包括利用SAT技术与机器学习技术加速LTL可满足判定过程；3）研究LTL可满足判定在系统测试及人工智能逻辑领域的应用，把基于可满足判定的新算法应用于系统测试的研究，并把该方法学拓展到人工智能领域逻辑的分析过程（如有限迹的线性时态逻辑的分析与验证）。

Linear Temporal Logic (LTL) plays an important role in the system verification, which is widely used in the model checking and temporal property reasoning for complex systems. This proposal tries to explore the basic theory of LTL and to study the theory, algorithm and application for its satisfiability decision procedure. We would like to exploit the mathematic characteristics for linear temporal logic and to design the new decision procedure, which takes the different way to improve the performance of solvers. The goals of this study include the following aspects: 1)Study the mathematic properties of satisfiable/unsatisfiable trace; 2)Study the new algorithm for LTL satisfiability checking, including how to utilize the SAT solver and machine learning techniques to accelerate the performance; 3)Study the application of LTL satisfiability decision procedure. One is to apply the technique to the run verification field, and the other is to apply the technique to the LTL analysis and verification on finite trace in AI field.