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

摘要

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

关键词

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

基金资助

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