A theoretic approach to translation of linear temporal logic into an automaton

Model checking is a fully automated inspection technology, which a system satisfies a group of required properties. Properties are used to define in linear time temporal logic (LTL), and are translated into automata in to be checked in explicit-state model checkers. In this paper, we give that an algorithm generates automata from LTL formula. We give a method consisting of three stages: the negative of the formula, a process of translation, and Simplified the resulting automaton. We put forward a process of translation that is optimal within a certain class of translation procedures. The simplification usually means can be used for automata. It reduces the number of transitions and states. This lends to more simples model checking of Linear-time temporal logic formula. Tests show that this algorithm is correct.