Quantitative Model Testing Based On Generalized Possibility Temporal Logic

The traditional model checking is an automatic technology widely used in correct-ness and performance reliability verification of the system,and it is a qualitative ver-ification method,which focus on the absolute guarantee of correctness about system specifications.With the system becoming more and more intricate,some uncertain in-formation caused by the system needs to be researched for verifying the system proper-ties.Correspondingly,only considering whether the model satisfies the specifications is not sufficient,we should analyse how well the model satisfies the specifications.It has been developed a quantitative model-checking technique,which can cope with the un-certain information of the system quantitatively and effectively.Especially,as the one of main forms of quantitative model checking,the generalized possibilistic model checking,which introduces the possibility measure into the classical temporal logic,can deal with the fuzzy uncertainty information not satisfying the additive of measure.And then,the possibility measure not only makes the temporal properties measurable,but also makes us capture the partial ignorance information of the system completely.The research of possibilistic model checking is still in its developing stage,and a lot of work needs to study.In the dissertation,we will study the generalized possibilis-tic model checking via classical model checking firstly,then the generalized possibilistic temporal proeperties are inspected with the help of the proven technique of the classical model checking.Secondly,we would discuss the generalized possibilistic model check-ing with fairness constraint for rejecting the unreasonable properties in the generalized possibilistic temporal logic.Because the generalized possibilistic temporal logic only makes the Boolean connectives and propositions fuzzy,and its formulas can't describe properties with fuzzy time,we shall introduce fuzzy temporal connectives to express properties with fuzzy time,and study the generalized possibilistic temporal logic with fuzzy time.The main contributions in the dissertation consist of the following four parts:1.We present the model checking algorithm of the generalized possibilistic comput-ing tree logic(GPoCTL).After giving the cuts of different levels in accordance with the state formulas of GPoCTL,we check if the state belongs to the level cuts using the clas-sical CTL model checking algorithm,then compute the possibility(or necessity)degree of state satisfying the formulas by fuzzy decomposition theorem,and its computing com-plexity is reduced relative to directly calculating the possibility state satisfying GPoCTL formulas by means of the fuzzy matrix.Furthermore,the semantics of GPoCTL formu-las with fairness constraint are given,and the complexity of GPoCTL model checking algorithm with fairness constraint is presented.2.We present the model checking algorithm of the generalized possibilistic linear temporal logic(GPoLTL)via LTL model checking algorithm.The LTL model checking algorithm is used to verify whether the Kripke structures of different levels according to the generalized possibilistic Kripke structure(GPKS)satisfies the LTL formulas,subse-quently,we can verify whether the GPKS satisfies the GPoLTL formulas or the GPKS has the expected properties.The conclusion is given that the complexity of GPoLTL model checking algorithm is linearly related to which of the LTL model checking algorithm.An algorithm based on deterministic fuzzy finite(Buchi)automata is provided for veri-fying fuzzy regular safety properties(fuzzy ?-regular properties).It is proved that the realizable fairness constraint has no effect on verifying the fuzzy safety properties,fur-therly,we regard the fairness constraint of the GPKS path as the LTL formula,then turn the GPoLTL formulas with fairness constraint into the general GPoLTL formulas when verifying the properties.3.We introduce the fuzzy temporal connectives into GPoLTL which can express fuzzy time,define the syntax and semantics of GPoLTL with fuzzy time(GPoFLTL).Especially,the semantics interpretation based on path and language turns out to be equiv-alent.We prove that GPoFLTL has stronger expressiveness than GPoLTL.The model checking problems of several kinds of linear temporal properties with fuzzy time are computed by means of fuzzy matrix.We present the algorithm of the GPoFLTL nec-essary threshold model checking,which can be calculated by the LTL model checking technique based on nondeterministic Buchi automata theory,accordingly,its complexity is provided.4.The fuzzy temporal connectives are introduced into GPoCTL,then the syntax and semantics of GPoCTL with fuzzy time(GPoFCTL)are defined.We show that not only GPoFCTL formulas can express the temporal properties with fuzzy time,but also GPoFCTL has stronger expressiveness than GPoCTL through an example.Whereafter,we study the model checking problems of some GPoFCTL state formulas by means of fuzzy matrix,such as formulas with "soon","lasts for t consecutive time instants at most",etc,which can express fuzzy time,then present the GPoFCTL model checking algorithm and its computing complexity.