---
title: "Synthesis for LTL and LDL on Finite Traces"
authors:
  - "Giuseppe De Giacomo"
  - "Moshe Y. Vardi"
doi: ""
url: "https://ijcai.org/proceedings/2015/223"
pdf: "https://ijcai.org/proceedings/2015/0223.pdf"
venue: "Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence"
year: 2015
pages: "1558-1563"
track: "Main Track"
keywords:
---

# Synthesis for LTL and LDL on Finite Traces

Giuseppe De Giacomo, Moshe Y. Vardi

*Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence*, 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.