Optimal translations link past temporal logic to deterministic automata
New Translations From LTL with Past to LDBA and DPA
Formal Languages and Automata Theory
Summary
This paper tackles how to translate complex time-based logical statements that include past events into simpler machines that computers can run efficiently. The authors provide new methods that build these machines step-by-step as needed, avoiding backtracking or correcting mistakes later on. They handle tricky cases where logic alternates between conditions that must always hold and those that only need to hold sometimes, improving on older techniques. These improved translations can help computer systems analyze sequences of events more effectively.
What this means in practice
- •For software verification engineers: Construct automata on-the-fly to verify programs with temporal properties involving past events more efficiently.
- •For runtime monitoring developers: Implement incremental automata generation for real-time monitoring of systems where past event conditions affect current correctness.
Authors
David Lidell, Nir Piterman
Abstract
We present asymptotically optimal translations from linear temporal logic with past to limit-deterministic Buchi automata and 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.