Symbolic LTLf Synthesis

Symbolic LTLf Synthesis

Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 1362-1369. https://doi.org/10.24963/ijcai.2017/189

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.
Keywords:
Knowledge Representation, Reasoning, and Logic: Automated Reasoning and Theorem Proving
Knowledge Representation, Reasoning, and Logic: Game Theory
Knowledge Representation, Reasoning, and Logic: Logics for Knowledge Representation