On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts
This work addresses a bottleneck in automated synthesis for formal verification, offering a more efficient solution for tasks like controller design or protocol verification, though it is incremental as it builds on prior automata-based methods.
The paper tackles the inefficiency of existing Linear Temporal Logic over finite traces (LTLf) synthesis methods, which require constructing a complete deterministic finite automaton with doubly exponential complexity, by introducing an on-the-fly synthesis framework that uses transition-based deterministic finite automata and game solving, achieving the best performance on tested benchmarks.
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.