随着计算机软件硬件系统的越来越复杂，如何保证其正确性和可靠性成为日益紧迫的问题，也是学术界和工业界共同关注的一个重要问题。在为此提出的许多理论和方法中，模型检测(modelchecking)以其有效性和自动化程度高而引人注目。　　模型检测是一种基于模型的、自动的、对系统性质进行验证的方法，它预期用于并发的、反应式系统，最初作为一种开发后方法论出现，是一种对有限状态并发系统进行自动检测的方法。模型检测是基于时态逻辑的，主要涉及到两种时态逻辑：一种是线性时态逻辑LTL(LinearTemporalLogic)，另一种是分支时间逻辑，即计算树逻辑CTL(ComputationalTreeLogic)。模型检测方法检测给定系统的初始状态是否满足LTL或CTL公式。本文对基于时态逻辑进行模型检测的方法进行了扩展，给出了LTL模型检测的近似算法。　　本文首先介绍了线性时态逻辑LTL和计算树逻辑CTL，并给出进行模型检测的三种方法：CTL公式的标记模型检测方法、LTL公式的Tableau模型检测法和基于有序二叉判定图OBDD的符号模型检测。　　然后介绍了近似算法中的贪婪、限制、松弛三种主要策略，实现了利用线性规划对LTL限界模型检测进行近似的算法，并提出了两种近似算法思路。先定义了限界语义，利用限界模型检测技术，把LTL模型检测问题转化为可满足性问题；再利用逻辑公式等价，把得到的命题可满足公式转化为合取范式的形式，便可以利用求解最大可满足问题的线性规划近似算法来解决。　　最后，本文总结了模型检测技术的基本原理和方法，提出后续的LTL近似算法研究工作和方向。