  This paper describes a method for converting formulas in finite propositional
linear-time temporal logic (Finite LTL) into finite-state automata whose
languages are the models of the given formula. Finite LTL differs from
traditional LTL in that formulas are interpreted with respect to finite, rather
than infinite, sequences of states; this fact means that traditional
finite-state automata, rather than {\omega}-automata such as those developed by
B\"uchi and others, suffice for recognizing models of such formulas. The
approach considered is based on well-known tableau-construction techniques
developed for LTL, which we adapt here for the setting of Finite LTL. The
resulting automata may be used as a basis for model checking, satisfiability
testing, and model synthesis.
