On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts
Shengping Xiao, Yongkang Li, Shufang Zhu, Jun Sun, Jianwen Li, Geguang Pu, Moshe Y. Vardi
TL;DR
The paper addresses the bottleneck of constructing complete deterministic automata for LTL_f synthesis by introducing an on-the-fly, top-down TDFA-based framework that couples automata construction with TDFA game solving. It develops a formal TDFA construction from LTL_f via formula progression, and defines TDFA games to capture realizability as a game on the automaton, enabling forward global and backward local reasoning with SCC detection. Two optimizations, model-guided synthesis and state entailment, improve practical efficiency, and the authors implement a tool called Tople to benchmark against state-of-the-art approaches. Experimental results show that the on-the-fly approach yields strong overall performance and complementary strengths across benchmark classes compared to backward and forward baselines. The work advance s practical reactive synthesis for finite-trace specifications and offers a viable path toward minimizing automata blowup in real-world scenarios.
Abstract
We present an on-the-fly synthesis framework for Linear Temporal Logic over finite traces (LTLf) based on top-down deterministic automata construction. Existing approaches rely on constructing a complete Deterministic Finite Automaton (DFA) corresponding to the LTLf 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 LTLf into Transition-based DFA (TDFA) by directly leveraging LTLf semantics, incorporating intermediate results as direct components of the final automaton to enable parallelized synthesis and automata construction. We then explore the relationship between LTLf synthesis and TDFA games and subsequently develop an algorithm for performing LTLf 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.