Computation Tree Logic And Kripke Structure Decision Processes Based On Possibility Measure

Since H. Hansson proposed the theory of Probability Computation Tree Logic based on probability measure and finite Markov Chains in the1990s, C. Baier studied deeply and discussed the closure property about probabilistic bisimulation events and the events'reachability in Markov Decision Processes in detail. But there still exist many fuzzy uncertain events which include many fuzzy attributes in real life, such as the concept with ambiguity. It is necessary to extend the existing model checking methods to process the checking of the systems with fuzzy uncertaity. For this reason, we discuss the Computation Tree Logic based on possibility measure, bisimulation and possibilistic Kripke structure decision processes in this thesis.The contents of this thesis are summarized as follows:(1) The concept of possibilistic Kripke structure is proposed, the possibility measure based on possibilistic Kripke structure is constructed, the language structure definition and satisfaction relation about Possibility Computation Tree Logic(PoCTL) are defined, the equivalence relation among some PoCTL formulae and some CTL formulae are studied, and the event◇□a can be expressed by PoCTL is verified.(2) Some notions related to possibilistic bisimulation are presented, the bisimulation-equivalent states and paths are given, the quotient of possibilistic Kripke structure is defined, bisimulation-closed a-algebra is introduced. The result shows that the paths started from two bisimulation-equivalent states have the same transition possibility. The PoCTL and PoCTL formulae are given, whether two bisimulation-equivalent states fulfill the same PoCTL, PoCTL and PoCTL formulae are analyzed in detail.(3) The concepts of possibilistic Kripke structure decision processes and scheduler are proposed. We show that the possibilistic Kripke structure can be induced by the possibilistic Kripke structure decision processes. The language structure definition and satisfaction relation of quantitative PoCTL which based on possibilistic Kripke structure decision processes are given. If two PoCTL formulae interpreted over possibilistic Kripke structure decision processes are equivalent, then the above formulae interpreted over possibilistic Kripke structure are also equivalent. The reachability of the events on possibilistic Kripke structure decision processes is analyzed, and a value iteration algorithm is given.