模型检测是一种完全自动化的系统可靠性与安全性的形式化验证技术，目前已经广泛应用于集成电路、通信协议、安全协议等软硬件系统的验证。模型检测技术基于对系统状态空间的遍历来完成系统性质的验证与分析，因此状态空间爆炸（系统的状态数目因系统并发量的增加而成指数级增长）问题成为制约着模型检测技术在工业界得以广泛使用的一个主要瓶颈问题。在为克服状态空间爆炸所提出的众多状态空间约简技术中，限界模型检测是最为有效的方法之一。限界模型检测之所以能够达到约简状态空间的目的，主要原因在于限界模型检测技术只关注于验证与系统性质相关的局部空间;同时，限界模型检测技术借助于命题公式满足性判定算法完成检测过程，进一步降低了空间需求。论文对线性时态逻辑LTL的限界检测过程进行了优化，提高了检测的效率，同时将限界检测的思想应用于马尔科夫决策过程的模型检测中，达到了约简状态空间的目的，具体工作包括以下两个方面:　　本文的主要研究内容包括:　　1.对异步系统提出了一种模型简化方法:影响核规约。该方法首先从描述待验证性质的时态逻辑公式中提取出变量集，然后利用状态转换关系递归计算出所有与验证属性相关的变量，从而通过剔除与验证的性质无关的变量达到降低被验证模型大小的目的。进一步在异步系统的LTL限界模型检测中提出了限界stuttering等价的概念，并证明了在stuttering等价下LTL-X的可满足性保持不变。在不变性的支撑下对LTL限界模型检测中的命题公式编码机制进行了优化，避免重复搜索stuttering等价的路径，提高了模型检测的效率。　　2.随机系统关注的是某件事件发生的概率，研究人员在计算树和线性时态逻辑中引入概率度量算子，同时设计不同概率度量算子的检测方法，形成了随机系统模型检测技术。而概率算子的反例和证据，其结构特征是状态转换关系满足一定的概率分布，命题逻辑对概率分布缺乏表达力。因此概率算子的特性决定了将限界检测技术扩展到马尔科夫决策过程上，必会出现很多新的有价值的理论问题。本论文依照限界模型检测的思路，结合马尔科夫决策过程的特点，提出了一种新的限界模型检测技术。　　马尔科夫决策过程具有非确定性选择的刻画能力，这也是其最大的特性，针对该特性本论文首先定义了马尔科夫决策过程上概率计算树逻辑(PCTL)的限界语义，并证明其正确性;然后基于不同界下所计算概率度量序列的演化趋势，设计了限界检测过程终止的判断准则;最后将限界模型检测过程转换为线性方程组的求解问题。通过验证实验我们得知，在证据较短的情况下，限界模型检测技术所需的内存空间要少于无界模型检测算法所需空间，这为将限界模型检测技术应用于大规模随机系统的可靠性分析中奠定了基础。