模型检测是一种自动化程度非常高的有限状态系统验证技术，目前已经在计算机硬件、通信与安全协议、软件可靠性的验证方面获得了较大的成功。传统模型检测技术关注的是系统行为的绝对正确性，如系统不能进入死锁状态。然而分布式算法，多媒体协议，容错系统等往往关心某种量化属性，如消息传送失败的概率不高于1％，在时间t内至多m个消息丢失的概率不高于0.8％，请求发送后在5到7个时间单元内得到响应的概率不低于70％等等。随机模型检测致力于解决这类属性的自动化验证问题。　　 在随机模型检测中一般使用概率计算树逻辑PCTL和连续随机逻辑CSL刻画属性，使用马尔科夫过程，概率时间自动机等建立系统模型。与传统模型检测一样，状态空间爆炸问题也是随机模型检测技术实用化的主要瓶颈。在为缓解状态空间爆炸问题已经提出的诸多理论和方法中，限界模型检测技术是克服状态空间爆炸问题的最为有效的方法之一。本文主要工作是提出了概率奖励计算树逻辑和概率实时认知逻辑的限界模型检测技术，具体包括以下两个方面:　　 1.概率奖励计算树逻辑以离散时间马尔可夫链作为系统模型，为缓解该模型上的状态空间爆炸问题，提出了概率奖励计算树逻辑的限界检测技术。首先定义概率奖励计算树逻辑的限界语义，并证明其正确性;其次提出基于线性方程组求解的限界模型检测算法;然后通过实例说明了限界模型检测的过程。最后在概率奖励计算树逻辑的基础上提出了重复可达性和持续性的限界语义和限界模型检测算法，并以实例来说明限界模型检测的过程。实验结果表明在属性成立的证据较短的情况下，限界模型检测能够快速的完成验证。　　 2.为了形式化描述多智体系统中与概率、实时、知识相关的性质，提出了一种概率实时认知逻辑PTCTLK。模型检测是验证多智体系统是否满足PTCTLK公式的主要技术，状态空间爆炸是该技术实用化的主要瓶颈。为此提出一种PTCTLK的限界模型检测算法。首先，将PTCTLK的模型检测问题转换为无实时算子的PBTLK的模型检测问题;其次，定义PBTLK的限界语义，并证明其正确性;然后，设计基于线性方程组求解的限界模型检测算法;最后，依据概率度量序列的演化规律和数值计算中牛顿迭代法使用的迭代过程终止判断准则，设计了一系列的限界检测终止性判别准则，并分析了各种准则适用的场景。此外还针对线性方程组的特点，给出了变元求解的次序，从而避免不必要的迭代运算。实例研究表明，与无界模型检测相比，在属性为真的证据较短的情况下，限界模型检测完成验证所需空间更少。