Synthesis for LTL and LDL on Finite Traces
Abstract
In this paper, we study synthesis from logical specifications over finite traces expressed in LTLf and its extension LDLf. Specifically, in this form of synthesis, propositions are partitionedin controllable and uncontrollable ones, and the synthesis task consists of setting the controllable propositions over time so that, in spite of how the value of the uncontrollable ones changes, the specification is fulfilled. Conditional planning in presence of declarative and procedural trajectory constraints is a special case of this form of synthesis. We characterize the problem computationally as 2EXPTIME-complete and present a sound and complete synthesis technique based on DFA (reachability) games.
Cite
Text
De Giacomo and Vardi. "Synthesis for LTL and LDL on Finite Traces." International Joint Conference on Artificial Intelligence, 2015.Markdown
[De Giacomo and Vardi. "Synthesis for LTL and LDL on Finite Traces." International Joint Conference on Artificial Intelligence, 2015.](https://mlanthology.org/ijcai/2015/giacomo2015ijcai-synthesis/)BibTeX
@inproceedings{giacomo2015ijcai-synthesis,
title = {{Synthesis for LTL and LDL on Finite Traces}},
author = {De Giacomo, Giuseppe and Vardi, Moshe Y.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2015},
pages = {1558-1564},
url = {https://mlanthology.org/ijcai/2015/giacomo2015ijcai-synthesis/}
}