  We present a translation from linear temporal logic with past to
deterministic Rabin automata. The translation is direct in the sense that it
does not rely on intermediate non-deterministic automata, and asymptotically
optimal, resulting in Rabin automata of doubly exponential size. It is based on
two main notions. One is that it is possible to encode the history contained in
the prefix of a word, as relevant for the formula under consideration, by
performing simple rewrites of the formula itself. As a consequence, a formula
involving past operators can (through such rewrites, which involve alternating
between weak and strong versions of past operators in the formula's syntax
tree) be correctly evaluated at an arbitrary point in the future without
requiring backtracking through the word. The other is that this allows us to
generalize to linear temporal logic with past the result that the language of a
pure-future formula can be decomposed into a Boolean combination of simpler
languages, for which deterministic automata with simple acceptance conditions
are easily constructed.
