形式化验证是用严格的数学方法来证明系统设计是否满足规约的验证方法。近几年来基于模型检测的形式化验证工具的使用范围不断扩大,而且大量的实例证明了模型检测在发现问题方面的能力。可以说,模型检测是自动推理在计算机科学中最成功的应用之一。自动机理论为线性时序逻辑模型检测提供了统一的算法框架。标准线性时序逻辑模型检测由线性时序逻辑公式转换为Büchi自动机、计算自动机的乘积和积自动机语言判空的三个步骤构成。结果自动机的质量直接决定了模型检测的应用范围,因此,产生状态数和迁移数少,接受状态简单的自动机成为了模型检测的研究重点。在模型检测中,自动机A可以替代另一个自动机A的条件是两个自动机所识别的语言相同,而语言相同的计算是十分困难的。因为模拟蕴含着语言的包含关系,而且计算直接模拟、公平模拟以及延迟模拟的时间复杂度为多项式时间,因此在实际中一般借助各种模拟的概念来完成对自动机的优化。K-模拟(当K = 1时对应的就是各种普通模拟)的实质就是对应于反对者的每次移动一颗宝石,拥护者可以移动K颗宝石。基于K-模拟可以对Büchi自动机进行更大程度的优化。本文研究了基于K-模拟的Büchi自动机优化算法。线性时序逻辑可以更自然的转化为广义Büchi自动机,广义Büchi自动机的接受状态为l个集合,而其状态数为等价Büchi自动机的1/l。因此直接对广义Büchi自动机进行优化是十分重要的工作,本文研究了基于直接模拟,延迟模拟,公平模拟的广义Büchi自动机优化算法。基于左右语言的优化是完全基于自动机理论的优化方法,所谓左语言是指从初始状态到指定状态的语言,而右语言是指从指定状态到接受状态的语言。K-模拟为左右语言的计算提供了一个高效的算法,本文研究了基于K-模拟的左右语言的Kripke结构,Büchi自动机以及广义Büchi自动机的优化方法。应对模型检测中“状态爆炸”问题的一个自然的方法是对系统进行分解,通过验证各子系统上的性质,然后根据这些性质推导出系统的性质。在验证各子系统的性质时一般需要考虑其环境的影响,Pnueli提出的假设/确保方法就是组合验证的一个成功的方法。但是该方法实现的瓶颈是存在模拟的计算,为此,本文研究了应用广义Büchi自动机的公平模拟替代存在模拟的组合验证以消除这一实现瓶颈。尽管模型检测取得了很大的进步,但是对于大系统的验证能力依然有限。在众多的状态减少和压缩技术中,抽象技术是最有效的方法之一。本文深入研究了基于K-模拟的抽象的高效算法,并证明了在线性时序逻辑框架下抽象的可靠性和完备性。