On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts

TL;DR

This paper introduces an efficient on-the-fly synthesis method for LTL over finite traces using direct TDFA construction and game solving, significantly improving performance over traditional automata-based approaches.

Contribution

It presents a novel on-the-fly synthesis framework leveraging direct TDFA construction, game-based algorithms, and optimization techniques for LTLf synthesis.

Findings

Achieves superior performance on benchmark tests

Enables parallelized synthesis and automata construction

Effectively complements existing LTLf synthesis tools

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.