Font Size: a A A

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

Posted on:2013-01-15Degree:MasterType:Thesis
Country:ChinaCandidate:Y XueFull Text:PDF
GTID:2218330374461937Subject:Computer software and theory
Abstract/Summary:PDF Full Text Request
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.
Keywords/Search Tags:possibilistic Kripke structure, possibility measure, possibilitycomputation tree logic, possibilistic bisimulation, possibilistic Kripke structuredecision processes
PDF Full Text Request
Related items
 1 Properties Of Temporal Logic Based Measure Possibility 2 Mutual Simulation Tree Logic And Probability Measure Based On Probability 3 LTL Model Checking Based On Possibility Measure 4 Mutual Analog And CTL Fixed Point Semantics Based On Generalized Probability Measure 5 Research On The Logical Expression Ability Of Generalized Likelihood Computing Trees 6 Research On Model Detection Theory Based On Automata And Possibility Kripke Structure 7 Parallelization Of LTL Model Detection Based On Likelihood Measure 8 Possibilistic Planning Using Possibilistic Decision Diagrams 9 Research On Presentation And Solution Of Possibilistic Planning Problems 10 Research And Implementation Of Possibilistic Concurrent Planning