The state-preserving model repair algorithm of Kripke structures

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 algorithm 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 construct 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.