线形时态逻辑的可满足性理论与应用研究

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.

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

线性时态逻辑（Linear Temporal Logic, LTL）在系统验证中扮演着重要的角色，它被广泛的应用于复杂系统的时态推理与模型检查领域。本项目面向线性时态逻辑LTL 的基础理论，研究LTL 的可满足性判定理论、算法以及潜在的应用。本项目在三个方面做了深入的研究：..1）LTL的可满足性理论与算法，我们研究了LTL公式本身的数学性质，发现了面向SAT的求解框架，研发了Aalta工具，在典型Benchmarks与国际工具对比，总体性能最优；2）LTL在有限迹下的综合研究，我们是国际上第一个研究了LTL在有限迹下的综合算法，包括安全性与公平性制约下的算法研究，实现了相应的工具；3）面向SAT的模型检查新算法研究，我们发现了一个新的硬件模型检查算法，基于模拟逼近的想法，在实验效果上与主流的验证工具性能相当，形成互补。..研究结果发表在人工智能与形式化方法的重要期刊与杂志，如IJCAI、AAAI、HVC、Formal methods in System Design等。培养了2名博士生，5名硕士生，1名博士后。