Research On Model Checking Methods For Some Fuzzy Measures

As a formal verification technique,model checking is based on mathematical theory to ensure the correctness and reliability of the whole verified system in an automated way.However,the classical model checking theory has two restrictions in modelling and checking.Firstly,the classical model checking theory is based on the expansion of Boolean logics,it is unable to verify some systems with uncertain and fuzzy information.Secondly,the state spaces sizes become very large for many systems,some of these systems may even contain infinite number of states.When the number of states increases exponentially to a certain level,state space explosion will be an inevitable problem.To break through above two restrictions,the model checking theories under fuzzy measures such as multi-value model checking,fuzzy model checking,possibility model checking are emerged at the right moments and right fields.At current,these theories and technologies of model checking are still in infancy,and some problems have not been resolved fundamentally.Therefore,the main purpose of the dissertation is to resolve the model checking problems under several fuzzy measures.The problems mainly include modeling,abstraction,equivalence,minimization,computer algorithm generating.The main work of this paper is as follows:1.The multi-valued uncertainties of states properties and transitions make state space explosion more obvious.To solve this multi-valued state space explosion problem,multi-valued ion,multi-valued equivalence,multi-valued minimization are respectively presented.Firstly,as the multi-valued abstraction methods,the concepts of multi-valued simulation are presented.The concepts of multi-valued abstraction function and multi-valued abstraction Kripke structures are also presented based on multi-valued simulation.Reflexivity and Transitivity of multi-valued simulation are proven.The conditions that paths and traces suit for multi-valued simulation are given.Secondly,as the multi-valued equivalence methods,the concepts of multi-valued bisimulation are presented.Reflexivity,Symmetry and Transitivity of multi-valued bisimulation are proven.The conditions that paths and traces suit for multi-valued bisimulation are given.And multi-valued bisimulation is strictly finer than multi-valued simulation equivalence is verified by an example.Finally,as the multi-valued minimization methods,the structures of multi-valued quotient are presented.And the application of multi-valued quotient simplifies the multi-valued model is illustrated by an example of ambulance smart decision.To resolve mathematical multi-valued quotient cannot recognize by computer,particularly,the multi-valued quotienting algorithms are designed by a multi-valued counter and states partition method.And the whole process of the multi-valued quotienting algorithms are shown by a series of examples.These multi-valued quotienting algorithms are more generalized and wide range for use through comparison.2.Current abstraction,equivalence,minimization technologies are all limited in a specified model,these methods cannot share among different models.To resolve the generalized problems of abstraction,equivalence and minimization,firstly,a standard nondeterministic fuzzy Kripke structures(NFKSs)is given,then nondeterministic fuzzy abstraction,equivalence,minimization are respectively presented.As the nondeterministic fuzzy abstraction methods,the concepts of nondeterministic fuzzy simulation(NF simulation),coarsest nondeterministic fuzzy simulation(CNF simulation)are presented,the conditions of NF simulation for different models are listed.And the concepts of fuzzy abstraction function,coarsest fuzzy abstraction function,abstraction NFKSs and coarsest abstraction NFKSs are also presented.Reflexivity and Transitivity of NF simulation and CNF simulation are proven.The conditions that paths and traces with the same strategy suit for NF simulation or CNF simulation are given.As the nondeterministic fuzzy equivalence methods,the concepts of nondeterministic fuzzy bisimulation(NF bisimulation)are presented,the conditions of NF bisimulation for different models are listed.Reflexivity,Symmetry and Transitivity of NF bisimulation are proven.The conditions that paths and traces with the same strategy suit for NF bisimulation are given.As the nondeterministic fuzzy minimization methods,the structures of nondeterministic fuzzy quotient(NF quotient)are presented.According to an example of nondeterministic tentative drug therapies,minimization of nondeterministic fuzzy Kripke structures(NFKSs)and refinement of NFKSs strategies are illustrated.Finally,the improved NF quotienting algorithms are designed to reduce the time complexities as far as possible.And the whole process of the improved NF quotienting algorithms are shown by a series of examples.The research result shows that this improved NF quotienting algorithms are more generalized,the improved NF quotienting algorithms will suit for Kripke structures,multi-valued Kripke structures,fuzzy Kripke structures,NFKSs respectively.3.In some possibility systems,there are a lot of losses and rewards in the states transitions.The definitions of generalized possibilistic reward Kripke structures(GPRKSs)and cumulative reward are proposed to resolve this kind of systems modeling issue.According to the fact that the accumulative reward is only an algebraic sum rather than a disjunctive operation,the properties of the GPRKSs are not exactly same as the generalized possibilistic Kripke structure(GPKSs).On this basis,generalized possibility expected reward and the structure and semantic definitions of the generalized possibilistic reward computation tree(GPRCTL)are given.Then,generalized possibilistic reward simulation(GPR simulation),generalized possibilistic reward bisimulation(GPR bisimulation)and generalized possibilistic reward quotient(GPR quotient)are proposed to solve the problems of abstraction,equivalence,minimization of GPRKSs.An example of a cloud routing system of self-driving car is given to illustrate how generalized possibility processes real-time traffic information and how GPR quotient helps the system to optimize routing.Finally,the GPR quotienting algorithms are given.