Timeline-based planning is an approach to automated planning, employed successfully over the last decades in space mission planning and scheduling, where problem domains are modelled as systems made of a number of independent but interacting components, whose behaviour over time, the timelines, is governed by a set of temporal constraints. Despite its practical success, a thorough theoretical understanding of the paradigm was missing. This thesis fills this gap, by providing the first detailed account of formal and computational properties of the timeline-based approach to planning. In particular, we focus on expressiveness and computational complexity issues. At first, we compare the expressiveness of timeline-based and action-based planning languages, showing that a particularly restricted variant of the problem is already expressive enough to compactly capture action-based temporal planning problems. Then, we move to the characterisation of the problem in terms of computational complexity, showing that finding a solution plan for a timeline-based planning problem is EXPSPACE-complete. Then, we approach the problem of timeline-based planning with uncertainty. We analyse the state-of-the-art approach to these problems, based on the concept of flexible plans, identifying some key issues, that we address by proposing timeline-based games, a two-players games where the controller plays agains the environment trying to satisfy the problem constraints. We show that this approach is strictly more general than the current one, and that deciding whether a winning strategy for such games exists belongs to 2NEXPTIME.
We then focus on expressiveness in logical terms, introducing a timed temporal logic apt to expressing timeline-based planning problem. We prove that satisfiability checking for this logic is EXPSPACE-complete, and we adapt to it a one-pass tree-shaped tableau method that extends one a recently introduced for LTL.
