桂林电子科技大学学报2024，Vol.44Issue(6)：599-605,7.DOI:10.16725/j.1673-808X.2022341
基于Kripke的状态保留模型修复算法
The state-preserving model repair algorithm of Kripke structures
摘要
Abstract
In order to solve the problem of model repair which has been widely concerned in model checking,this paper proposes to preserve as many reachable states as possible in the original model on the basis of minimal model repair,and gives a repair algo-rithm with polynomial time complexity.If the model is checked to violate the given property,we can find out the failure paths in the model by the fixed point idea of classical model checking and then repair them.In addition,since global model repair is proven to be NP-hard,the scope constraint of the repair algorithm is discussed in a subset of CTL.According to the idea of minimal model repair,we consider two kinds of repair operations which have the least influence on the states in the original model.At the same time,based on the classical model checking,the fixed point idea and some properties of the graph algorithm are combined to con-struct the State-Preserving model repair algorithm of the corresponding logical formulas,the time complexity of state-preserving model repair algorithm is reduced to polynomial time.关键词
模型检验/模型修复/可达状态/计算树逻辑/Kripke结构Key words
model checking/model repair/reachable states/computation tree logic/Kripke structure分类
信息技术与安全科学引用本文复制引用
戴敏,潘海玉..基于Kripke的状态保留模型修复算法[J].桂林电子科技大学学报,2024,44(6):599-605,7.基金项目
国家自然科学基金(62162014) （62162014）
广西自然科学基金(2018GXNSFAA281326) （2018GXNSFAA281326）
广西可信软件重点实验室基金(KX201911) （KX201911）
