PDDL 2.1 is the community standard for specifications of temporal planning problems, involving actions that have a duration and can overlap in time. Recent work has shown that some modelling features, such as intermediate and conditional effects, can be expressed in PDDL 2.1 by means of specific encodings. At the core of these encodings is a construction that requires two events to happen simultaneously. However, in practice, almost none of the state-space heuristic search planners known in the literature are capable of finding plans exhibiting this required simultaneity, suggesting that the search approach they use is actually incomplete with regards to the official PDDL 2.1 semantics. In this paper, we explore this issue both theoretically and experimentally. On the theoretical side, we define two different notions of required simultaneity, and we isolate which features of the semantics of PDDL 2.1 allow for such behaviors and how to possibly change the semantics to forbid each of them. In particular, we prove that the crucial detail is how the over-all conditions interact with the mutex relation. From these observations we isolate the reason why most search-based planners cannot find plans with required simultaneity, and provide an updated search strategy that recovers semantic completeness at the cost of a larger branching factor which, however, can be suitably pruned thanks to an application of our results. On the experimental side, we compare the proposed search strategies, showing that our pruning criterion allows us to recover semantic completeness without significant overhead.

We investigate a fragment of Linear Temporal Logic (LTL) comprising the tomorrow (X) and eventually (F) modalities, and present a singly exponential time algorithm for the pastification problem within this fragment. The pastification problem consists of constructing, for a given LTL formula, an equivalent formula that exclusively employs past temporal operators. While the best known algorithms for this task in full LTL–and in the fragment under consideration–exhibit triply exponential time complexity, our approach achieves optimal complexity for this fragment. The proposed algorithm proceeds in two main stages: (i) the input formula is first translated into a tailored normal form, and then (ii) a pure past formula is synthesized from a tree-like structure derived from the normalized formula. With minor adaptations, the algorithm extends to handle the fragment of LTL featuring the tomorrow and globally modalities. We provide an implementation of the algorithm in the temporal reasoning tool BLACK, and report on an experimental evaluation of its performance.1

First-order linear temporal logic (FOLTL) is a flexible and expressive formalism capable of naturally describing complex behaviors and properties. Although the logic is in general highly undecidable, the idea of using it as a specification language for the verification of complex infinite-state systems is appealing. However, a missing piece, which has proved to be an invaluable tool in dealing with other temporal logics, is an automaton model capable of capturing the logic. In this paper we address this issue, by defining and studying such a model, which we call first-order automaton. We define this very general class of automata, and the corresponding notion of regular first-order language (of finite words), showing their closure under most language-theoretic operations. We show how they can capture any FOLTL formula over finite words, over any signature and theory, and provide sufficient conditions for the semi-decidability of their non-emptiness problem. Then, to show the usefulness of the formalism, we prove the decidability of monodic FOLTL, a classic result known in the literature, with a simpler and direct proof.

Counterfactual Explanations (CEs) are a powerful technique used to explain Machine Learning models by showing how the input to a model should be minimally changed for the model to produce a different output. Similar proposals have been made in the context of Automated Planning, where CEs have been characterised in terms of minimal modifications to an existing plan that would result in the satisfaction of a different goal. While such explanations may help diagnose faults and reason about the characteristics of a plan, they fail to capture higher-level properties of the problem being solved. To address this limitation, we propose a novel explanation paradigm that is based on counterfactual scenarios. In particular, given a planning problem P and an LTLf formula ψ defining desired properties of a plan, counterfactual scenarios identify minimal modifications to P such that it admits plans that comply with ψ. In this paper, we present two qualitative instantiations of counterfactual scenarios based on an explicit quantification over plans that must satisfy ψ. We then characterise the computational complexity of generating such counterfactual scenarios when different types of changes are allowed on P. We show that producing counterfactual scenarios is often only as expensive as computing a plan for P, thus demonstrating the practical viability of our proposal and ultimately providing a framework to construct practical algorithms in this area.

Linear Temporal Logic over finite traces ( LTL f ) has proved itself to be an important and effective formalism in formal verification as well as in artificial intelligence. Pure past LTL f ( pLTL ) is the variant of LTL f featuring only past temporal modalities, and is naturally interpreted at the end of a finite trace. It is known that each property definable in LTL f is also definable in pLTL , and vice versa (they are expressively equivalent). The same goes for the safety and cosafety fragments of Linear Temporal Logic over infinite traces ( LTL ), when compared to G ( pLTL ) and F ( pLTL ) formulas, respectively, that is, pLTL formulas prefixed by a globally and an eventually modality. However, despite being extensively used in practice, to the best of our knowledge, there is no systematic study of their succinctness. Moreover, when considering (co)safety fragments of LTL devoid of binary temporal modalities, there are no known characterizations based on pLTL . In this paper, we investigate succinctness issues for LTL f and (co)safety fragments of LTL when compared with their pure past counterparts. First, we provide a pure past characterization of the (co)safety fragments of LTL devoid of binary temporal modalities. Then, we prove that the (co)safety fragments of LTL have pure past counterparts that can be exponentially more succinct. Finally, we show that the same holds for LTL f with respect to pLTL , and viceversa: LTL f and pLTL are incomparable when succinctness is concerned.

Abstract Operator Precedence Languages (OPL) have been recently identified as a suitable formalism for model checking recursive procedural programs, thanks to their ability of modeling the program stack. OPL requirements can be expressed in thePrecedence Oriented Temporal Logic(), which features modalities to reason on the natural matching between function calls and returns, exceptions, and other advanced programming constructs that previous approaches, such as Visibly Pushdown Languages, cannot model effectively. Existing approaches for model checking of have been designed following the explicit-state, automata-based approach, a feature that severely limits their scalability. In this paper, we give the first symbolic, SMT-based approach for model checking properties. While previous approaches construct the automaton for both the formula and the model of the program, we encode them into a (sequence of) SMT formulas. The search of a trace of the model witnessing a violation of the formula is then carried out by an SMT-solver, in a Bounded Model Checking fashion. We carried out an experimental evaluation, which shows the effectiveness of the proposed solution.

Abstract Linear temporal logic( $$\textsf{LTL}\,$$ LTL ) and its variant interpreted onfinite traces( $$\textsf{LTL}_{\textsf{f}\,}$$ LTLf ) are among the most popular specification languages in the fields of formal verification, artificial intelligence, and others. In this paper, we focus on the satisfiability problem for $$\textsf{LTL}\,$$ LTL and $$\textsf{LTL}_{\textsf{f}\,}$$ LTLf formulas, for which many techniques have been devised during the last decades. Among these aretableau systems, of which the most recent is Reynolds’ tree-shaped tableau. We provide a SAT-based algorithm for $$\textsf{LTL}\,$$ LTL and $$\textsf{LTL}_{\textsf{f}\,}$$ LTLf satisfiability checking based on Reynolds’ tableau, proving its correctness and discussing experimental results obtained through its implementation in the BLACK satisfiability checker.

In the timeline-based approach to planning, the evolution over time of a set of state variables (the timelines) is governed by a set of temporal constraints. Traditional timeline-based planning systems excel at the integration of planning with execution by handling temporal uncertainty. In order to handle general nondeterminism as well, the concept of timeline-based games has been recently introduced. It has been proved that finding whether a winning strategy exists for such games is 2EXPTIME-complete. However, a concrete approach to synthesize controllers implementing such strategies is missing. This paper fills this gap, by providing an effective and computationally optimal approach to controller synthesis for timeline-based games.

Abstract Realizability and reactive synthesis from temporal logics are fundamental problems in formal verification. The complexity of these problems for linear temporal logic with past ( ) led to the identification of fragments with lower complexities and simpler algorithms. Recently, the logic of extended bounded response ( $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P for short) has been introduced. It allows one to express safety languages definable in and it is provided with an efficient, fully symbolic algorithm for reactive synthesis. This paper features four related contributions. First, we introduce - , an extension of $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P with fairness conditions, assumptions, and guarantees that, on the one hand, allows one to express properties beyond the safety fragment and, on the other, it retains the efficiency of $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P in practice. Second, we the expressiveness of - starting from the expressiveness of its fragments. In particular, we prove that: (1) $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P is expressively complete with respect to the safety fragment of , (2) the removal of past operators from $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P results into a loss of expressive power, and (3) - is expressively equivalent to the logic of Bloem et al. Third, we provide a fully symbolic algorithm for the realizability problem from - specifications, that reduces it to a number of safety subproblems. Fourth, to ensure soundness and completeness of the algorithm, we propose and exploit a general framework for safety reductions in the context of realizability of (fragments of) . The experimental evaluation shows promising results.

The field of tumor phylogenetics focuses on studying the differences within cancer cell populations. Many efforts are done within the scientific community to build cancer progression models trying to understand the heterogeneity of such diseases. These models are highly dependent on the kind of data used for their construction, therefore, as the experimental technologies evolve, it is of major importance to exploit their peculiarities. In this work we describe a cancer progression model based on Single Cell DNA Sequencing data. When constructing the model, we focus on tailoring the formalism on the specificity of the data. We operate by defining a minimal set of assumptions needed to reconstruct a flexible DAG structured model, capable of identifying progression beyond the limitation of the infinite site assumption. Our proposal is conservative in the sense that we aim to neither discard nor infer knowledge which is not represented in the data. We provide simulations and analytical results to show the features of our model, test it on real data, show how it can be integrated with other approaches to cope with input noise. Moreover, our framework can be exploited to produce simulated data that follows our theoretical assumptions. Finally, we provide an open source R implementation of our approach, called CIMICE, that is publicly available on BioConductor.

Linear Temporal Logic (LTL) is the de-facto standard temporal logic for system specification, whose foundational properties have been studied for over five decades. Safety and cosafety properties of LTL define notable fragments of LTL, where a prefix of a trace suffices to establish whether a formula is true or not over that trace. In this paper, we study the complexity of the problems of satisfiability, validity, and realizability over infinite and finite traces for the safety and cosafety fragments of LTL. As for satisfiability and validity over infinite traces, we prove that the majority of the fragments have the same complexity as full LTL, that is, they are PSPACE-complete. The picture is radically different for realizability: we find fragments with the same expressive power whose complexity varies from 2EXPTIME-complete (as full LTL) to EXPTIME-complete. Notably, for all cosafety fragments, the complexity of the three problems does not change passing from infinite to finite traces, while for all safety fragments the complexity of satisfiability (resp., realizability) over finite traces drops to NP-complete (resp., Πᴾ₂- complete).

We study Linear Temporal Logic Modulo Theories over Finite Traces (LTLMTf), a recently introduced extension of LTL over finite traces (LTLf) where propositions are replaced by first-order formulas and where first-order variables referring to different time points can be compared. In general, LTLMTf was shown to be semi-decidable for any decidable first-order theory (e.g., linear arithmetics), with a tableau-based semi-decision procedure. In this paper we present a sound and complete pruning rule for the LTLMTf tableau. We show that for any LTLMTf formula that satisfies an abstract, semantic condition, that we call finite memory, the tableau augmented with the new rule is also guaranteed to terminate. Last but not least, this technique allows us to establish novel decidability results for the satisfiability of several fragments of LTLMTf, as well as to give new decidability proofs for classes that are already known.

Bounded numeric planning, where each numeric variable domain is bounded, is PSPACE-complete, but such a complexity result does not capture how hard it really is, since the same holds even for the practically much easier STRIPS fragment. A finer way to compare the difficulty of planning formalisms is through the notion of compilability, which has been however extensively studied only for classical planning by Nebel. This paper extends Nebel's framework to the setting of bounded numeric planning. First, we identify a variety of numeric fragments differing on the degree of the polynomials involved and the availability of features such as conditional effects and Boolean conditions; then we study the compilability of these fragments to each other and to the classical fragments. Surprisingly, numeric and classical planning with conditional effects and Boolean conditions can be compiled both ways preserving plan size exactly, while the same does not hold when targeting pure STRIPS. Our study reveals also that numeric fragments cluster into two equivalence classes separated by the availability of incomplete initial state specifications, a feature allowing to specify uncertainty in the initial state.

Confronting the past can be hard. This is true even in Linear Temporal Logic (LTL), interpreted on either infinite or finite traces, when faced with the problem of transforming a temporally future formula into an equivalent one that contains past temporal modalities only. To our knowledge, the best among the available pastification procedures for full LTL, as well as for expressive enough fragments of it (that is, containing at least one temporal modality other than tomorrow), are triply exponential in the size of the input. In this paper, we focus on the fragment of LTL that features the tomorrow and eventually modalities, and provide a singly exponential pastification algorithm for it. The transformation is based on a normalisation procedure that requires a non-trivial complexity analysis, and on the subsequent generation of a pure past formula from suitably-defined dependency tree structures. Moreover, leveraging its purely syntactic nature, we present an implementation of our procedure in a temporal satisfiability checking tool that deals with both future and past modalities.

Many complex scenarios require the coordination of agents holding different points of view, possibly cooperating and not necessarily agreeing. For this reason, standpoint logic (SL) has been recently introduced in the context of knowledge integration, allowing one to reason with diverse and potentially conflicting viewpoints held by different agents. Linear temporal logic (LTL) is the most widely known formalism to express temporal properties of systems and processes, both in formal methods and artificial intelligence related fields. In this paper, we present 'standpoint linear temporal logic' (SLTL), a new logic that combines the temporal features of LTL with the multi-perspective modelling capacity of SL. We define the logic SLTL, its syntax, its semantics, establish its decidability and complexity, and provide a terminating tableau calculus to automate SLTL reasoning. Conveniently, this offers a clear path to extend existing LTL reasoners to provide practical reasoning support for temporal reasoning in multi-perspective settings.

Linear Temporal Logic (LTL) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free omega-automata, to star-free omega-regular expressions, and (by Kamp's theorem) to the First-Order Theory of Linear Orders (FO-TLO). Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. SafetyLTL (resp., coSafetyLTL) is a fragment of LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. The main contribution of this paper is the introduction of a fragment of FO-TLO, called SafetyFO, and of its dual coSafetyFO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize SafetyLTL and coSafetyLTL, respectively, a result that joins Kamp's theorem, and provides a clearer view of the characterization of (fragments of) LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in LTL is definable in SafetyLTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we prove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL) devoid of the tomorrow (resp., weak tomorrow) operator captures the safety (resp., co-safety) fragment of LTL over finite words.

Abstract Linear Temporal Logic ( $$\mathsf {LTL}$$ LTL ) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Its widespread use is also due to its strong foundational properties. One of them is Kamp’s theorem, showing that $$\mathsf {LTL}$$ LTL and the first-order theory of one successor ( $$\mathsf {S1S}[\mathsf {FO}]$$ S 1 S [ FO ] ) are expressively equivalent. Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not or does belong to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for $$\mathsf {LTL}$$ LTL . $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL (resp., $$\mathsf {coSafety\text {-} \mathsf {LTL}}$$ coSafety - LTL ) is a fragment of $$\mathsf {LTL}$$ LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. In this paper, we introduce a fragment of $$\mathsf {S1S}[\mathsf {FO}]$$ S 1 S [ FO ] , called $$\mathsf {Safety\text {-} FO}$$ Safety - FO , and its dual $$\mathsf {coSafety\text {-} FO}$$ coSafety - FO , which are expressively complete with regards to the $$\mathsf {LTL}$$ LTL -definable safety languages. In particular, we prove that they respectively characterise exactly $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL and $$\mathsf {coSafety\text {-} \mathsf {LTL}}$$ coSafety - LTL , a result that joins Kamp’s theorem, and provides a clearer view of the charactisations of (fragments of) $$\mathsf {LTL}$$ LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in $$\mathsf {LTL}$$ LTL is definable in $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL interpreted over finite and infinite traces.

This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spirit of Satisfiability Modulo Theories. The resulting logic, called LTLf Modulo Theories (LTLfMT), is semi-decidable. Nevertheless, its high expressiveness comes useful in a number of use cases, such as model-checking of data-aware processes and data-aware planning. Despite the general undecidability of these problems, being able to solve satisfiable instances is a compromise worth studying. After motivating and describing such use cases, we provide a sound and complete semi-decision procedure for LTLfMT based on the SMT encoding of a one-pass tree-shaped tableau system. The algorithm is implemented in the BLACK satisfiability checking tool, and an experimental evaluation shows the feasibility of the approach on novel benchmarks.

In this paper, we study the computational complexity of action-based temporal planning interpreted over dense time. When time is assumed to be discrete, the problem is known to be EXPSPACE-complete. However, the official PDDL 2.1 semantics and many implementations interpret time as a dense domain. This work provides several results about the complexity of the problem, focusing on some particularly interesting cases: whether a minimum amount ε of separation between mutually exclusive events is given, in contrast to the separation being simply required to be non-zero, and whether or not actions are allowed to overlap already running instances of themselves. We prove the problem to be PSPACE-complete when self-overlap is forbidden, whereas, when it is allowed, it becomes EXPSPACE-complete with ε-separation and even undecidable with non-zero separation. These results clarify the computational consequences of different choices in the definition at the core of the PDDL 2.1 semantics, which have been vague until now.1

LTL+Past is the extension of Linear Temporal Logic (LTL) supporting past temporal operators. The addition of the past does not add expressive power, but does increase the usability of the language both in formal verification and in artificial intelligence, e.g., in the context of multi-agent systems. In this paper, we add the support of past operators to BLACK, a satisfiability checker for LTL based on a SAT encoding of a tree-shaped tableau system. We implement two ways of supporting the past in the tool. The first one is an equisatisfiable translation that removes the past operators, obtaining a future-only formula that can be solved with the original LTL engine. The second one extends the SAT encoding of the underlying tableau to directly support the tableau rules that deal with past operators. We describe both approaches and experimentally compare the two between themselves and with the νXmv model checker, obtaining promising results.

This paper studies the computational complexity of temporal planning, as represented by PDDL 2.1, interpreted over dense time. When time is considered discrete, the problem is known to be EXPSPACE-complete. However, the official PDDL 2.1 semantics, and many implementations, interpret time as a dense domain. This work provides several results about the complexity of the problem, studying a few interesting cases: whether a minimum amount ϵ of separation between mutually exclusive events is given, in contrast to the separation being simply required to be non-zero, and whether or not actions are allowed to overlap already running instances of themselves. We prove the problem to be PSPACE-complete when self-overlap is forbidden, whereas, when allowed, it becomes EXPSPACE-complete with ϵ-separation and undecidable with non-zero separation. These results clarify the computational consequences of different choices in the definition of the PDDL 2.1 semantics, which were vague until now.

Reactive synthesis is a key technique for the design of correct-by-construction systems and has been thoroughly investigated in the last decades.It consists in the synthesis of a controller that reacts to environment's inputs satisfying a given temporal logic specification.Common approaches are based on the explicit construction of automata and on their determinization, which limit their scalability.In this paper, we introduce a new fragment of Linear Temporal Logic, called Extended Bounded Response LTL (LTL EBR ), that allows one to combine bounded and universal unbounded temporal operators (thus covering a large set of practical cases), and we show that reactive synthesis from LTL EBR specifications can be reduced to solving a safety game over a deterministic symbolic automaton built directly from the specification.We prove the correctness of the proposed approach and we successfully evaluate it on various benchmarks.

The timeline-based approach to automated planning was originally developed in the context of space missions. In this approach, problem domains are expressed as systems consisting of independent but interacting components whose behaviors over time, the timelines, are governed by a set of temporal constraints, called synchronization rules. Although timeline-based system descriptions have been successfully used in practice for decades, the research on the theoretical aspects only started recently. In the last few years, some interesting results have been shown concerning both its expressive power and the computational complexity of the related planning problem. In particular, the general problem has been proved to be EXPSPACE-complete. Given the applicability of the approach in many practical scenarios, it is thus natural to ask whether computationally simpler but still expressive fragments can be identified. In this paper, we study the timeline-based planning problem with the restriction that only qualitative synchronization rules, i.e., rules without explicit time bounds in the constraints, are allowed. We show that the problem becomes PSPACE-complete.

In timeline-based planning, domains are described as sets of independent, but interacting, components, whose behaviour over time (the set of timelines) is governed by a set of temporal constraints. A distinguishing feature of timeline-based planning systems is the ability to integrate planning with execution by synthesising control strategies for flexible plans. However, flexible plans can only represent temporal uncertainty, while more complex forms of nondeterminism are needed to deal with a wider range of realistic problems. In this paper, we propose a novel game-theoretic approach to timeline-based planning problems, generalising the state of the art while uniformly handling temporal uncertainty and nondeterminism. We define a general concept of timeline-based game and we show that the notion of winning strategy for these games is strictly more general than that of control strategy for dynamically controllable flexible plans. Moreover, we show that the problem of establishing the existence of such winning strategies is decidable using a doubly exponential amount of space.

Automated planning is an important area of Artificial Intelligence, which has been thoroughly developed in the last decades. In recent years, a significant amount of research has focused on planning languages and systems supporting temporal reasoning, recognizing its importance in modeling and solving real-world complex tasks. Many such languages are action-based, i.e. they model planning problems by specifying which actions can be executed at any given time to affect the environment. Timeline-based planning, a different paradigm originally introduced to support planning and scheduling of space operations, models planning domains as systems composed of a set of independent, but interacting, components, whose behavior over time, the timelines, is governed by a set of temporal constraints. A thorough theoretical study of timeline-based planning languages, and a rigorous comparison with action-based languages, are still missing. We outline recent results and future directions on this front.

Within the timeline-based framework, planning problems are modeled as sets of independent, but interacting, components whose behavior over time is described by a set of temporal constraints. Timeline-based planning is being used successfully in a number of complex tasks, but its theoretical properties are not so well studied. In particular, while it is known that Linear Temporal Logic (LTL) can capture classical action-based planning, a similar logical characterization was not available for timeline-based planning formalisms. This paper shows that timeline-based planning with bounded temporal constraints can be captured by a bounded version of Timed Propositional Temporal Logic, augmented with past operators, which is an extension of LTL originally designed for the verification of real-time systems. As a byproduct, we get that the proposed logic is expressive enough to capture temporal action-based planning problems.

Linear Temporal Logic (LTL) is a de-facto standard formalism for expressing properties of systems and temporal constraints in formal verification, artificial intelligence, and other areas of computer science. The problem of LTL satisfiability is thus prominently important to check the consistency of these temporal specifications. Although adding past operators to LTL does not increase its expressive power, recently the interest for explicitly handling the past in temporal logics has increased because of the clarity and succinctness that those operators provide. In this work, a recently proposed one-pass tree-shaped tableau system for LTL is extended to support past operators. The modularity of the required changes provides evidence for the claimed ease of extensibility of this tableau system.

Planning prblems are usually expressed by specifying which actions can be performed to obtain a given goal. In temporal planning problems, actions come with a time duration and can overlap in time, which noticeably increase the complexity of the reasoning process. Action-based temporal planning has been thoroughly studied from the complexity-theoretic point of view, and it has been proved to be EXPSPACE-complete in its general formulation. Conversely, timeline-based planning problems are represented as a collection of variables whose time-varying behavior is governed by a set of temporal constraints, called synchronization rules. Timelines provide a unified framework to reason about planning and execution under uncertainty. Timeline-based systems are being successfully employed in real-world complex tasks, but, in contrast to action-based planning, little is known on their computational complexity and expressiveness. In particular, a comparison of the expressiveness of the action-and timeline-based formalisms is still missing. This paper contributes a first step in this direction by proving that timelines are expressive enough to capture action-based temporal planning, showing as a byproduct the EXPSPACE-completeness of timeline-based planning with no temporal horizon and bounded temporal relations only.