Bounded Timed Propositional Temporal Logic with Past Captures Timeline-based Planning with Bounded Constraints

1 Introduction

Most of the languages used to describe automated planning problems, as, for instance, PDDL [Fox and Long, 2003; Gerevini et al., 2009], follow an action-based paradigm, focusing on which actions can be performed by an executor in order to achieve its goal. On the other hand, in timeline-based planning, problems are described as a set of independent, but interacting, components, whose behavior over time (the timelines) is governed by a set of temporal constraints. This more declarative approach turns out to be useful in describing and reasoning about problems dealing with a high number of interacting components. Moreover, the concept of flexible timeline allows one to represent uncertainty in the duration of tasks, as well as uncontrollable components modeling the behavior of the surrounding environment. Since its introduction at NASA [Muscettola, 1994] in the context of planning

gigante.nicola@spes.uniud.it of space operations, the timeline-based approach has been adopted by a number of planning systems, like EUROPA [Barreiro et al., 2012], ASPEN [Chien et al., 2000] and APSITRF [Cesta et al., 2009], and successfully employed in a variety of complex tasks and missions [Jónsson et al., 2000; Cesta et al., 2007; Cesta et al., 2010].

This work was partially supported by the Italian ¡NδA Σ GNCS project Logics and Automata for Interval Model Checking. In addition, Dario Della Monica acknowledges the financial support from a Marie Curie ¡NδA Σ -COFUND-2012 Outgoing Fellowship.

Action-based planning has been extensively studied from a theoretical point of view. Classical planning is known to be PSPACE-complete [Bylander, 1994], while temporal planning, where actions have explicit durations, is EXPSPACEcomplete [Rintanen, 2007]. Logical characterizations of action-based planning have been provided in [Cialdea Mayer et al., 2007; Cimatti et al., 2017], encoding the problem into Linear Temporal Logic (LTL) [Pnueli, 1977] or its variations.

Little is known about the theoretical properties of timelinebased planning problems. In particular, a complete picture of computational complexity and expressiveness of timelinebased planning languages is missing. A formalization of the problem, including flexible timelines and uncontrollable components, can be found in [Cimatti et al., 2013; Cialdea Mayer et al., 2014; Cialdea Mayer et al., 2016]. In [Gigante et al., 2016], Gigante et al. isolated a fragment of non-flexible timeline-based planning, which forbids the use of unbounded interval relations and is expressive enough to capture temporal action-based planning, and proved that it is EXPSPACEcomplete. A logical characterization of timeline-based planning is missing. Besides being a very natural question by itself, it would allow one to approach the problem of the controllability of problems with uncontrollable components in terms of logical synthesis [Schewe and Tian, 2011].

Timed Propositional Temporal Logic (TPTL) is an extension of LTL aimed at the verification of reactive systems with real-time constraints [Alur and Henzinger, 1994]. It extends LTL with a freeze quantifier that allows one to give a name to the timestamp of a given state, and then to employ it in timing constraints. The satisfiability checking problem for TPTL is EXPSPACE-complete, which makes it a good candidate for capturing timeline-based planning; unfortunately, it lacks the necessary past operators, and the extension of TPTL with past (TPTL+P) is non-elementary [Alur and Henzinger, 1993].

In this paper, we give a logical characterization of the fragment of non-flexible timeline-based planning studied in [Gigante et al., 2016], by showing that it can be naturally captured by a guarded fragment of TPTL+P which imposes an exponential upper bound to the scope of temporal operators when applied to formulae with free variables. We show that this restriction is enough to keep the satisfiability checking problem for the resulting logic EXPSPACE-complete. By exploiting the expressiveness result of [Gigante et al., 2016], the result directly transfers to temporal action-based planning.

The rest of the paper is organized as follows. In Sect. 2, we introduce the timeline-based planning problem. Then, in Sect. 3 we show that the considered fragment of TPTL with past is sufficient to capture it. Next, in Sect. 4 we determine the complexity of the logic. We conclude the paper by discussing future developments.

2 Timeline-based Planning

This section introduces notation and terminology of timelinebased planning, mostly borrowed from [Gigante et al., 2016] and extensively discussed in [Cialdea Mayer et al., 2016].

Definition 1 (State variable). A state variable x is a triple (Vx, Tx, Dx), where:

• Vx is the finite domain of the variable x;
• Tx : Vx → 2Vx is the value transition function, which maps each value v ∈ Vx to the set of values that x can take immediately after v;
• Dx : Vx → N×N is a function that maps each v ∈ Vx to a pair (dmin, dmax), with dmin ≤ dmax, where dmin and dmax are respectively the minimum and maximum duration of an interval over which x takes value v.

Which value is taken by a state variable over a specified time interval is described by means of tokens.

Definition 2 (Token). A token for x is a tuple τ = (x, v, d), where x = (Vx, Tx,Dx) is a state variable, v ∈ Vx, and d ∈ N is the duration of the token, with dmin ≤ d ≤ dmax, and Dx(v) = (dmin, dmax).

The time-varying behavior of a state variable is represented by means of a finite sequence of tokens, called a timeline.

Definition 3 (Timeline). A timeline for a state variable x = (Vx, Tx, Dx) is a non-empty finite sequence T = 〈τ1, . . . , τk〉 of tokens for x, where vi+1 ∈ Tx(vi) for i ∈ {1, . . . , k - 1}.

Notice that the values of x in two consecutive tokens do not need to be different. A time interval can be associated with any token τi = (x, vi, di) in a timeline T = 〈τ1, . . . , τk〉 by means of the functions start_time(τi) = ∑i-1 j=1 dj and end_time(τi) = start_time(τi)+di. The end time of the last token of a timeline is called the horizon of the timeline. In the following, when there is no ambiguity, we will interchangeably refer to a token and to the associated time interval.

The behavior of state variables is constrained by a set of synchronization rules, which relate tokens, possibly belonging to different timelines, through temporal relations among intervals or among intervals and time points. To express these temporal constraints, we adopt the compact notation proposed in [Gigante et al., 2016]. Let Σ = {a, b, c, . . .} be a set of token names used to refer to tokens.

Definition 4 (Atoms). An atom is either a clause of the form a ≤e1,e2 [l,u] b (interval), or of the form a ≤e1 [l,u] t or a ≥e1 [l,u] t

(time-point), where a, b ∈ Σ, l, u, t ∈ N, and e1, e2 are either start_time or end_time, respectively s and e for short.

As an example, the atom a ≤s,e [l,u] b constrains the token a to start before the end of b, and the distance between the two related endpoints to be between l and u.

Definition 5 (Synchronization rules). Let SV be a set of state variables. An existential statement is a statement of the form:

where C ≡ ρ0 ∧ . . . ∧ ρm is a conjunction of atoms, xi ∈ SV , ai ∈ Σ, and vi ∈ Vxi for each i ∈ {1, . . . , n}. The clauses ai[xi = vi] are called quantifiers. A token name used in C, but not occurring in any quantifier, is said to be free. A synchronization rule R is a clause in one of the following forms:

where a0 ∈ Σ, x0 ∈ SV , v0 ∈ Vx0 , and E1, . . . , Ek are existential statements where only a0 may appear free. In rules of the first form, the quantifier a0[x0 = v0] is called trigger. Rules of the second form are said to be trigger-less.

Intuitively, the trigger is a universal quantifier, which says that for all the tokens a0, where the variable x0 takes the value v0, at least one of the existential statements Ei must be true. The existential statements in turn assert the existence of tokens a1, . . . , an, where the respective state variables take the specified values, that satisfy the temporal constraints given by C. Trigger-less rules simply assert the satisfaction of the existential statements.

Definition 6 (Semantics of atoms). Given a set of tokens Γ and a function λ : Σ → Γ that assigns a token to each token name, an interval atom a ≤e1,e2 l,u b is satisfied by λ if l ≤ e2(λ(b)) - e1(λ(a)) ≤ u. A time-point atom of the form a ≤e[l,u] t or a ≥e[l,u] t is satisfied by λ if, respectively, l ≤ t - e(λ(a)) ≤ u or l ≤ e(λ(a)) - t ≤ u.

Definition 7 (Semantics of synchronization rules). Given a set of tokens Γ and a function λ : Σ → Γ, a quantifier a[x = v] is satisfied by λ if λ(a) = (xa, va, da), with xa = x and va = v. An existential statement E, with conjunct clause C, is satisfied by λ if all the quantifiers of E and all the atoms in C are satisfied by λ. A synchronization rule R of the form a0[x0 = v0] -→ E1 ∨ E2 ∨ . . . ∨ Ek is satisfied by Γ if, for every token τ = (xτ , vτ , dτ) ∈ Γ where xτ = x0 and vτ = v0, there is an existential statement Ei and a mapping λ : Σ → Γ such that λ(a0) = τ and λ satisfies Ei.

A timeline-based planning domain is specified by a set of state variables and a set of synchronization rules representing their admissible behaviors. Trigger-less rules can be used to express initial conditions, domain invariants, and the goals of the problem.

Definition 8 (Planning problem). A timeline-based planning problem is a pair P = (SV, S), where SV is a set of state variables and S is a set of synchronization rules involving variables in SV . A solution plan for P is a set of timelines

π = {T1, . . . , Tn}, one for each xi ∈ SV , such that all the synchronization rules in S are satisfied by the set Γ of all the tokens involved in π, that is, Γ = {τ | τ ∈ Ti, 1 ≤ i ≤ n}.

Some useful relations can be defined. As an example, a bounded version of the thirteen Allen's ordering relations between pairs of intervals [Allen, 1983] can be defined in terms of the basic interval atoms of Definition 4. For instance, the equality and the contains interval relations between a and b can be defined as, respectively, a ≤s,s [0,0] b ∧ a ≤e,e [0,0] b and a ≤s,s [l1,u1] b ∧ b ≤e,e [l2,u2] a for some bounds l1, l2, u1, u2 ∈ N.

3 Bounded TPTL with Past Captures Timeline-based Planning

This section introduces TPTLB+P, a variant of Timed Propositional Temporal Logic (TPTL), and shows how to reduce the timeline-based planning problem to the satisfiability problem of TPTLB+P formulae. TPTL is an extension of LTL originally introduced in the area of formal verification to model properties of real-time systems [Alur and Henzinger, 1994], whose satisfiability checking problem is EXPSPACE-complete. In its original definition, the logic only supports future temporal operators, because the addition of past modalities makes the complexity of the problem for the resulting logic TPTL+P non-elementary [Alur and Henzinger, 1993].

As a matter of fact, the possibility of referring to the past is useful to compactly encode timeline-based planning problems. For this reason, in this paper we introduce TPTLB+P, a guarded fragment of TPTL+P that features past modalities, but restricts the scope of both future and past modalities. TPTLB+P turns out to be expressive enough to capture timeline-based planning problems, without increasing the computational complexity of the satisfiability checking problem, which stays EXPSPACE-complete.

Let AP be a set of proposition letters and V be a set of variables. A TPTLB+P formula φ over AP and V is recursively defined as follows:

where p ∈ AP, φ1, φ2 are TPTLB+P formulae, x, y ∈ V, c ∈ Z, w ∈ N ∪ {+∞}, and in any formula of the forms Xwφ1, Ywφ1, φ1 Uw φ2, and φ1 Sw φ2, if w = +∞, then φ1, φ2 are closed formulae (a formula ψ is closed if any occurrence of a variable x is inside a subformula of the form x.φ). Formulae of the form x.φ are called freeze quantifications, while those of the forms x ≤ y+c and x ≤ c are called timing constraints. A missing w subscript stands for w = +∞. Standard logical and temporal shortcuts are used, such as ⊤ for p ∨ ¬p, for some p ∈ AP, ⊥ for ¬⊤, φ1 ∧ φ2 for ¬(¬φ1 ∨ ¬φ2), Fφ for ⊤U φ, Gφ for ¬F¬φ, and Pφ for ⊤S φ, as well as constraint shortcuts, such as, e.g., x ≤ y for x ≤ y + 0, x > y for ¬(x ≤ y), and x = y for ¬(x < y) ∧ ¬(y < x).

TPTLB+P formulae are interpreted over timed state sequences, i.e., structures ρ = (σ, τ), where σ = 〈σ0, σ1, . . .〉 is an infinite sequence of states σi ∈ 2AP , with i ≥ 0, and τ = 〈τ0, τ1, . . .〉 is an infinite sequence of timestamps τi ∈ N, with i ≥ 0, such that (i) τi+1 ≥ τi (monotonicity) and (ii) for all t ∈ N, there is some i ≥ 0 such that τi ≥ t (progress).

Formally, the semantics of TPTLB+P is defined as follows. An environment is a function ξ : V → N that interprets a given variable as a timestamp. A timed state sequence ρ = (σ, τ) satisfies a TPTLB+P formula φ at position i ≥ 0, under the environment ξ, written ρi |=ξ φ, if and only if:

• ρi |=ξ p iff p ∈ σi;
• ρi |=ξ φ1 ∨ φ2 iff either ρi |=ξ φ1 or ρi |=ξ φ2;
• ρi |=ξ ¬φ1 iff ρi ̸|=ξ φ1;
• ρi |=ξ x ≤ y + c iff ξ(x) ≤ ξ(y) + c;
• ρi |=ξ x ≤ c iff ξ(x) ≤ c;
• ρi |=ξ x.φ1 iff ρi |=ξ′ φ1 where ξ ′ = ξ[x ← τi];
• ρi |=ξ Xwφ1 iff τi+1 ≤ τi +w and ρi+1 |=ξ φ1;
• ρi |=ξ φ1 Uw φ2 iff there exists j ≥ i such that:
• (i) τj ≤ τi + w, (ii) ρj |=ξ φ2, and (iii) ρk |=ξ φ1 for all k such that i ≤ k < j;
• ρi |=ξ Ywφ1 iff i > 0, τi ≤ τi-1 +w, and ρi-1 |=ξ φ1;
• ρi |=ξ φ1 Sw φ2 iff there exists j ≤ i such that: (i) τi ≤ τj + w, (ii) ρj |=ξ φ2, and (iii) ρk |=ξ φ1 for all k such that j < k ≤ i;

where ξ ′ = ξ[x ← τi] is the environment that agrees with ξ on each variable but x, where ξ ′ (x) = τi.

A closed formula φ is said to be satisfied by a timed state sequence ρ, written ρ |= φ, if ρ0 |=ξ φ for any ξ.

The logic TPTLB+P, as well as the original TPTL, is an extension of standard LTL with the addition of the freeze quantifier x.φ, which allows one to give a name to the timestamp of the current state. Then, timing constraints can refer back to two states, e.g., named x and y, comparing their timestamps. Thus, TPTL is a sort of metric extension of LTL, combined with some features typical of hybrid logics, but in a way that retains decidability and (relatively) low complexity. Here, in addition, we allow the use of past modalities yesterday and since. Adding them naïvely to TPTL would cause the complexity of the satisfiability problem to become nonelementary [Alur and Henzinger, 1993]. Here, we restrict all temporal modalities (including future ones) to look only as far as w time steps from the current state. An infinite bound w = +∞ is allowed only if the argument formula is closed. This implies that in any timing constraint x ≤ y + c, the timestamps x and y can be distant, at most, an amount of time that is exponential in the size of the formula. Note that TPTLB+P is still an extension of LTL (standard LTL operators are obtained from bounded ones by always using w = +∞), and the bounded operators are expressible in the full TPTL+P by replacing, for instance, a formula Xwφ, with w ̸= +∞, by x.Xy.(y ≤ x+w∧φ). TPTLB+P is thus a guarded fragment of full TPTL+P.

Intuitively, the syntactic restriction imposed in TPTLB+P occurs naturally in the specification of timeline-based problems as defined in Sect. 2. As an example, consider the rule:

The involved token names can be partitioned into two components, namely, {a, b, c} and {d, e}, such that in both of them each element is related to the others. Since each atom provides an upper bound on the distance of the corresponding token endpoints, they can span an amount of time that is bounded by the sum of all the coefficients involved in the atoms of the component.

Definition 9. Let P = (SV, S) be a timeline-based planning problem, R ∈ S be a synchronization rule, and E be an existential statement of R. Let ΣE be the subset of token names used in E and GE = (ΣE,E) be an undirected graph such that (a, b) ∈ E iff E contains an atom a ≤e1,e2 l,u b. A component Γ of E is a maximal subset of ΣE whose elements are vertices of a connected component of GE .

Definition 10. Let P = (SV, S) be a timeline-based planning problem. The window of the problemWP is the product of all the non-zero coefficients appearing in the problem as duration bounds of tokens (Dx function of any variable x) or as bounds of atoms of any synchronization rules.

Intuitively, WP is a very weak, but correct, upper bound on how far away a component of an existential statement can look from any of its elements. In [Gigante et al., 2016], this observation led to a doubly exponential upper bound to the size of the solution, which was exploited to devise an exponential-space decision procedure. Here, it allows us to provide a TPTLB+P encoding of timeline-based planning problems: each token required by an existential statement is identified by a combination of bounded temporal operators and suitable timing constraints. While a single component can be confined into its exponential-size window, different components can be located arbitrarily far away from each other. For this reason, in [Gigante et al., 2016] we restricted the result to rules with only a single component. Here, we can relax this restriction thanks to the unbounded temporal operators of TPTLB+P: since components are unrelated to each other, they can be described by closed formulae. In what follows, w.l.o.g., we will assume that the names used in each rule of a timeline-based planning problem are unique.

Thus, if P = (SV, S) is a timeline-based planning problem, the equivalent TPTLB+P formula φP is made as follows:

where φ0 ≡ t.(t = 0) states that time starts at timestamp zero, φx encodes the basic facts about each state variable x ∈ SV , and φR encodes the semantics of synchronization rules R ∈ S. For each state variable x ∈ SV , the formula uses two sets of proposition letters: for each value v ∈ Vx, a proposition letter sxv , to mark the start of a token for the variable x where x = v, and a proposition letter ⊥x to mark the end of the timeline for x. A shortcut formula sx ≡ ∨v∈Vx sxv will be used to assert the start of a token for x of any value.

Now, the formula φx that encodes the behavior of a variable x = (Vx, Tx,Dx) ∈ SV is the conjunction of a few axioms, including the following: (1) at most one token starts at a given state, (2) the timeline eventually ends, and (3) either a token starts at t = 0 or it is preceded by another one.

These three statements are encoded as follows:

Then, φx has to state that after the start of each token, the end must happen within the bounds required by the Dx function and the following token (if any) must respect the Tx function:

where Dx(v) = (dvmin , dvmax ) and, for all v, x, and t, εxv (t) is the following formula:

which is true if the state at timestamp t was the start of a token for x = v, and the current state is the end of that token.

Note that the end of a token is represented by the start of the following one (or by ⊥x), and an empty token is described by two symbols sx labeling states with the same timestamp.

The last part of φP describes the synchronization rules. Consider the synchronization rule R ≡ a0[x = v0] -→ E1 ∨ . . . ∨ Ek. The formula φR that encodes R has the form:

where the formula φEi encodes the existential statement Ei, as shown in the following.

Let Γ be a component of a given existential statement E and let a1[x1 = v1], . . . , ak[xk = vk] be the quantifiers used in E to introduce the names in Γ. Then, the formula encoding Γ is the following one:

where ∃wφ ≡ FwPwφ and ψΓ encodes the atoms of the component through the conjunction of suitable timing constraints. In φΓ, all the starting and ending endpoints of each token involved in the component are quantified, and their timestamps assigned to variables, respectively tsai and teai for the start and end of the token ai. Thus, in ψΓ, the atoms can be encoded directly. As an example, an atom a1 ≤s,e [3,7] a2 can be encoded as (tea2 ≥ tsa1 + 3) ∧ (tea2 ≤ tsa1 + 7).

Thus, let {Γ1, . . . , Γm} be the components of the existential statement E. At most one of these components, say Γi, contains the name a0 used in the trigger, while the others are independent from it. Thus, the formula φE that encodes E has the following form:

Note that since all the components other than Γi do not mention the trigger, formulae Γj (for j ̸= i) do not have free variables, as all the needed time points are quantified inside, and thus they are allowed to occur inside the unbounded eventually and past operators. Also note that the only free variables in any φE are tsa0 and tea0 , i.e., those referring to the trigger. A trigger-less rule is only determined by the satisfaction of its existential statements. Thus, the formula φR′ for a rule R′ ≡ ⊤ -→ E ′1 ∨ . . . ∨ E ′k is simply φR′ ≡ F ∨ki=1 (φE ′ i ); since R′ has no free variables, it is syntactically well-formed. It can be verified that φP correctly encodes the problem P, and that a solution plan can be effectively extracted from a model of φP .

Theorem 1. Given a timeline-based planning problem P with bounded constraints, there exists a solution plan for P if and only if the TPTLB+P formula φP is satisfiable.

Moreover, it is easy to see that the size of φP is polynomial in the size of P . Note that enumerating all the possible values of a variable, e.g., in sx , is permitted, since |Vx| ∈ O(|P|), as the values are already enumerated extensionally in the input representation of P to specify the Tx and Dx functions.

4 Complexity of TPTLB+P

We now show that, given a closed TPTLB+P formula φ, deciding whether φ has a model is EXPSPACE-complete. Hardness comes from the encoding shown in Sect. 3, and the complexity result from [Gigante et al., 2016], thus here we only provide an exponential-space decision procedure. We start with some notation. Let n = |φ| be the length of φ, and m be the number of temporal modalities of φ with a finite bound, with {w1, . . . , wm} the set of all such finite bounds. Among those, let w0 = max{wi | 1 ≤ i ≤ m} be the maximum one, and let W = w0 · (m+ 1). Similarly, let ∆ = ∏i |ci| for all the finite and non-zero coefficients ci appearing in timing constraints of the formula, e.g., in x ≤ y+c. Note that, since coefficients are succinctly encoded, the size of both ∆ and W is exponential in n.

W.l.o.g., hereafter we restrict ourselves to formulae without absolute timing constraints of the type x ≤ c. To show that the problem can be solved in exponential space, we outline a tableau-based decision procedure based on the tableau for TPTL outlined in Alur and Henzinger [1994], which in turn exploits ideas very similar to those of classic tableau systems for LTL [Manna and Pnueli, 1995; Lichtenstein and Pnueli, 2000]: a graph is built, where each node represents a possible state of a model, and then a model is searched among the infinite paths of this graph. In contrast to the usual LTL tableaux, however, a tableau for TPTL and TPTLB+P has also to keep track, in addition to the truth assignment of any given node, of how much time has to pass between two different states, and handle the freeze quantifications accordingly. The key ingredient is the following.

Definition 11. Consider a TPTLB+P formula x.ψ and δ ∈ Z. Then, the formula x.ψδ is obtained from x.ψ in two steps:

1. one first replaces all the subformulae of the forms x ≤ y + c and y ≤ x + c by, respectively, x ≤ y + (c + δ) and y ≤ x + (c - δ);
2. then, all the subformulae of the forms x ≤ y + c and y ≤ x + c are replaced by ⊤ (resp., ⊥) if c > W (resp., c < -W).

Intuitively, x.ψδ is a time-shifted version of x.ψ where x is mapped to x - δ, in such a way that x.ψδ holds at time τ if and only if ψ holds at τ - δ.

As in classic tableaux, the nodes are sets of formulae drawn from the closure set of φ, which contains all the formulae needed to assess the truth of φ over a model.

Definition 12. Given a closed TPTLB+P formula φ of the form x.φ′ , the closure of φ is the smallest set of formulae C(φ) containing x.φ′ such that:

• if x.(ψ1 ∨ ψ2) ∈ C(φ), then {x.ψ1, x.ψ2} ⊆ C(φ),
• if x.Xwψ ∈ C(φ), then {x.ψδ | δ ∈ N} ⊆ C(φ),
• if x.Ywψ ∈ C(φ), then {x.ψ-δ | δ ∈ N} ⊆ C(φ),
• if x.(ψ1 Uw ψ2) ∈ C(φ), then x.ψ1, x.ψ2, and x.Xw(ψ1 Uw-δ ψ2), for all δ ≤ w, belong to C(φ),
• if x.(ψ1 Sw ψ2) ∈ C(φ), then x.ψ1, x.ψ2, and x.Yw(ψ1 Sw-δ ψ2), for all δ ≤ w, belong to C(φ),
• if x.z.ψ ∈ C(φ), then x.ψ[z/x] ∈ C(φ),

where w - δ = w if w = +∞ and ψ[z/x] is obtained from ψ by replacing every free occurrence of z with x.

Note that, w.l.o.g., we can restrict our attention to formulae φ of the form x.φ′ and observe that C(φ) only contains closed formulae of the form z.ψ, for some variable z. As one may see, the definition of the closure of φ is very similar to that given for TPTL by Alur and Henzinger [1994], but it differs in the handling of the bounds in the temporal operators Uw and Sw, which are decremented by the suitable amount at each expansion. Another crucial difference is the definition of x.ψδ (Definition 11), which has to deal with shifts in both directions. Note that the closure of x.Xwψ (resp., x.Ywψ) seems to generate an infinite number of formulae x.ψδ , for all δ ∈ N, but this is not the case. In the case of TPTL, one may assume that in a closed formula of the form x.ψ, any other variable y that occurs in ψ is instantiated only at a timestamp later than x. This fact ensures that the closure set remains finite, since, for instance, any formula of the form x ≤ y+c can be replaced by ⊤ for any c. Here, however, since ψ may use past operators, this argument does not work, and the closure set is at risk of becoming infinite. Nevertheless, we ensure its finiteness by replacing with ⊤ or ⊥ any formula x ≤ y + c where c goes respectively above W or below -W. This replacement is sound thanks to the restriction that unbounded temporal operators may only be used with closed formulae, which guarantees that the value of any x and y used in a timing constraint can only differ as much as W. In addition, we can bound the size of the closure set which, as in the TPTL case, is exponential in the size of the formula. Thus, the following two results can be proved.

Lemma 1. Let ρ = (σ, τ) be a timed state sequence and ξ be an environment. Consider a position i ≥ 0 and δ ∈ Z such that δ ≤ τi. Then, for any formula x.ψ ∈ C(φ):

Lemma 2. Let φ be a TPTLB+P formula. Then,

We now show how the tableau for φ is built. To this end, let C ∗ (φ) = C(φ) ∪ {Prevδ | 0 ≤ δ ≤ ∆} ∪ {Succγ | 0 ≤ γ ≤ ∆} be an extension of the closure set of φ with fresh proposition letters Prevδ and Succγ, which keep track of the time between the current state and, respectively, the previous and the next one. Note that we consider only time steps up to ∆, since, as the TPTL case, we can restrict ourselves to timed state sequences where τi - τi-1 < ∆ for all i > 0.

Definition 13 (Atoms for φ). An atom for φ is a maximal subset Φ of C ∗ (φ) such that:

• Prevδ ∈ Φ and Succγ ∈ Φ for exactly one δ and exactly one γ between 0 and ∆. Such δ and γ will be denoted respectively as δΦ and γΦ, and, for i ≤ j, we let δΦi,Φj = ∑i<k≤j δΦk .
• x.(x ≤ x + c) ∈ Φ iff c ≥ 0,
• x.z.ψ ∈ Φ iff x.ψ[z/x] ∈ Φ,
• x.¬φ ∈ Φ iff x.φ ̸∈ Φ,
• x.(φ1 ∨ φ2) ∈ Φ iff either x.φ1 ∈ Φ or x.φ2 ∈ Φ,
• x.(φ1 Uw φ2) ∈ Φ iff either x.φ2 ∈ Φ or both x.φ1 ∈ Φ and x.Xw(φ1 Uw-γΦ φ2) ∈ Φ,
• x.(φ1 Sw φ2) ∈ Φ iff either x.φ2 ∈ Φ or both x.φ1 ∈ Φ and x.Yw(φ1 Sw-δΦ φ2) ∈ Φ.

Definition 14 (Tableau for φ). The tableau for φ is a graph where the nodes are all the possible atoms for φ and there is an edge between Φ and Ψ iff the following conditions hold:

1. γΦ = δΨ;
2. z.Xwψ ∈ Φ iff γΦ ≤ w and z.ψγΦ ∈ Ψ;
3. z.Ywψ ∈ Ψ iff δΨ ≤ w and z.ψ-δΨ ∈ Φ.

Conditions 2 and 3 above handle the temporal operators tomorrow and yesterday, by ensuring that whenever there is an edge between two atoms, the formulae requested by temporal operators in the two atoms are present. Intuitively, this is also the point where the tableau handles the binding of variables without explicitly keeping track of any environment, by pushing the freeze quantification to the next state while shifting the formula to preserve the semantics, thanks to Lemma 1. Then, as in the tableaux for LTL and TPTL, the search for a model for φ is reduced to the search for a particular infinite path.

Definition 15. Given the tableau for φ, a φ-path is an infinite path Φ = 〈Φ0, Φ1, . . .〉 of atoms from the tableau such that:

1. φ ∈ Φ0,
2. No formulae of the form x.Ywψ belong to Φ0,
3. δΦi > 0 for infinitely many i ≥ 0,
4. for all i ≥ 0 and all x.(φ1 Uw φ2) ∈ Φi, there is k ≥ i such that δΦi,Φk ≤ w, and both x.φδΦi,Φk 2 ∈ Φk and x.φδΦi ,Φj 1 ∈ Φj for all j with i ≤ j < k, and
5. for all i ≥ 0 and all x.(φ1 Sw φ2) ∈ Φi, there is k ≤ i such that δΦk,Φi ≤ w, and both x.φδΦk,Φi 2 ∈ Φk and x.φδΦj ,Φi 1 ∈ Φj for all j with k < j ≤ i.

Intuitively, a φ-path contains all the necessary pieces of information to build a model for the formula. Each atom corresponds to a state of the model, and its elements are the formulae (in particular, the proposition letters) that will be true in that state. The timestamps of each state can be derived from δΦ0 + δΦ0,Φi for each i. Vice versa, given a model we can build a φ-path by simply listing in each atom all the formulae from the closure set that are true in each state. In verifying these claims, both directions of Lemma 1 play a crucial role, and conditions 4 and 5 of Definition 15 ensure its applicability. The decision of the satisfiability of φ can thus be reduced to the search for a φ-path into the tableau (see Lemma 3).

Lemma 3 (Correctness and Completeness). A TPTLB+P formula φ is satisfiable if and only if its tableau has a φ-path.

The search for a φ-path is non-trivial since there might be an infinite number of them. However, as in the TPTL case, we can restrict the search to periodic φ-paths of bounded length.

Lemma 4. Let φ be a TPTLB+P formula and let m be the number of nodes of the tableau for φ. If the tableau contains a φ-path, then it contains a periodic φ-path of the form Φ0Φ1 . . . Φi(Φi+1 . . . Φl)ω , for i, l ∈ O(m · n · W · ∆).

Observe that the number m of nodes in the tableau is at most 2|C(φ)| , that is, doubly exponential in the size of the formula, by Lemma 2. Looking for a doubly exponentially long φ-path can be done without constructing the whole graph, in singly exponential space as in other LTL and TPTL tableau systems [Manna and Pnueli, 1995; Alur and Henzinger, 1994].

Theorem 2. Given a TPTLB+P formula φ, the problem of deciding whether φ is satisfiable is EXPSPACE-complete.

5 Conclusions

The present paper provides a logical characterization of the fragment of non-flexible timeline-based planning studied in [Gigante et al., 2016], showing that it can be captured by TPTLB+P, a particular guarded fragment of TPTL augmented with past modalities. Thanks to the encoding shown in [Gigante et al., 2016], the result directly transfers to actionbased temporal planning, which thus can also be captured by TPTLB+P (a different logical characterization of temporal planning has been recently given in terms of LTLRA in [Cimatti et al., 2017]). The proposed logic has been shown to be EXPSPACE-complete by adapting the original tableau-based decision procedure for TPTL. The encoding of timeline-based planning problems into TPTLB+P provided in Sect. 3 turned out to be very natural, and shows how unbounded interval relations affect the expressive power of the formalisms. In usual settings (see e.g., [Cialdea Mayer et al., 2016]), where timeline-based planning problems are given with a bound on the solution horizon, allowing for unbounded interval relations do not increase the expressive power (action-based temporal planning cannot be captured in those settings). On the contrary, enriching our setting with unbounded interval relations would result in increased expressive power, as we do not impose bounds on the horizon. Unfortunately, a naïve adaptation of our encoding into TPTLB+P is feasible but results in exponentially-sized formulae. The problem of finding a polynomial encoding is under investigation.