David Lidell

Highlights Conference 2025 Conference Abstract

Translations from LTL with Past to Omega-Automata

• David Lidell

MFCS Conference 2024 Conference Paper

A Direct Translation from LTL with Past to Deterministic Rabin Automata

• Shaun Azzopardi
• David Lidell
• Nir Piterman

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.

Highlights Conference 2023 Conference Abstract

ppLTLTT: Temporal testing for pure-past linear temporal logic formulas

• David Lidell

We introduce ppLTLTT, a command-line tool for translating pure-past lineartemporal logic formulas into automata monitoring their truth values at everypoint in time. We show how ppLTLTT can be used to easily extend existing LTL-based tools, such as LTL-to-automata translators and reactive synthesis tools, to support a richer input language. Namely, with ppLTLTT, tools that acceptLTL input are also made to handle pure-past LTL as atomic formulae. Whilethe addition of past operators does not increase the expressive power of LTL, itopens up the possibility of writing more intuitive and succinct specifications. Weillustrate this intended use of ppLTLTT for Slugs, Strix and Spot’s commandline tool LTL2TGBA by describing three corresponding wrapper tools pSlugs, pStrix and pLTL2TGBA, that all leverage ppLTLTT. All three wrapper tools aredesigned to seamlessly fit this paradigm, by staying as close to the respectivesyntax of each underlying tool as possible. Contributed talk given by David Lidell Lunch Wednesday 14h00 - 15h24, Contributed Talks Automata and Transducers | HS 3 | chair: Sophie Pinchinat VASS, Skolem and Petri Net Problems | HS 4 | chair: Georg Zetzsche Automata and Transducers | HS 3 | chair: Sophie Pinchinat VASS, Skolem and Petri Net Problems | HS 4 | chair: Georg Zetzsche