First-Order vs. Second-Order Encodings for $$\textsc {ltl}_f$$-to-Automata Translation

Translating formulas of Linear Temporal Logic (ltl) over finite traces, or \({\textsc {ltl}}_f\), to symbolic Deterministic Finite Automata (DFA) plays an important role not only in \({\textsc {ltl}}_f\) synthesis, but also in synthesis for Safety ltl formulas. The translation is enabled by using \(\mathsf {MONA}\), a powerful tool for symbolic, BDD-based, DFA construction from logic specifications. Recent works used a first-order encoding of \({\textsc {ltl}}_f\) formulas to translate \({\textsc {ltl}}_f\) to First Order Logic (fol), which is then fed to \(\mathsf {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.