Abstract: On the basis of introduction to LTL formula and theory of automata, we present a algorithm which can transfer LTL formulae into Buchi automata. In this algorithm, the LTL formula is simplified first, then transferred into an alternating Buchi automaton,be

Key words: Model checking,Buchi automata, Alternating buchi automata, Linear temporal logic