Synthesis for LTL and LDL on Finite Traces
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Main Track. Pages 1558-1563.
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.
@inproceedings{ijcai2015p223,
title = {Synthesis for LTL and LDL on Finite Traces},
author = {De Giacomo, Giuseppe and Vardi, Moshe Y.},
booktitle = {Proceedings of the Twenty-Fourth International Joint Conference on
Artificial Intelligence, {IJCAI-15}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Qiang Yang and Michael Wooldridge},
pages = {1558--1563},
year = {2015},
month = {7},
note = {Main Track},
url = {https://ijcai.org/proceedings/2015/223},
}
TY - CPAPER TI - Synthesis for LTL and LDL on Finite Traces AU - De Giacomo, Giuseppe AU - Vardi, Moshe Y. T2 - Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15 PB - International Joint Conferences on Artificial Intelligence PY - 2015 SP - 1558 EP - 1563 UR - https://ijcai.org/proceedings/2015/223 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
