Research On Formal Methods Of Fuzzy System Verification

Formal verification is a particular kind of mathematical-based techniques to ensure the correctness and performance reliablity of computer software and hard systems.Tradi-tional formal verification is based on two-valued logic.However,it is unable to verify the systems enriched with quantitative information.Hence,quantitative formal verification comes its being,and provides a method for verifying the systems with quantitative in-formation.Meanwhile,quantitative formal verification has attracted wide attention from both the academic and industrial communities.Formal verification of fuzzy systems is a fundamental direction of quantitative formal verification.Now,the research of formal verification of fuzzy systems is still in the primary stage,the model-checking approach and synthesis technique of fuzzy systems have not been fully developed yet.The main reason is that the variety of fuzzy logic and complex of fuzzy systems make it very diffi-cult to give an effective formal verification method.To solve the verification problems of fuzzy systems,the focus of this dissertation is to study the model-checking problem of fuzzy systems,the synthesis problem of fuzzy linear temporal logic and the reachability problem of fuzzy open systems.The main contributions are as follows:(1)The model-checking method of computation tree logic over fuzzy systems is proposed.Nondeterministic fuzzy Kripke structures(NFKSs)are introduced,which can be used as a general formalism for fuzzy systems.Then the syntax and semantics of fuzzy computation tree logic are proposed to specify branching temporal properties of NFKSs.Finally,the model-checking algorithm of fuzzy computation tree logic over NFKSs with polynomial-logarithmic running time is given.(2)The model-checking problem for fuzzy computation tree logic with fairness over NFKSs is studied.The fair semantics of fuzzy computation tree logic over NFKSs is given,which ensures that model checking of fuzzy computation tree logic is based on the fair paths of NFKSs.The model-checking method of fuzzy computation tree logic based on fair semantics over NFKSs is provided.(3)The syntax and semantics of fuzzy linear temporal logic are given,in order to solve the synthesis problem of fuzzy linear temporal logic.Fuzzy game graphs are intro-duced,and the construction methods of winning strategies for both players in fuzzy game graphs are proposed.Furthermore,the method is provided about how to transform the synthesis problem of fuzzy linear temporal logic into constructing the optimal winning strategy in fuzzy game graphs.(4)The reachability problem of fuzzy open systems is solved.Lattice-valued reach-ability game graphs(LRGs)are introduced to study the reachability objective of fuzzy open systems.The methods for computing the truth values that players win at each state of LRGs are given,it is proved that both players have the same winning truth values at all states of LRGs.Finally,the reachability problem of fuzzy open systems is thus reduced to the problem of computing the winning truth values of every state of LRGs.