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., $mathbf{LTL}_{f}$. We propose a SAT-based approach to translate an $mathbf{LTL}_{f}$ 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. $mathbf{LTL}_{f}$ satisfiability checking and synthesis. Unlike extant approaches to translate $mathbf{LTL}_{f}$ formulas to the equivalent finite automata, which are indirect and have to introduce intermediate procedures, our methodology enables the direct construction from $mathbf{LTL}_{f}$ formulas to the finite automata. We evaluated our NFA construction together with other two $mathbf{LTL}_{f}$ -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.