Publication Type

Journal Article

Version

acceptedVersion

Publication Date

7-2025

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 formula size in the worst case. In this case, the synthesis 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 via 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 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.

Keywords

Reactive Synthesis, Realizability, LTL over Finite Traces, Game

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Areas of Excellence

Digital transformation

Publication

ACM Transactions on Software Engineering and Methodology

First Page

1

Last Page

32

ISSN

1049-331X

Identifier

10.1145/3749101

Publisher

Association for Computing Machinery (ACM)

Additional URL

https://doi.org/10.1145/3749101

Download

Share

COinS