Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications

TL;DR

This paper introduces a hybrid explicit-symbolic approach to convert LTLf formulas into DFAs, significantly improving scalability and efficiency in reactive synthesis by overcoming existing bottlenecks.

Contribution

It proposes a novel hybrid state-space representation combining explicit and symbolic methods for LTLf to DFA conversion, addressing scalability issues in reactive synthesis.

Findings

Hybrid approach outperforms existing methods in scalability.

Reduces time and memory consumption during conversion.

Supports larger and more complex specifications.

Abstract

LTLf synthesis is the automated construction of a reactive system from a high-level description, expressed in LTLf, of its finite-horizon behavior. So far, the conversion of LTLf formulas to deterministic finite-state automata (DFAs) has been identified as the primary bottleneck to the scalabity of synthesis. Recent investigations have also shown that the size of the DFA state space plays a critical role in synthesis as well. Therefore, effective resolution of the bottleneck for synthesis requires the conversion to be time and memory performant, and prevent state-space explosion. Current conversion approaches, however, which are based either on explicit-state representation or symbolic-state representation, fail to address these necessities adequately at scale: Explicit-state approaches generate minimal DFA but are slow due to expensive DFA minimization. Symbolic-state representations can be succinct, but due to the lack of DFA minimization they generate such large state spaces that even their symbolic representations cannot compensate for the blow-up. This work proposes a hybrid representation approach for the conversion. Our approach utilizes both explicit and symbolic representations of the state-space, and effectively leverages their complementary strengths. In doing so, we offer an LTLf to DFA conversion technique that addresses all three necessities, hence resolving the bottleneck. A comprehensive empirical evaluation on conversion and synthesis benchmarks supports the merits of our hybrid approach.