模态逻辑是逻辑学领域最重要的分支之一。特别是克里普克可能世界语义学的建立,使模态逻辑有了准确可靠的语义模型,促进了模态逻辑的快速发展。模型检测技术是形式化验证领域的重要组成部分,可以对软硬件系统的正确性进行高度自动化的验证,在软件工程领域和工业界备受瞩目。而如何避免状态空间爆炸问题、系统性质正确描述和长反例理解是模型检测技术面临的三个主要挑战。如何将模态逻辑这一强大工具有效地应用到模型检测技术中,提高对大型复杂系统进行检测的能力,从而保证系统的可靠性与安全性是一项意义重大的工作,同时也是理论计算机科学与软件工程领域的一个重要研究内容。针对该课题,本文主要在以下几个方面进行了研究:(1)提出了一种有限状态迁移系统模型的状态空间约简方法。该方法通过适当选取自函子的终结余代数,通过模态逻辑理论中的互模拟等价关系来产生最小的有限状态迁移系统模型。使得该迁移系统能够完全等价地模拟原迁移系统的所有行为,保证系统验证的等效性,有效地避免对系统进行模型检测时的状态空间爆炸问题。(2)在Global作用域下构造了一类可以正确描述系统性质的抽象CTL公式模板。首先,通过对系统性质与系统行为进行研究,阐述了以组合命题作为模式与作用域参数的形式化描述研究的可行性与必要性。然后,通过对线性时序逻辑LTL与分支时序逻辑CTL的研究,给出了用CTL描述系统性质的方法。同时,通过重新定义的三个逻辑运算符来简化公式,使构造的CTL公式模板更加简洁,易于理解。最后,构造出Global作用域下所有模式的CTL公式模板,用来生成由组合命题类、模式和作用域定义的描述系统复杂性质和行为的CTL公式。针对所构造的CTL公式模板,给出了模板正确性的证明,说明该方法构造的CTL公式模板可以生成正确的CTL公式。(3)在Before等作用域下构造了可以正确描述系统性质的抽象CTL公式模板,从而完善了所有作用域与模式组合的CTL公式模板类。首先,通过对将来区间逻辑FIL的语法和语义研究,说明将来区间逻辑FIL在刻画系统性质和系统行为方面表达能力的不足。特别是对Prospec描述结果的表示形式上,CTL无疑具有不可替代的优势,而且CTL也是现在众多优秀模型检测器的输入语言。然后,通过对系统行为进一步研究,扩展了接受组合命题作为参数的全部抽象CTL公式模板类,使CTL公式模板构造完整化。接着,通过证明得出,所构造的CTL公式模板可以正确地产生系统性质和行为描述的CTL公式,描述结果简洁有效。这些模板可以集成到现有的以CTL为输入语言的模型检测器中,作为模型检测中的系统性质描述工具。最后,给出了 CTL公式模板的生成实例。(4)提出了一种基于带权偶图演化的不可满足子式求解算法,用来求解近似最小不可满足子式。首先,给出了偶图演化与带权偶图演化定义。然后,分析了不可满足合取范式的极大可满足子式与极小不可满足子式以及与最小不可满足子式之间的关系,并给出了它们之间的关系定理。最后,通过带权偶图演化的数学模型,给出求解近似最小不可满足子式的算法,同时给出了该算法正确性的证明与分析。该方法以从无到有的方式自动生成近似最小不可满足子式的子句集合,能够快速准确地求解出CNF公式的近似最小不可满足子式。从而最大程度地剔除系统不满足验证性质时反例中的无关变量,提高系统错误诊断的效率。