A Compositional Framework for On-the-Fly LTLf Synthesis

TL;DR

This paper presents a novel compositional on-the-fly synthesis framework for LTLf that combines existing methods, enabling efficient reactive synthesis for large formulas by integrating composition during game solving and employing pruning strategies.

Contribution

It introduces a new framework that integrates compositional and incremental DFA construction during game solving, improving scalability for large LTLf specifications.

Findings

Solves more instances than existing solvers.

Enables early unrealizability detection.

Offers two effective composition variants.

Abstract

Reactive synthesis from Linear Temporal Logic over finite traces (LTLf) can be reduced to a two-player game over a Deterministic Finite Automaton (DFA) of the LTLf specification. The primary challenge here is DFA construction, which is 2EXPTIME-complete in the worst case. Existing techniques either construct the DFA compositionally before solving the game, leveraging automata minimization to mitigate state-space explosion, or build the DFA incrementally during game solving to avoid full DFA construction. However, neither is dominant. In this paper, we introduce a compositional on-the-fly synthesis framework that integrates the strengths of both approaches, focusing on large conjunctions of smaller LTLf formulas common in practice. This framework applies composition during game solving instead of automata (game arena) construction. While composing all intermediate results may be necessary in the worst case, pruning these results simplifies subsequent compositions and enables early detection of unrealizability. Specifically, the framework allows two composition variants: pruning before composition to take full advantage of minimization or pruning during composition to guide on-the-fly synthesis. Compared to state-of-the-art synthesis solvers, our framework is able to solve a notable number of instances that other solvers cannot handle. A detailed analysis shows that both composition variants have unique merits.