模型检验是一种基于对系统的状态空间进行穷举搜索的自动验证技术。对并发和实时系统进行模型检验时,状态数目往往随着并发分量和系统中无穷的时间值数目的增加呈指数增长；因此,当实时系统的并发数量较多时,直接对其状态空间进行穷举搜索是不可行的,这就是所谓的状态爆炸问题。随着模型检验技术在各个领域的深入应用,状态爆炸问题日益成为其广泛应用道路上的最大障碍,如何缩减状态空间避免状态爆炸已经成为模型检验技术亟待研究的一个重要课题。有鉴于此,我们进行了关于模型检验状态空间缩减技术方面的研究。　　 本文首先探讨了模型检验的一般过程及其框架,接着简单介绍了已有的模型检验工具，在此基础上详细地分析了状态爆炸问题产生的因为,为新模型的建立和状态的表示奠定了必要的基础，最后详细讨论了缩减模型检验状态空间的技术和实现方法。状态空间的大小和系统的模型、模型的形式化表示和公式的形式化表示有着非常密切的关系；因此,在马尔可夫链和二元决策图的基础上,引入了模糊马尔可夫链,用MTBDD来对系统模型进行形式化表示,用ROBDD对其状态公式进行形式化描述,并且采用了偏序和飞行式检测等辅助优化技术来缩减模型检验的状态空间,尽量避免状态爆炸问题。最后,为了便于对BDD和MTBDD等实现操作,开发实现了MRDD程序包。