模型检测理论是逻辑学和计算机科学的一个交叉领域，作为模态逻辑的一个重要分支时间逻辑，它的繁荣发展就出现在这一领域。数理逻辑和计算机理论科学中的最高奖图灵奖曾于1996年和2007年两度颁给对模型检测有重要贡献的三位科学家。20世纪90年代后期，模型检测的研究基础才稳固下来，它对逻辑学界的影响以及逻辑学界对它的重视也开始日益明显。　　在逻辑、数学和计算机科学的交界处，有着长久的受重视的传统，模型检测思想和这个传统有着相同的起源，著名的Büchi定理、 Church的序列电路乃至图灵机都可以为此佐证。然而，从模态/时间逻辑的角度出发来研究模型检测理论在纯逻辑学界却是一个新课题，笔者第一次站在逻辑学的视角下，勾勒出模型检测和应用于计算机科学的时间逻辑的发展图景。模型检测是关于时间逻辑可满足性判定问题的研究，其研究的两类实体一是关于刻画程序计算性质的逻辑公式，二是用来刻画程序的模型，模型检测的任务就是要校准这两种不同形式的信息——公式和模型——是否相一致。　　线性时间逻辑LTL是应用于计算机科学的一种最基础的模态逻辑，而LTL的模型检测理论也是这个领域中最基础的部分。笔者将模型检测理论的研究内容划分为两部分:一是可满足性问题研究，二是模型检测问题研究，前者研究对于某个时间逻辑公式是否存在可满足的模型，后者研究对于给定模型某个时间逻辑公式是否可满足。表列、自动机、博弈通常被认为是用于解决模型检测问题的三种元逻辑技术，笔者分别详细阐述了线性时间逻辑LTL基于表列、自动机、博弈的模型检测理论，并对这三种判定方法进行了比较研究。在考察了三种元逻辑的基础上，对一种新兴的扩展时间逻辑——动态线性时间逻辑DLTL——进行了全面的更为完整的定义，并使用目前流行的博弈方法给出DLTL模型检测问题的一个解决方案。概括说来，笔者的主要工作和创新点包括以下四个方面。　　第一，在对模型检测的任务和步骤进行了简单概括之后，从新的思路出发，以模型检测中的核心问题“判定性问题”为线索，系统地回顾了模型检测的萌芽、初步形式、正式提出和广泛应用、各种扩展时间逻辑的提出四个阶段。　　第二，在对字逻辑、线性时间逻辑LTL、程序与计算、并发程序等进行概括介绍的基础上，深入探讨了三种元逻辑方法以及它们应用于LTL的模型检测理论，即LTL基于表列的模型检测理论、LTL基于自动机的模型检测理论、LTL基于博弈的模型检测理论，以可满足性问题研究和模型检测问题研究为主要内容，对相应的判定过程分别证明了其可靠性和完全性。　　第三，从新的角度将LTL和DLTL同时定义在标号转换系统的路径和字模型的字上，以此建立起LTL、自动机、DLTL之间的内在联系。之后在前人工作的基础上，对DLTL的语义进行了全新的更为完整的定义，尝试使用博弈的判定方法探讨DLTL的模型检测理论。　　第四，从哲学和逻辑学的立场出发，对应用于模型检测的表列、自动机和博弈进行了比较研究和哲学分析，在较为宽广的背景下探讨这项研究的理论意义，尝试着展望未来的发展前景并分析了可能进一步探讨的方向。　　时间逻辑在模型检测中完成了从理论到应用的一次转变，也将模型检测引入到模态逻辑中为模态逻辑的发展加大了马力。目前，国内逻辑学界对时间逻辑和模型检测的研究还非常薄弱，而国内计算机科学界对模型检测的研究已经兴起。笔者相信，这一项研究会为模型检测在国内逻辑学研究中作出一定的贡献，在不断地从理论到应用交替发展中，也会为国内计算机科学中模型检测的后继研究提供适当养料。