LTL Model Checking Based On Possibility Measure

Model checking is a very important approach of automatic verification. It was put forward by Clarke, Emerson, Quielle and Sifakis in1981. Using model checking method, we can verify the proposition of the concurrent systems with the finite state mainly through the state search. Model checking method can execute automatically, and provide counterexample when the system can't fulfil the property. In many situations, we can verify infinite state system by the combination of model checking and other kinds of inductive principles.In classical model checking, Kripke structure is an important model and linear temporal logic is an important sequential logic tool in studying linear property. In2008, 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. On the other hand, since Zadeh proposed the theory of fuzzy sets in1965, many scholars have been devoting themselves to the research in this theory and its application. As a branch of the theory of fuzzy sets, possibility measure is a development of classical measure, which focuses on non-additive cases that is different from the probability measure. Most problems in real situations are complicated and non-additive; therefore, it is necessary to do some research work in the theory and application of model-check on non-deterministic systems of non-additive measure. And this paper attempts to initiate an LTL model-check based on possibility measure.This paper we discuss a common not-additive measure:probability measure and study the theory of model checking based on the possibility measure. Specifically, we mainly study model checking of linear property under the probability measure. This forms the main topic of this paper.1. We define possibilistic Kripke structure and analyse the Linear Temporal Logic (LTL) model checking in possibilistic Kripke structure using possibility measure. Then we compare the propety of possibility measure and probability measure.2. Firstly, we study the algebraic expressions and the calculation method of possibility measure which finite possibilistic Kripke structure satisfy reachability and repeated reachability linear-time properties and compare with probability measuret of the Markov chain model satisfy the two properties. Secondly, we introduce standard safety property and co-regular property in possibilistic Kripke structur and thoroughly study the verification of regular safety property and ω--regular property using finite automata. Then we get the conclusion:the verification of regular safety property and ω-regular property in finite possibilistic Kripke structure can be transformed into the verification of reachability property and repeated reachability property in the product possibilistic Kripke structure introduced in this paper and we give several examples to illustrate the methods presented. Finally, we summarise the basic contents of this paper and propose some problems about future research.