# First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation

arXiv: https://arxiv.org/abs/1901.06108 · HTML: https://mlsanity.com/paper/1901.06108/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Jan 2019.

## Built on by (most cited first, 5 of 5)

- [Planning for Temporally Extended Goals in Pure-Past Linear Temporal Logic: A Polynomial Reduction to Standard Planning](https://mlsanity.com/paper/2204.09960/) (2022)
- [Automata for dynamic answer set solving: Preliminary report](https://mlsanity.com/paper/2109.01782/) (2021)
- [Automata Techniques for Temporal Answer Set Programming](https://mlsanity.com/paper/2109.08279/) (2021)
- [LTLf Synthesis Under Unreliable Input](https://mlsanity.com/paper/2412.14728/) (2024)
- [Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version)](https://mlsanity.com/paper/2602.06227/) (2026)

## Abstract (arXiv)

Translating formulas of Linear Temporal Logic (LTL) over finite traces, or LTLf, to symbolic Deterministic Finite Automata (DFA) plays an important role not only in LTLf synthesis, but also in synthesis for Safety LTL formulas. The translation is enabled by using MONA, a powerful tool for symbolic, BDD-based, DFA construction from logic specifications. Recent works used a first-order encoding of LTLf formulas to translate LTLf to First Order Logic (FOL), which is then fed to MONA to get the symbolic DFA. This encoding was shown to perform well, but other encodings have not been studied. Specifically, the natural question of whether second-order encoding, which has significantly simpler quantificational structure, can outperform first-order encoding remained open. In this paper we address this challenge and study second-order encodings for LTLf formulas. We first introduce a specific MSO encoding that captures the semantics of LTLf in a natural way and prove its correctness. We then explore is a Compact MSO encoding, which benefits from automata-theoretic minimization, thus suggesting a possible practical advantage. To that end, we propose a formalization of symbolic DFA in second-order logic, thus developing a novel connection between BDDs and MSO. We then show by empirical evaluations that the first-order encoding does perform better than both second-order encodings. The conclusion is that first-order encoding is a better choice than second-order encoding in LTLf-to-Automata translation.