Mutual Simulation Tree Logic And Probability Measure Based On Probability

For its simplicity and highly automatopn, model checking has been applied to many fields, such as industrial design, especially hardware and software system, and has been an automatic technology which is based on simulation, testing, deductive, reasoning. As a kind of formal method and tool, model checking can check the ab-sence of errors and give a counterpart, therefore model checking can be considered as an intelligent and effective debugging technique. Many experts and scholars have made great contribution on this formal automatic validation technology not only in the classic model checking, but also in probabilistic model checking. Classical model checking technology requires that the system model and properties must be accurate and unambiguous. However, in the real world, whatever the description of information or the acquisition of information are often uncertain, this uncertainty includes probability uncertainty and fuzzy uncertainty. Baier and Katoen systemat-ically introduced the principle and method of model checking based on probability measure with finite Markov chain for the model of the probability system in2008, it made the model checking techniques having greatly development on theory and application. A new discipline is established after the concept of fuzzy sets proposed by Zadeh. One of the most important application fields of fuzzy sets is computation intelligence. Now the notion of fuzzy sets plays a very important role in every areas of computer science and engineering. We mainly study the theory of model checking based on possibility measure in this thesis.In the theory of classical model checking, if the number of states increase in terms of exponential form, then the phenomena of state explosion would happen. Bisimulation is one of the methods to restrain state explosion, and it can effectively simplify the number of states. In order to solve the problem of state explosion under the possibility measure, the study of bisimulation based on possibility measure is very important.Cost is always one of the important application of model checking in the auto-mated test. Baier and Katoen introduced the probability cost with finite Markov chain for the model of the probabilistic system, and especially for the probability cost on reachability properties. This thesis tries to set up costly computation tree logic based on possibility measure.The contents of this thesis are summarized as follows:(1) We mainly address some properties of possibility computation tree logic*(termed PoCTL*) and possibility computation tree logic-(termed PoCTL-) based on possibility Kripke structure.(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 o algebra is introduced. The results have shown that the paths starting from two bisimulation-equivalent states have the same transition possibility. We discuss that whether two bisimulation-equivalent states satisfy the same formulae of PoCTL, PoCTL*and PoCTL-(3) The concepts of probabilistic costly computation tree logic PoRCTL*are proposed. The reachability cost based on possibility measure is analyzed.