一种基于遗传算法的概率假设-保证验证方法与实现

作者：马艳; 曹子宁^*

来源：南京邮电大学学报(自然科学版), 2019, 39(06): 54-61.

DOI：10.14132/j.cnki.1673-5439.2019.06.009

• 随机模型检测
• 假设-保证推理
• 遗传算法
• 正则安全性

概率假设-保证推理(Probabilistic Assume-Guarantee Reasoning)是一种用于缓解随机模型检测中状态空间爆炸的方法,其将整个系统的验证分解为对较小组件的验证,组合较小组件的验证结果以达到对整个系统的验证。针对目前基于学习的概率假设-保证推理过程的缺陷:因学习假设过程中所有中间结果都需要存储而造成很高的空间复杂度,提出一种基于遗传算法(Genetic Algorithm,GA)学习假设的概率假设-保证推理方法,并将其用于组合验证MDP的正则安全性质。遗传算法本质上是一种随机算法,它的正确性通过满足训练集中的所有约束条件保证。该方法不需要记录中间结果,只需记录问题域和训练集的编码。因此,大大降低了产生假设的空间复杂度。实现了该概率假设-保证推理框架的原型工具,并通过领导人选举协议的实例对比了其有效性。

• 单位
  光电控制技术重点实验室; 南京航空航天大学; 工业和信息化部