Symbolic LTLf Synthesis

Understand

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.