We present asymptotically optimal translations from linear temporal logic with past initially to limitdeterministic Büchi automata and then onwards to deterministic parity automata.In contrast to previously known translations involving past, the ones presented here are incremental: states and transitions can be constructed as needed on-the-fly, and they do not involve backtracking in order to correct for temporal inconsistencies.The past is naturally encoded in the formula by alternating between weak and strong versions of past operators.To handle the difficulties that arise from the alternation of least and greatest fix-point operators (such as between the "until" operator and its weak counterpart), we rewrite the given formula based on the infinitary behavior of a given word with respect to subformulae rooted with such operators.
No takes yet. Share an insight, caveat, or question.
Lidell et al. (2026) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: