可能性测度下的LTL模型检测并行化研究

摘要：

分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决.对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法.首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证.

关键词：可能的Kripke结构、状态空间划分、定量分布式模型检测

所属期刊栏目：45

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金11271237,11301321;中央高校基本科研业务费专项资金GK201603086

在线出版日期：2018-06-07（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：71-75,88