On-the-fly Synthesis for LTL over Finite Traces

We present an on-the-fly synthesis framework for Linear Temporal Logic over finite traces (LTL 𝑓 ) based on top-down deterministic automata construction. Existing approaches rely on constructing a complete Deterministic Finite Automaton (DFA) corresponding to the LTL 𝑓 specification, a process with doubly exponential complexity relative to the formula size in the worst case. In this case, the synthesis procedure cannot be conducted until the entire DFA is constructed. This inefficiency is the main bottleneck of existing approaches. To address this challenge, we first present a method for converting LTL 𝑓 into Transition-based DFA (TDFA) by directly leveraging LTL 𝑓 semantics, incorporating intermediate results as direct components of the final automaton to enable parallelized synthesis and automata construction. We then explore the relationship between LTL 𝑓 synthesis and TDFA games and subsequently develop an algorithm for performing LTL 𝑓 synthesis using on-the-fly TDFA game solving. This algorithm traverses the state space in a global forward manner combined with a local backward method, along with the detection of 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 tools and approaches. CCS Concepts: • Software and its engineering → Formal methods; • Theory of computation → Automated reasoning; Modal and temporal logics.