SAT-Based Automata Construction for LTL over Finite Traces

In this paper, we consider the automata construction problem for Linear Temporal Logic over finite traces, i.e., LTLf. We propose a SAT-based approach to translate an LTLf formula to both of its equivalent Nondeterministic and Deterministic Finite Automata (NFA and DFA). Notably, the generated automata are transition-based instead of state-based, which may potentially be a better fit for the applications that can be achieved on the fly, e.g. LTLf satisfiability checking and synthesis. Unlike extant approaches to translate LTLf formulas to the equivalent finite automata, which are indirect and have to introduce intermediate procedures, our methodology enables the direct construction from LTLf formulas to the finite automata. We evaluated our NFA construction together with other two LTLf -to-automata approaches implemented in the MONA and SPOT tools, which shows that the performance of our construction is comparable to the other two. We leave the comparison on the DFA construction in the future work.