First-order vs. Second-order encodings for LTL_f-to-automata translation

Translating formulas of Linear Temporal Logic (ltl) over finite traces, or LTL_f, to symbolic Deterministic Finite Automata (DFA) plays an important role not only in LTL_f 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 LTL_f formulas to translate LTL_f 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 LTL_f formulas. We first introduce a specific mso encoding that captures the semantics of LTL_f 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 LTL_f -to-Automata translation.