摘要: 模型检测是一种强有力的系统验证技术。在计算机的硬件，通信协议，控制系统等方面的分析与验证中取得了令人瞩目的成功。由于模型检测技术是基于对状态空间的穷举搜索，状态爆炸问题是模型检测技术面临的主要困难。符号化的模型检测技术利用二叉图（Binary Decision Diagram）表示状态转换关系，降低了系统模型所需的内存空间。 同时状态转换的计算可以以集合为单位，提供了搜索的效率。但是并不是所有的状态转换关系都可以用二叉图紧凑的表示。另外符号化的模型检测技术非常依赖于布尔变量的排序，得到一个好的排序需要消耗很长时间。近年来出现了一种新的克服状态爆炸的方法：有界模型检测。该方法的主要思想是把检测系统在有限步行为中是否存在错误归约到命题公式的可满足性的判定上。因为基于搜索的命题公式的可满足性判定过程不存在状态爆炸问题，所以该方法是对符号化模型检测的很好的补充。但是到目前为止有界模型检测能够验证的性质非常有限，就我们所知目前该方法只能验证全称属性，如线性时态逻辑LTL,分支时态逻辑ACTL。本文中我们所做的工作主要是扩展有界模型检测方法，使它能够验证一般化的系统属性。 我们的工作主要包括：1．定义了CTL*的有界语义，并探讨了CTL*的有界语义和无界语义的关系。2．提出了一个算法把CTL*在有界语义下满足性的检测规约到一个QBF(Quantified Boolean Formulas)问题的满足性的判定上，同时证明了算法的正确性。3．对由算法产生的QBF公式，提出了一个深度优先的满足性判定方法。 类似于SAT的判定过程，基于搜索的QBF的满足性的决策过程也不存在状态爆炸问题。因此如果能够把模型检测规约到QBF的满足性的判定上，将是解决状态爆炸问题一个非常有效的方法。本文中我们第一次展示了如何把检测系统满足CTL*描述的性质归约到QBF的满足性的判定过程上。和基于二叉图的符号化方法相比我们的方法使用了更少的内存空间，同时加速了验证过程。和已有的有界模型检测方法相比我们可以验证更多的性质。