Research On The Logical Expression Ability Of Generalized Likelihood Computing Trees

In order to solve the validity problem of complex computer systems to ensure the correctness and reliability of such systems,model checking was proposed by Clark and Emerson in 1981.Model checking is a kind of formalized automatic verification technology,and can run through the whole process of system develop-ment.It is mainly divided into the following three processes:Firstly,abstracting the mathematical model of a given system;secondly,describing formally the veri-fied properties;finally,verifying whether the system satisfies the properties by using model checking algorithms,if it satisfies the properties and returns true;otherwise it provides us with a counterexample.Classical model checking focuses on the completely deterministic systems,which rarely exists in reality.Therefore,people began to embed quantitative information into the state-transition models,such as probability,multi-value,time and possibil-ity,etc.In order to solve the validity problem of fuzzy systems,Li Yongming com-bined possibility measures with model checking and proposed the theory of model checking based on possibility measures.Furthermore,Li Yongming extended pos-sibility measures to generalized possibility measures,and proposed the theory of model checking based on generalized possibility measures.Studying the expressive-ness of logic formulas plays an important role in model checking with uncertainty,there is a need to study the expressiveness of generalized possibilistic computation tree logic.Based on the previous work,this thesis discusses the relationship of gen-eralized possibilistic computation tree logic and computation tree logic with respect to their expressiveness in a finite generalized possibilistic Kripke structure,and the relationship of generalized possibilistic computation tree logic and possibilistic com-putation tree logic with respect to their expressiveness in a finite strong generalized possibilistic Kripke structure.The main content of this paper is arranged as follows:1.We define the syntax and semantics of interval generalized possibilistic com-putation tree logic.2.We introduce the definition of equivalence relation between interval gener-alized possibilistic computation tree logic formulas and computation tree logic for-mulas based on a finite generalized possibilistic Kripke structure,and prove that computation tree logic is a proper subclass of interval generalized possibilistic com-putation tree logic by induction and contradiction.Then,the algorithm is proposed to translate computation tree logic formulas into interval generalized possibilistic computation tree logic formulas.3.We give the notion of strong generalized possibilistic Kripke structure and define the equivalence relation between interval generalized possibilistic computa-tion tree logic formulas and possibilistic computation tree logic formulas based on a finite strong generalized possibilistic Kripke structure,and prove that possibilis-tic computation tree logic is a proper subclass of interval generalized possibilistic computation tree logic by induction and contradiction.Then,the algorithm is introduced to translate possibilistic computation tree logic formulas into interval generalized possibilistic computation tree logic formulas.4.We extend the previous definition of equivalence relation and give another definition of equivalence of formulas.