A Direct Translation from LTL with Past to Deterministic Rabin Automata

TL;DR

This paper introduces a direct, asymptotically optimal translation method from linear temporal logic with past to deterministic Rabin automata, avoiding intermediate non-deterministic automata and enabling efficient automaton construction.

Contribution

It presents a novel direct translation approach that encodes past information within the formula, simplifying the automaton construction process and improving efficiency.

Findings

Produces doubly exponential size Rabin automata

Enables evaluation of past operators without backtracking

Decomposes future formulas into simpler automata

Abstract

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.