模型检测是一种形式化自动验证技术,通过对系统状态空间进行穷举搜索,以验证用时序逻辑公式描述的系统性质在该模型上是否可以满足。模型检测可以自动执行,并能在系统不满足性质时提供反例路径,因此被广泛地应用于计算机硬件、通信协议、控制系统、安全认证协议等方面的分析与验证中,取得了令人瞩目的成果。然而随着信息技术的发展,不断涌现的系统变得越来越复杂,模型检测技术的瓶颈,即状态爆炸问题,已经严重制约了模型检测的应用;且越来越多的系统包含有不确定信息,这也是经典模型检测技术无法处理的。李永明的科研团队将可能性测度与模型检测技术结合起来,提出了基于可能性测度的模型检测方法,有效地解决了模型检测中处理不确定信息的问题。本文研究基于可能性测度的LTL模型验证的并行化问题,旨在提供一种可行的方法,以解决可能性测度下LTL模型验证面临的状态爆炸问题。论文的主要工作如下:1.提出了一个新的动态系统状态空间划分方法。选一个并发分量并依据状态之间的关系完成系统状态的分割,使关系紧密的状态尽可能地分布于同一个计算结点上;然后调整划分结果使得计算负载平衡;最后将划分结果与其它并发分量状态叉乘以完成系统状态空间划分。从理论和实验两方面证明了该方法能够保证分布式模型检测系统负载平衡,为提高分布式验证算法执行效率提供了良好基础。2.给出了定量模型检测并行化验证算法。系统模型转化为可能的Kripke结构,性质用非确定性有限自动机表示,在两者的乘积上利用扩展的基于嵌套DFS的LTL分布式验证算法,完成了系统的定性验证和定量验证。本文的贡献在于,为解决可能性测度下LTL模型检测的状态爆炸问题提供了一种可行的方法。