Generalized Possibility Multi-value Temporal Logic Model Detection Based On Multi-value Decision Process

Model Checking is an important formal verification method,it is widely used for automated verification of hardware and software system.To verify concurrent systems with non-deterministic,incomplete and inconsistent information effectively,based on temporal logic and decision process(DP),this thesis studies the generalized possibilistic multi-valued temporal logic model checking algorithm with multi-valued decision process(MvDP),and its applications in non-deterministic system verifica-tion.Firstly,the system is modeled by the constructed MvDP.Secondly,the sys-tem properties are described by multi-valued temporal logic.Finally,the general-ized possibilistic model checking algorithms of multi-valued temporal logic based on multi-valued decision process is presented.In the algorithm,the scheduling of the decision process turns the model checking problems into the problems of polynomial-time fuzzy matrix operations or fuzzy matrix fixed-point calculations.The time complexity of the obtained multi-valued computation tree logic(MvCTL)model checking algorithm is O(size(M)·|?|),and both multi-valued linear temporal logic(MvLTL)and multi-valued branching temporal logic(MvCTL*)model checking algorithms have the time complexity of O(size(M)·exp(|?|)).The main contribu-tion of this thesis is as follows:1.We construct multi-valued decision process as a model of finite state system.First we give definitions of MvDP and its scheduling.Second,the formal represen-tations of state transitions,precursors and successors,and finite and infinite paths are discussed.Last we give matrix representations of initial distribution,transition distribution of MvDP and some related concepts.Further based on the MvDP mod-el,we give the definitions of the possibility measure over paths and the cylinder set,and discuss the matrix representation of the cylinder set.2.We give the syntax and semantic definition of multi-valued temporal logic.First we give the definitions of MvCTL,MvLTL,MvCTL*respectively.Second we discuss the semantic interpretation of the three temporal logics based on possibility measure and we give the inductive semantic definitions.Last the equivalence of MvLTL's linguistic semantics and path semantics based on possibility measure is discussed.3.Generalized possibilistic multi-valued temporal logic model checking algo-rithms based on MvDP is presented.First we give a description of model checking problems based on MvDP and a recursive definition of numbers of sub-formulas;Sec-ond we discuss the matrix calculation method for temporal connectives such as "?","(?)","(?)?n" and give the fixed point calculation method for connectives such as" ?"and "(?)";Then the generalized possibilistic MvCTL model checking algorithm(GPo-MvCTL algorithm)based on MvDP is given and its time complexity is discussed.Third we discuss the possibility measure of several special reachable events.And by defining the semantics and semantics of MvLTL PNF,generalized possibilis-tic MvLTL model checking algorithm(GPo-MvLTL algorithm)based on MvDP is given,and its time complexity is discussed.Last by combining GPo-MvLTL algo-rithm with GPo-MvCTL algorithm,we give generalized possibilistic MvCTL*model checking algorithm(GPo-MvCTL*algorithm)based on MvDP and discuss its time complexity.