模型检测是一种有效的自动化验证技术,已成功应用于安全和通讯协议、随机分布式算法、生物系统和电源管理等领域对系统进行分析与验证。作为一种形式化验证技术,模型检测能够对系统的状态空间进行穷举搜索并验证性质的正确性。当系统不满足逻辑公式所描述的性质时能够提供反例,从而帮助建模者进行修改模型或者再设计。模型检测也被广泛用作一项调试技术,帮助用户在模型不满足性质时分析错误原因。概率模型检测不仅可以对系统进行定性检测,而且还可以定量地检测一个具有随机行为的有限状态系统的正确性,因此被广泛应用,并取得了瞩目的成果。但对于不满足性质的系统,现有的概率模型检测器并没有提供反例。特别是检测复杂系统,例如信号转导网络或者基因调控网络(各种信号转导通路相互作用、相互识别,将信号从细胞外传递到细胞内;在细胞内负责不同功能的信号通路之间除了执行自身信号传递功能,还与其它通路存在相互制约或相互促进作用,在各信号通路间形成串扰,所以系统十分复杂),当系统不满足待验证的性质时,如果不能提供有用的调试信息,将会极大限制概率模型检测在复杂网络中的应用。目前,国内外的许多学者在经典模型检测和概率模型检测的应用领域进行了大量的研究,但在概率模型检测反例生成及分析方面尚未研究全面。本文研究了如何使用概率模型检测验证血小板衍生生长因子(PDGF)信号转导路径,对于不满足性质的系统给出反例;并且通过反例信息,分析导致系统不满足性质的原因。本文研究主要有以下几点:1.本文将概率模型检测技术应用到PDGF信号转导路径验证中,通过概率模型检测研究信号路径的动态性以及信号通路之间的串扰现象,并在PDGF信号转导路径中解释其生物现象。2.通过XBF算法给出PDGF信号转导路径不满足性质的反例路径,帮助建模者分析和调试系统错误。3.通过对反例的进一步分析找出导致PDGF信号转导路径不满足所描述性质的原因。