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自动机。方法基于两个核心概念：其一，通过对待转换公式本身执行简单重写，即可编码词前缀中包含的、与当前公式相关的历史信息。基于此，涉及过去时态算子的公式（通过此类重写——交替使用公式语法树中过去时态算子的弱化与强化版本）可在未来任意时间点被正确求值，而无需回溯整个词序列。其二，这一机制使得纯未来时态公式语言可分解为更简单语言的布尔组合这一结论得以推广至带过去时态的线性时序逻辑，而针对这些简单语言可轻松构造具有简单接受条件的确定性自动机。