Symbolic LTLf Synthesis
Logic in Computer Science
2017-09-22 v2 Artificial Intelligence
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
@article{arxiv.1705.08426,
title = {Symbolic LTLf Synthesis},
author = {Shufang Zhu and Lucas M. Tabajara and Jianwen Li and Geguang Pu and Moshe Y. Vardi},
journal= {arXiv preprint arXiv:1705.08426},
year = {2017}
}