Research On Several Problems Of Lattice-valued Alternating Automata

Theory of computation is one of the basic contents of theoretical computer science,which includes automata theory,formal languages,computational complexity,etc.Non-determinism has different important roles in the theory of computation.In formal lan-guage theory,certain languages can be described by some nondeterministic automata;in complexity theory,nondeterminism is the base of NP-class of decision problems.In automata theory,even though nondeterministic automata and deterministic au-tomata have the same expressive power,nondeterministic automata have simpler struc-tures than deterministic ones.From the point of view of logic,there are only existential quantifiers in the transitions of nondeterministic automata.Alternating automata,a gen-eralized model of finite nondeterministic automata,have both existential quantifiers and universal quantifiers.Since alternating automata and nondeterministic automata are e-quivalent and it is easy to complement alternating automata,then the alternating automa-ta model is important in formal verification.In order to enhance the processing ability of alternating automata,we discuss fuzzy alternating automata over distributive lattices.Especially,we discuss the expressive power and algebraic properties of lattice-valued fuzzy alternating automata.In addition,we study some decision problems for lattice-valued fuzzy alternating Buchi automata and provide an automata-theoretic approach to lattice-valued computation tree logic model checking.The main contributions of this thesis are shown as below:1.In Chapter 3,we introduce notions of fuzzy positive Boolean formulas and fuzzy alternating automata over distributive lattices.We prove that lattice-valued fuzzy alter-nating automata and lattice-valued fuzzy nondeterministic automata have the same ex-pressive power.There is an exponential blow-up in the number of states arising from the transformation from a lattice-valued fuzzy alternating automaton into its equivalent lattice-valued fuzzy nondeterministic automaton,and we can illustrate that such expo-nential blow-up is unavoidable.Besides,we discuss closure properties of lattice-valued fuzzy alternating automata.2.In Chapter 4,we propose the notion of lattice-valued fuzzy alternating Biichi automata and study their closure properties and expressive power.Without the aid of equivalence relationship between lattice-valued fuzzy alternating Buchi automata and lattice-valued fuzzy nondeterministic Buchi automata,we use the game theory and the?-regularity of languages accepted by lattice-valued fuzzy alternating co-Buchi automa-ta to directly show the closure under complementation of languages accepted by lattice-valued fuzzy alternating Biichi automata.At last,we discuss some decision problems for lattice-valued fuzzy alternating Buchi automata.3.In Chapter 5,we give the definition of lattice-valued fuzzy alternating tree au-tomata.By comparing the expressive power of lattice-valued fuzzy alternating tree au-tomata and lattice-valued fuzzy tree automata,we show that they are equivalent and we give algorithms for transformation between them.The description of the time complexity of algorithms is also included.Moreover,we study the closure under complementation of lattice-valued fuzzy alternating tree automata based on the notion of lattice-valued computation trees.4.In Chapter 6,we introduce the definition of lattice-valued fuzzy alternating Buchi tree automata.We compare the expressive power of lattice-valued fuzzy alternating Buchi tree automata and lattice-valued fuzzy Buchi tree automata,and we give algorithms for transformation between them in two special cases.We establish a translation between lattice-valued computation tree logic formulas and lattice-valued fuzzy alternating Buchi tree automata,and provide an automata-theoretic approach to determining if a lattice-valued Kripke structure satisfies a lattice-valued computation tree logic formula or not.