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.

翻译：本文提出了一种从带过去时态的线性时序逻辑到确定性Rabin自动机的转换方法。该转换具有直接性，即不依赖于中间的非确定性自动机，且具有渐近最优性，可生成双指数规模的Rabin自动机。该方法基于两个核心概念：其一，通过对公式本身进行简单重写，可以将词语前缀中包含的历史信息（与所考虑公式相关的部分）进行编码。因此，涉及过去时态算子的公式（通过此类重写——即在公式语法树中交替使用过去时态算子的弱版本与强版本）能够在未来任意时间点被正确求值，而无需对词语进行回溯。其二，这使得我们可以将纯未来公式的语言可分解为简单语言的布尔组合这一结论推广至带过去时态的线性时序逻辑，而对于这些简单语言，具有简单接受条件的确定性自动机可以轻松构建。