An On-the-Fly Synthesis Framework for LTL over Finite Traces

We present an on-the-fly synthesis framework for Linear Temporal Logic over Finite Traces (<ani:sans-serif>LTL</ani:sans-serif>_f) based on top-down deterministic automata construction. Existing approaches rely on constructing a complete Deterministic Finite Automaton (<ani:sans-serif>DFA</ani:sans-serif>) corresponding to the <ani:sans-serif>LTL</ani:sans-serif>_f specification, a process with doubly exponential complexity relative to formula size in the worst case. In this case, the synthesis cannot be conducted until the entire <ani:sans-serif>DFA</ani:sans-serif> is constructed. This inefficiency is the main bottleneck of existing approaches. To address this challenge, we first present a method for converting <ani:sans-serif>LTL</ani:sans-serif>_f into Transition-Based <ani:sans-serif>DFA</ani:sans-serif> (<ani:sans-serif>TDFA</ani:sans-serif>) by directly leveraging <ani:sans-serif>LTL</ani:sans-serif>_f semantics, incorporating intermediate results as direct components of the final automaton to enable parallelized synthesis and automata construction. We then explore the relationship between <ani:sans-serif>LTL</ani:sans-serif>_f synthesis and <ani:sans-serif>TDFA</ani:sans-serif> games and subsequently develop an algorithm for performing <ani:sans-serif>LTL</ani:sans-serif>_f synthesis via on-the-fly <ani:sans-serif>TDFA</ani:sans-serif> game solving. This algorithm traverses the state space in a global forward manner combined with a local backward method, along with detecting strongly connected components. Moreover, we introduce two optimization techniques—model-guided synthesis and state entailment—to enhance the practical efficiency of our approach. Experimental results demonstrate that our on-the-fly approach achieves the best performance on the tested benchmarks and effectively complements existing approaches.