Generalized Possibility Temporal Logic Model Detection Based On Decision-making Process

As computer hardware and software systems become more and more complex,how to ensure the correctness and performance reliability of such systems has become a prob-lem of wide concern.Model checking has attracted wide attention from both the aca-demic and industrial communities because of its solid mathematical basis and high level of automation.Traditional model checking method is qualitative,whose emphasis is on the absolute correctness of system satisfying the specifications.However,many practical systems are endowed with quantitative behavior characteristics and hence need to be ana-lyzed quantitatively as to what extent they meet the users' functional and nonfunctional requirements.In recent years,researchers begin to develop quantitative model-checking technique,which can not only quantify to what extent a system satisfies its specification,but also check the performance requirements and reliability of the systems,thus greatly extends the application range of model checking · Quantitative model checking can be further divided into probabilistic model checking and fuzzy model checking based on the validation of different objects.The probabilistic model checking is mainly used to verify probabilistic systems,while fuzzy model checking is used to check fuzzy systems with uncertain and inconsistent information.As the one of main forms of fuzzy model check-ing,the generalized possibilistic model checking,which considers the information of the possibility measure,can much fully check the properties of fuzzy systems.The aim of this dissertation is to deal with fuzzy systems.First,a formal mod-el called generalized possibilistic decision process(GPDP)is introduced to specify the behaviour of the systems.Then using the theories related to possibility measure and decision-making process,we generalize model checking for Computation Tree Logic(CTL),linear-time properties,Linear-time Temporal Logic(LTL),branching-time log-ic CTL*and bisimulation equivalence to the setting of GPDPs.The dissertation can be further divided into three parts.1.GPoCTL model-checking technique.We first propose GPDP to model the behav-iors of fuzzy systems,and define the notion of schedule so as to further define generalized possibility measures and the computational method needed.Then GPoCTL is introduced to describe the specifications of the systems,and its semantics over the GPDPs is giv-en.Finally,we present GPoCTL model-checking algorithm,which turns the GPoCTL model-checking problem into the problems of fuzzy matrix operations and fixed-point computation.2.Generalized possibilistic linear-time properties model-checking technique.First-ly,we generalize possibilistic LTL(GPoLTL)to specify linear-time properties of GPDPs,give its path semantics and language semantics,and show that the two semantics coincide.Then we present linear-time properties such as eventually reachability,always reachabil-ity,persistent reachability and repeated reachability,so the model-checking problems for these properties are turned into the operations of a fuzzy matrix or fixed-point computa-tion.Finally,we study the model-checking problems for generalized possibilistic regular safety properties and generalized possibilistic ?-regular properties.Their model checking problems are thus transformed into a model checking problem of generalized possibilistic linear-time properties with always reachability and repeated reachability,respectively.3.GPoCTL*model-checking technique and the maximal possibility bisimulation.We first introduce the syntax of generalized possibilistic CTL*(GPoCTL*)and GPoLTL Positive Normal Form(GPoLTL PNF),and define their semantics over GPDPs,and then present the GPoLTL PNF model-checking algorithm.After that,the method is giv-en about how to transforms every GPoCTL*model-checking problem into a GPoCTL model-checking problem or GPoLTL model-checking problem.Finally we provide relat-ed concepts of maximum possibility bisimulation,and give its logical characterization.