Symbolic 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.
Cite
Text
Zhu et al. "Symbolic LTLf Synthesis." International Joint Conference on Artificial Intelligence, 2017. doi:10.24963/IJCAI.2017/189Markdown
[Zhu et al. "Symbolic LTLf Synthesis." International Joint Conference on Artificial Intelligence, 2017.](https://mlanthology.org/ijcai/2017/zhu2017ijcai-symbolic/) doi:10.24963/IJCAI.2017/189BibTeX
@inproceedings{zhu2017ijcai-symbolic,
title = {{Symbolic LTLf Synthesis}},
author = {Zhu, Shufang and Tabajara, Lucas M. and Li, Jianwen and Pu, Geguang and Vardi, Moshe Y.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2017},
pages = {1362-1369},
doi = {10.24963/IJCAI.2017/189},
url = {https://mlanthology.org/ijcai/2017/zhu2017ijcai-symbolic/}
}