Symbolic LTLf Synthesis
This work addresses scalability issues in LTLf synthesis for formal verification and AI planning, though it is incremental as it builds on an existing reduction technique.
The paper tackles LTLf synthesis by proposing a symbolic framework that represents the DFA as a boolean formula instead of an explicit graph, enabling strategy generation via boolean synthesis. Experiments with the tool Syft show the symbolic approach scales better than the explicit one on scalable benchmarks.
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.