This talk addresses the following problem:  given a finite set of observations of system behavior, each observation itself being a finite sequence of system states, and a query consisting of a Finite LTL formula with missing subformulas, compute missing the missing subformulas that make the LTL formula true for all observations.  This so-called query-checking problem has many applications in the analysis of time-series data, including server logs and financial trend data, as well as generally in system comprehension and system-specification mining.  The presentation will begin by introducing Finite LTL, which is the well-known Linear-Time Temporal Logic of Pnueli interpreted over finite, rather than infinite, state sequences.  It will then show how automata may be constructed from such formulas that recognize exactly the sequences making the formula true, and how these automata may be adapted to Finite LTL queries in which subformulas are missing.  A procedure is then described that uses the automaton representation of such a query to solve for the missing subformulas for a given a set of finite state sequences.  Preliminary experimental results of a prototype implementation are also given.