Symbolic LTLf Synthesis

TL;DR

This paper introduces a symbolic framework for LTLf synthesis that uses boolean formulas to represent automata, enabling more scalable strategy generation compared to explicit graph methods.

Contribution

It proposes a novel symbolic approach to LTLf synthesis based on boolean formulas, improving scalability and efficiency over traditional explicit automata methods.

Findings

Symbolic approach scales better on large benchmarks.

Implementation in the Syft tool demonstrates improved performance.

Strategy generation via boolean synthesis is effective for LTLf synthesis.

Abstract

LTLf synthesis is the process of finding a strategy that satisfies a linear temporal specification over finite traces. An existing solution to this problem relies on a reduction to a DFA game. In this paper, we propose a symbolic framework for LTLf synthesis based on this technique, by performing the computation over a representation of the DFA as a boolean formula rather than as an explicit graph. This approach enables strategy generation by utilizing the mechanism of boolean synthesis. We implement this symbolic synthesis method in a tool called Syft, and demonstrate by experiments on scalable benchmarks that the symbolic approach scales better than the explicit one.