基于Kripke的状态保留模型修复算法

戴敏, 潘海玉

桂林电子科技大学学报 ›› 2024, Vol. 44 ›› Issue (06) : 599-605. DOI: 10.16725/j.1673-808X.2022341

基于Kripke的状态保留模型修复算法

  • 戴敏, 潘海玉
作者信息 +
History +

摘要

针对模型验证中受到广泛关注的模型修复问题,在极小模型修复的基础上保留原模型中尽可能多的可达状态,并给出了具有多项式时间复杂度的修复算法。模型经过检验后,若被判定存在违反给定性质的行为,则可以借助经典模型检验的不动点思想,找出模型中的验证失败路径,从而进行修复。此外,由于全局模型修复已被证明是NP问题,将修复算法的范围约束在CTL的一个子集内进行讨论。根据极小修复思想,选取对原模型中状态影响最小的修复操作,同时在经典模型检测的基础上,结合不动点思想以及图算法的部分性质,构造出相应逻辑公式的修复算法,使状态保留的修复算法时间复杂度得以降低到多项式时间。

关键词

模型检验 / 模型修复 / 可达状态 / 计算树逻辑 / Kripke结构

中图分类号

TP301

引用本文

导出引用
戴敏, 潘海玉. 基于Kripke的状态保留模型修复算法. 桂林电子科技大学学报. 2024, 44(06): 599-605 https://doi.org/10.16725/j.1673-808X.2022341

基金

国家自然科学基金(62162014); 广西自然科学基金(2018GXNSFAA281326); 广西可信软件重点实验室基金(KX201911)

评论

Accesses

Citation

Detail

段落导航
相关文章

/