The Model Repair Of Model Checking Fuzzy Computation Tree Logic

The correctness of software and hardware systems are more and more important in production and life of human.As an automatic verification technology,model checking aims to verify whether the systems can satisfy theirs desired properties,so as to guarantee the correctness of the systems.The model repair technology has promoted the application of model checking in practice.When the the model does not satisfy the desired properties,the model repair technology can automatically repair the model to satisfy the requirements.With the increasing complexity of software and hardware systems,the systems often contain amounts of uncertain or inconsistent information.In order to solve the verification problem of such systems,the fuzzy model checking technique is proposed based on fuzzy logic.In fuzzy model checking,the fuzzy Kripke structures is often used to model the system,and the desired properties of the system can be described by the fuzzy computation tree logic.Although great achievements have been made in fuzzy model checking,it is still to be studied how to repair the fuzzy computation tree logic formula of fuzzy Kripke structures.Based on the existing fuzzy model checking theory,this paper discusses the repair of fuzzy computation tree logic formula of fuzzy Kripke structures.Our main work is as follows:1.The model repair of fuzzy Kripke structures is discussed.First,on the basis of fuzzy Kripke structures,the semantic relationship of fuzzy computation tree logic formulas are discussed,which provides support for the research of the repair algorithm of fuzzy computation tree logic.Second,three primitive repair operations with fuzzy Kripke structures are defined.Then,we give the the definition of fuzzy Kripke structures distance by combining with the hamming distance definition method,and on this basis,the definition of fuzzy Kripke structures approximation is given.Finally,the concept of?-minimal repair model of fuzzy Kripke structures is proposed by introducing the threshold ?,which as a quantitative extension of the concept of minimal repair model in classical model repair theory.2.Based on the concept of ?-minimal repair model,firstly,the algorithm is proposed to solve the problem of propositional logic formulas of fuzzy computation tree logic formulas.Then,based on this,combining with the semantics of the fuzzy computation tree logic formulas,the algorithm is proposed to solve the problem of repairing the fuzzy computation tree logic formulas with the temporal operators X,G and U.Finally,theresearch results are applied to a case of robot exploring objects to illustrate the practical applicability of the algorithm for repairing fuzzy computation tree logic formulas.