Properties Of Temporal Logic Based Measure Possibility

It is inevitable to appear the uncertainty and inconsistent issues in the process of the lager and complex systematic verification, so not all the verification problem in the concurrent system can be dealt by the classical model checking. To handle with the systematic verification which has something to do with uncertainties in probability, Baier and Katoen systematically introduced the principle and method of model checking based on probability measure and related applications with Markov chain model for probability system, Sharir talked over the logic of timing sequence in probability propositions and applied probability theory to model checking in which the uncertainty is modeled by probability measure. Many complicated problems in real situation are non-additive, and Markov chain models which focus on additive cases can not deal with all the systematic verification. It is necessary to do some research work in the theory and application of model checking on non-deterministic systems of non-additive measure. The model checking of Linear-Temporal Logic(LTL) and Computation Tree Logic(CTL) which are non-additive cases have some important results based on possibility measure. However, there are many important and critical issues that have not been studied, i.e, whether possibility instaneous measure exists in possibility measure or not, what is the relationship between the possibility measure and possibility instaneous measure, and what is the relationship of CTL formulae and PoCTL formulae. This paper attempts to resolve the above problems.The contents of this thesis are summarized as follows:(1) We give the definition of the transient possibility measure of a possibilistic Kripke structure, and show that the reachability possibility measure is equivalent to the reachability transient possibility measure with a structured approach under the condition of the unconstrained step-bounded and the constrained, respectively. Then, we investigate the conditions of the operation of union and intersection which hold under possibility measure, several properties of LTL are studied in detail. Especially, some properties of possibilities measure of repeated reachability event and persistence event are researched under the strong connected subset.(2) We further study the CTL model checking in possibilistic finite Kripke structure using possibility measure. We provide the definition of the equivalence of PoCTL formulae and CTL formulae, and the notion of the equivalence of PoCTL formulae and PoCTL formulae. We prove that the supplement operation of the formule PoJ(φ) holds in possibility measure for the PoCTL formulae is equivalent to the CTL formulae. Qualitative properties of PoCTL whose possibility is more than0or equal to0are thoroughly studied. We study the equivalence and difference between PoCTL and CTL in detail, especially, we show that any CTL formula can be expressed by a PoCTL formula, and CTL is strictly contained in PoCTL. Qualitative properties of repeated reachability and persistence are studied in more detail, in a similar way, quantitative properties of repeated reachability and persistence are also analyzed in this paper. At the same time, we give several examples to illustrate the difference of CTL between probability meaure and possibility meaure. Finally, the steps and complexity of model checking which baseed on possibility measure are given, which illustrate the feasibility of model checking.