The underlying idea is to construct for a formula f an automaton A that accepts exactly the model of f. The algorithms that computes A closely resembles the one described in Improved Automata Generation for Linear Temporal Logic, where the propositional tableau rules are replaced by calls to the DLL procedure.

By resorting to DLL we hope to reduce the size of the computed automaton and to obtain speed ups on non-trivial specifications. Our decision procedures should be part of a system that performs on-the-fly model checking for LTL specifications.