基于切片技术的复杂模型验证方法

• 作者: 么一诺 于明霞 毕曦文 纪明宇
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 复杂概率系统 模型检测 概率矩阵 状态约减 反例路径
• 年，卷（期）: 2020,（9）
• 所属期刊栏目: 算法
• 页码范围: 188-193
• 页数: 6页
• 分类号: TP301.2
• 字数: 4229字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2020.09.031

摘要

针对模型检测中的状态空间爆炸问题,提出一种基于带资源消耗的复杂概率迁移系统模型的性质验证方法.使用PRCTL进行模型语义逻辑表示,对迁移步数约束采用基于栈的深度遍历算法完成检验,针对冗余的迁移和状态实施二次约减,完成复杂的概率迁移系统的模型简化;针对简化后的迁移图进行概率矩阵迭代运算以判定概率条件,同时完成资源条件的判定,并进行相应的实例分析.该模型验证方法能够在一定程度上缓解复杂系统带来的状态冗余和计算繁琐问题,为性质验证工作提供了新的思路.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	纪明宇	东北林业大学信息与计算机工程学院	11	15	3.0	3.0
2	于明霞	东北林业大学信息与计算机工程学院	1	0	0.0	0.0
3	么一诺	东北林业大学信息与计算机工程学院	1	0	0.0	0.0
4	毕曦文	东北林业大学信息与计算机工程学院	2	0	0.0	0.0