A Paradigm Study Of Generalized Likelihood Computing Tree Logic

Since Clark and Emerson introduced the notion of model checking in 1981,it has been widely concerned for the reason that model checking,as a kind of formal automatic verification technology,can solve the problems left over from the traditional testing method.The general steps of model checking include abstracting the appropriate model of the current system and describing the verified properties,then determining whether the system satisfies the properties or not by the means of model checking algorithms.In the classical theory of model checking,by the reason that the uncertainty problems can not be solved successfully,some scholars put forward kinds of quantitative extensions of the transition system,one of which is the generalized possibility computation tree logic based on generalized Kripke structure.The normal forms of temporal logic have important applications in model checking,however,normal forms of generalized possibility computation tree logic have not been researched systematically,so the main work of this paper is based on this background.The main contents of this paper are as follows:1.I give two kinds of normal forms of computation tree logic based on generalized possibility measures—Positive Normal Form and Existential Normal Form,here write PNF and ENF for short,and put forward the syntax and semantics of them.2.I prove that any formula of generalized possibility computation tree logic can be translated into a normal form in PNF and ENF by the method of inductive hypothesis.3.I present an algorithm which translates a formula of generalized possibility computation tree logic into a normal form in PNF or ENF,and explains by an example.