An Automaton Method For Generalized Possible Linear Sequential Logic

Model checking verifies the systems with finite states and it can execute au-tomatically. The model of model checking is the transition system, and the the classical model checking system is qualitative. With the development of computer hardware and software, there will be a lot of uncertain information in the transition system. In order to solve the problems caused by the uncertain information, the researchers have extended the states transition system. For example, adding time factor in the states,or joining probability or statistics in transition system. In 1965, Zadeh proposed the fuzzy set theory, and then the fuzzy possibility measures has been widely studied. Recently,Li Yongming proposed the generalized possibility measures of model checking.This paper is a cross subject about generalized possibility model checking and automata theory and basis, and one of the important methods of linear temporal log-ic of model checking is to transform the linear temporal logic formulae into Buchi automata,and then giving the model checking algorithm by automata. Although the generalized possibility measures of model checking has been studied,but how to transform the generalized linear temporal logic formulae into Buchi automata has not been studied. In this paper work will be carried out in this area, a method about the generalized linear temporal logic formulae turn to fuzzy alternating Biichi au-tomata and fuzzy Buchi automata is given.Meanwhile, generalized possibility linear temporal logic of model checking and the algorithm and complexity is analyzed.The main work is as follows:1 Firstly, we give the linear temporal logic syntaxes and semantics, generalized possibilistic Kripke structure and some related properties.2 secondly, we introduce the alternating Buchi automata, non-deterministic Buchi automata, fuzzy alternating Biichi automata and fuzzy Buchi automata.3 At the end of the paper,we give a method for converting generalized possibilis-tic linear temporal logic formulae to fuzzy alternating Buchi automata and fuzzy B uchi automata.Under the generalized possibility measures,we give a method about generalized linear temporal logic of model checking, and then give the complexity analysis and algorithm.