The present work focuses on timeline-based planning over dense temporal domains. In automated planning, the temporal domain is commonly assumed to be discrete, the dense case being dealt with by resorting to some form of discretization. In the last years, the planning problem over dense temporal domains has been nally addressed both in the timeline-based setting and, very recently, in the action-based one. Dense timeline-based planning, in its full generality, has been shown to be undecidable. Decidability has been recovered by imposing suitable syntactic and/or semantic restrictions (the complexity of decidable fragments varies a lot, spanning from non-primitive recursive hardness to NP-completeness, passing through EXPSPACE- and PSPACEcompleteness). In this paper, we proved that restricting to the future fragment is not enough to get decidability.
The present contribution adds an important piece to the general picture of timeline-based planning over dense temporal domains by showing that restricting to the future fragment is not enough to get decidability.
Inspired by classical control theory, timeline-based planning has emerged as a viable alternative to the more common action-based approach to planning. Action-based planning aims at determining a sequence of actions that, given the initial state of the world and a goal, lead to a state where the goal is met. Timeline-based planning looks at the problem more abstractly, focusing on what has to happen to meet the goal instead of what an agent has to do to reach it.
In timeline-based planning, planning domains are described as collections of independent, but interacting, components, each one consisting of a set of state variables. The evolution of the values of state variables over time is modeled by ? Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). means of a set of timelines (sequences of tokens), and it is governed by a set of transition functions, one for each state variable, and a set of synchronization rules, that constrain the temporal relations among state variables.
The temporal domain is commonly assumed to be discrete, the dense case being dealt with by forcing a more or less arti cial discretization of the domain.
In [
Even though the potentialities of automated planning over dense time, in terms of both naturalness and expressiveness, are commonly recognized, its systematic investigation has been undertaken only very recently.
The computational complexity of action-based temporal planning, as
represented by PDDL 2.1, over dense time has been addressed in [
TP over dense time has been studied in depth in [
A rst restriction that can be imposed on trigger rules is that the name of
a non-trigger token appears exactly once in the body (interval atoms ) of the
rule (simple trigger rules ). Such a syntactical restriction avoids comparisons of
multiple token time-events with a non-trigger reference time-event. A second
restriction concerns future and past tokens. When a token is \selected" by a
trigger, the synchronization rule allows one to compare tokens of the timelines
both preceding (past) and following (future) the trigger token. One can restrict
the comparison only to tokens in the future with respect to the trigger
(future semantics of trigger rules ). In [
The decidability status of the TP problem with arbitrary trigger rules under
the future semantics was left open in [
The paper is organized as follows. In Section 2, we recall the distinctive features of the TP framework. Then, in Section 3, we prove that future TP is undecidable. Conclusions give a short assessment of the work and outline future research directions. 2
In this section, we provide some notation and background knowledge about
the TP problem. For a systematic account of expressiveness and complexity
of timeline-based planning, including a careful analysis of the way in which
temporal uncertainty and nondeterminism are dealt with, we refer the reader
to [
Let N be the set of natural numbers, R+ be the set of non-negative real numbers, and Intv be the set of intervals in R+ whose endpoints are in N [ f1g. Moreover, let us denote by Intv (0;1) the set of intervals I 2 Intv such that either I is unbounded, or I is left-closed with left endpoint 0. Such intervals I can be replaced by expressions of the form n for some n 2 N and 2 f<; ; >; g. Let w be a nite word over some alphabet. By jwj we denote the length of w. For all 0 i < jwj, w(i) is the i-th letter of w. 2.1
The TP Problem
In the following, we recall the TP framework as presented in [
De nition 1. A state variable x is a triple x = (Vx; Tx; Dx), where Vx is the nite domain of the variable x, Tx : Vx ! 2Vx is the value transition function, which maps each v 2 Vx to the (possibly empty) set of successor values, and Dx : Vx ! Intv is the constraint function that maps each v 2 Vx to an interval.
A token for a variable x is a pair (v; d) consisting of a value v 2 Vx and a duration d 2 R+ such that d 2 Dx(v). Intuitively, a token for x represents an interval of time where the state variable x takes value v. The behavior of the state variable x is speci ed by means of timelines which are non-empty sequences of tokens = (v0; d0) : : : (vn; dn) consistent with the value transition function
Tx, that is, such that vi+1 2 Tx(vi) for all 0 the end time e( ; i) of the i-th token (0 i
i as follows: e( ; i) = Xdh and s( ; i) = 0 if i = 0, and s( ; i) =
h=0 See Figure 1 for an example. i < n. The start time s( ; i) and n) of the timeline are de ned i 1 Xdh otherwise. h=0 x t = 0 x = a x = b x = c
x = b t = 7 t = 10 t = 13:9
Given a nite set SV of state variables, a multi-timeline of SV is a mapping assigning to each state variable x 2 SV a timeline for x. Multi-timelines of SV can be constrained by a set of synchronization rules, which relate tokens, possibly belonging to di erent timelines, through temporal constraints on the start/end-times of tokens (time-point constraints) and on the di erence between start/end-times of tokens (interval constraints). The synchronization rules exploit an alphabet of token names to refer to the tokens along a multi-timeline, and are based on the notions of atom and existential statement. De nition 2. An atom is either a clause of the form o1 Ie1;e2 o2 ( interval atom), or of the forms o1 Ie1 n or n Ie1 o1 ( time-point atom), where o1; o2 2 , I 2 Intv , n 2 N, and e1; e2 2 fs; eg.
An atom is evaluated with respect to a -assignment for a given multitimeline which is a mapping assigning to each token name o 2 a pair (o) = ( ; i) such that is a timeline of and 0 i < j j is a position along (intuitively, ( ; i) represents the token of referenced by the name o). An interval atom o1 Ie1;e2 o2 is satis ed by if e2( (o2)) e1( (o1)) 2 I. A point atom o Ie n (resp., n Ie o) is satis ed by if n e( (o)) 2 I (resp., e( (o)) n 2 I).
De nition 3. An existential statement E for a nite set SV of state variables is a statement of the form:
E := 9o1[x1 = v1] 9on[xn = vn]:C where C is a conjunction of atoms, oi 2 , xi 2 SV , and vi 2 Vxi for each i = 1; : : : ; n. The elements oi[xi = vi] are called quanti ers. A token name used in C, but not occurring in any quanti er, is said to be free. Given a assignment for a multi-timeline of SV , we say that is consistent with the existential statement E if for each quanti ed token name oi, (oi) = ( ; h) where = (xi) and the h-th token of has value vi. A multi-timeline of SV satis es E if there exists a -assignment for consistent with E such that each atom in C is satis ed by .
De nition 4. A synchronization rule R for a nite set SV of state variables is a rule of one of the forms o0[x0 = v0] ! E1 _ E2 _ : : : _ Ek; > ! E1 _ E2 _ : : : _ Ek; where o0 2 , x0 2 SV , v0 2 Vx0 , and E1; : : : ; Ek are existential statements. In rules of the rst form ( trigger rules), the quanti er o0[x0 = v0] is called trigger, and we require that only o0 may appear free in Ei (for i = 1; : : : ; n). In rules of the second form ( trigger-less rules), we require that no token name appears free. A trigger rule R is simple if for each existential statement E of R and each token name o distinct from the trigger, there is at most one interval atom of E where o occurs.
Intuitively, a trigger o0[x0 = v0] acts as a universal quanti er, which states that for all the tokens of the timeline for the state variable x0, where the variable x0 takes the value v0, at least one of the existential statements Ei must be true. Trigger-less rules simply assert the satisfaction of some existential statement. The intuitive meaning of the simple trigger rules is that they disallow simultaneous comparisons of multiple time-events (start/end times of tokens) with a nontrigger reference time-event. The semantics of synchronization rules is formally de ned as follows.
De nition 5. Let be a multi-timeline of a set SV of state variables. Given a trigger-less rule R of SV , satis es R if satis es some existential statement of R. Given a trigger rule R of SV with trigger o0[x0 = v0], satis es R if for every position i of the timeline (x0) for x0 such that (x0) = (v0; d), there is an existential statement E of R and a -assignment for which is consistent with E such that (o0) = ( (x0); i) and satis es all the atoms of E .
In the paper, we focus on a stronger notion of satisfaction of trigger rules, called satisfaction under the future semantics. It requires that all the non-trigger selected tokens do not start strictly before the start-time of the trigger token. De nition 6. A multi-timeline of SV satis es under the future semantics a trigger rule R = o0[x0 = v0] ! E1 _ E2 _ : : : _ Ek if satis es the trigger rule obtained from R by replacing each e9xoisnt[exnnti=al vsnt]a:Ctem^eVnint=1Eio0= [90;o+11[x[1 i= v1] 9on[xn = vn]:C with 9o1[x1 = v1] s;s o .
A TP domain P = (SV; R) is speci ed by a nite set SV of state variables and a nite set R of synchronization rules modeling their admissible behaviors. Trigger-less rules can be used to express initial conditions and the goals of the problem, while trigger rules are useful to specify invariants and response requirements. A plan of P is a multi-timeline of SV satisfying all the rules in R. A future plan of P is de ned in a similar way, but we require that the ful llment of the trigger rules is under the future semantics. We are interested in the following decision problems: (i) TP problem: given a TP domain P = (SV; R), is there a plan for P ? (ii) Future TP problem: similar to the previous one, but we require the existence of a future plan. 3
In this section, we establish the following result.
Theorem 1. Future TP with one state variable is undecidable even if the intervals are in Intv (0;1).
Theorem 1 is proved by a polynomial-time reduction from the halting problem
for Minsky 2-counter machines [
We adopt the following notational conventions. For an instruction op = ( ; c) 2 L, let c(op) := c 2 f1; 2g be the counter associated with op. For a transition 2 of the form = (q; op; q0), we de ne from( ) := q, op( ) := op, c( ) := c(op), and to( ) := q0. Without loss of generality, we make these assumptions: { for each transition 2 , from( ) 6= qhalt and to( ) 6= qinit, and { there is exactly one transition in , denoted init, having as source the initial location qinit.
An M -con guration is a pair (q; ) consisting of a location q 2 Q and a counter valuation : f1; 2g ! N. M induces a transition relation, denoted by !, over pairs of M -con gurations de ned as follows. For con gurations (q; ) and (q0; 0), (q; ) ! (q0; 0) if for some instruction op 2 L, (q; op; q0) 2 and the following holds, where c 2 f1; 2g is the counter associated with the instruction op: (i) 0(c0) = (c0) if c0 6= c; (ii) 0(c) = (c) + 1 if op = (inc; c); (iii) 0(c) = (c) 1 if op = (dec; c) (in particular, it has to be (c) > 0); and (iv) 0(c) = (c) = 0 if op = (zero; c).
A computation of M is a non-empty nite sequence C1; : : : ; Ck of con
gurations such that Ci ! Ci+1 for all 1 i < k. M halts if there is a computation
starting at the initial con guration (qinit; init), where init(1) = init(2) = 0,
and leading to some halting con guration (qhalt; ). The halting problem is to
decide whether a given machine M halts, and it is was proved to be undecidable [
For c 2 f1; 2g, a c-code for the main value 2 is a nite word wc over Vsec of the form ( ; c; beg) ( ; c; #)h ( ; c; end) for some h 0 such that h = 0 if op( ) = (zero; c). The c-code wc encodes the value for counter c given by h (or equivalently jwcj 2). Note that only the occurrences of the symbols ( ; c; #) encode units in the value of counter c, while the symbol ( ; c; beg) (resp., ( ; c; end)) is only used as left (resp., right) marker in the encoding.
A con guration-code w for a main value 2 is a nite word over V of the form w = w1 w2 such that for each counter c 2 f1; 2g, wc is a c-code for the main value . The con guration-code w encodes the M -con guration (from( ); ), where (c) = jwcj 2 for all c 2 f1; 2g. Note that if op( ) = (zero; c), then (c) = 0.
A computation-code is a non-empty sequence of con guration-codes = w 1 w k , where for all 1 i k, w i is a con guration-code with main value i, and whenever i < k, it holds that to( i) = from( i+1). Note that by our assumptions to( i) 6= qhalt for all 1 i < k, and j 6= init for all 1 < j k. The computation-code is initial if the rst con guration-code w 1 has the main value init and encodes the initial con guration, and it is halting if for the last con guration-code w k in , it holds that to( k) = qhalt. For all 1 i k, let (qi; i) be the M -con guration encoded by the con guration-code w i and ci = c( i). The computation-code is well-formed if, additionally, for all 1 j < k, the following holds: { j+1(c) = j (c) if either c 6= cj or op( j ) = (zero; cj ) (equality requirement ); { j+1(cj ) = j (cj ) + 1 if op( j ) = (inc; cj ) (increment requirement ); { j+1(cj ) = j (cj ) 1 if op( j ) = (dec; cj ) (decrement requirement ). Clearly, M halts i there exists an initial and halting well-formed computationcode.
De nition of xM and RM . We now de ne a state variable xM and a set RM of synchronization rules for xM with intervals in Intv (0;1) such that the untimed part of every future plan of P = (fxM g; RM ) is an initial and halting well-formed computation-code. Thus, M halts if and only if there is a future plan of P .
Formally, variable xM is given by xM = (V = Vmain [ Vsec; T; D), where for each v 2 V , D(v) =]0; 1[. Thus, we require that the duration of a token is always greater than zero (strict time monotonicity ). The value transition function T of xM ensures the following property.
Claim. The untimed parts of the timelines for xM whose rst token has value init correspond to the pre xes of initial computation-codes. Moreover, init 2= T (v) for all v 2 V .
By construction, it is a trivial task to de ne T so that the previous requirement is ful lled.
Let Vhalt = f 2 j to( ) = qhaltg. By Claim 3 and the assumption that from( ) 6= qhalt for each transition 2 , in order to enforce the initialization and halting requirements, it su ces to ensure that a timeline has a token with value init and a token with value in Vhalt. This is captured by the trigger-less rules > ! 9o[xM = init]:> and > ! Wv2Vhalt 9o[xM = v]:>.
Finally, the crucial well-formedness requirement is captured by the trigger rules in RM which express punctual time constraints3. We refer the reader to Figure 2, that gives an intuition on the properties enforced by the rules we are about to de ne. In particular, we essentially take advantage of the dense temporal domain to allow for the encoding of arbitrarily large values of counters in two time units.
w (;1;beg) (;2;beg) (;2;# ) (;2;end) 0 ( 0;1;beg) ( 0;1;#) ( ;01;end)
( 0;2;beg) = 1 = 1 ( 0;1;#) ( 0;2;#) ( ;02;enwd)0 = 1 3 Such punctual constrains are expressed by pairs of conjoined atoms whose intervals are in Intv (0;1). Trigger rules for 1-Time distance between consecutive main values. We de ne non-simple trigger rules requiring that the overall duration of the sequence of tokens corresponding to a con guration-code amounts exactly to two time units. By Claim 3, strict time monotonicity, and the halting requirement, it su ces to ensure that each token tk having a main value in Vmain n Vhalt is eventually followed by a token tk0 such that tk0 has a main value and s(tk0) s(tk) = 1 (this denotes|with a little abuse of notation|that the di erence of start times is exactly 1). To this aim, for each v 2 Vmain n Vhalt, we write the non-simple trigger rule with intervals in Intv (0;1):
_ u2Vmain o[xM = v] ! Trigger rules for the equality requirement. In order to ensure the equality requirement, we exploit the fact that the end time of a token along a timeline corresponds to the start time of the next token (if any). Let Vs=ec be the set of secondary states ( ; c; t) 2 Vsec such that to( ) 6= qhalt, and either c 6= c( ) or op( ) = (zero; c). Moreover, for a counter c 2 f1; 2g and a tag t 2 fbeg; #; endg, let Vct Vsec be the set of secondary states given by fcg ftg. We require the following: (*) each token tk with a (Vct \ Vs=ec)-value is eventually followed by a token tk0 with a Vct-value such that s(tk0) s(tk) = 1 (i.e., the di erence of start times is exactly 1). Moreover, if t 6= end, then e(tk0) e(tk) = 1 (i.e., the di erence of end times is exactly 1).
Condition (*) is captured by the following non-simple trigger rules with intervals in Intv (0;1): { for each v 2 Vct \ Vs=ec and t 6= end,
o[xM = v] ! Wu2Vct 9o0[xM = u]: o s;s [1;+1[ o0 ^ o s;s [0;1] o0 ^ o e;e [1;+1[ o0 ^ o e;e [0;1] o0; { for each v 2 Vcend \ Vs=ec, o[xM = v] !
_ u2Vcend 9o0[xM = u]: o s;s [1;+1[ o0 ^ o s;s [0;1] o0:
We now show that Condition (*) together with strict time monotonicity and 1-Time distance between consecutive main values ensure the equality requirement. Let be a timeline of xM satisfying all the rules de ned so far, w and w 0 two adjacent con guration-codes along with w preceding w 0 (note that to( ) 6= qhalt), and c 2 f1; 2g a counter such that either c 6= c( ) or op( ) = (zero; c). Let tk0 tk`+1 (resp., tk00 tk`00+1) be the sequence of tokens associated with the c-code of w (resp., w 0 ). We need to show that ` = `0. By construction tk0 and tk00 have value in Vcbeg, tk`+1 and tk`00+1 have value in Vcend, and for all 1 i ` (resp., 1 i0 `0), tki has value in Vc# (resp., tki00 has value in Vc#). Then strict time monotonicity, 1-Time distance between consecutive main values, and Condition (*) guarantee the existence of an injective mapping g : ftk0; : : : ; tk`+1g ! ftk00; : : : ; tk`00+1g such that g(tk0) = tk00, g(tk`+1) = tk`00+1, and for all 0 i `, if g(tki) = tkj0 (note that j < `0 + 1), then g(tki+1) = tkj0+1 (we recall that the end time of a token is equal to the start time of the next token along a timeline, if any). These properties ensure that g is surjective as well. Hence, g is a bijection and `0 = `.
Trigger rules for the increment requirement. Let Vsiencc be the set of secondary states ( ; c; t) 2 Vsec such that to( ) 6= qhalt and op( ) = (inc; c). By reasoning like in the case of the rules ensuring the equality requirement, in order to express the increment requirement, it su ces to enforce the following conditions for each counter c 2 f1; 2g: (i) each token tk with a (Vcbeg \Vsiencc)-value is eventually followed by a token tk0 with a Vcbeg-value such that e(tk0) s(tk) = 1 (i.e., the di erence between the end time of token tk0 and the start time of token tk is exactly 1); (ii) for each t 2 fbeg; #g, each token tk with a (Vct \ Vsiencc)-value is eventually followed by a token tk0 with a Vc#-value such that s(tk0) s(tk) = 1 and e(tk0) e(tk) = 1 (i.e., the di erence of start times and end times is exactly 1). Observe that the token with a (Vcbeg \ Vsiencc)-value is associated with a token with Vc#-value anyway; (iii) each token tk with a (Vcend \ Vsiencc)-value is eventually followed by a token tk0 with a Vcend-value such that s(tk0) s(tk) = 1 (i.e., the di erence of start times is exactly 1); Intuitively, if w and w0 are two adjacent con guration-codes along a timeline of xM , with w preceding w0, (i) and (ii) force a token tk0 with a Vc#-value in w0 to \take the place" of the token tk with (Vcbeg \ Vsiencc)-value in w (i.e., they have the same start and end times). Moreover a token with Vcbeg-value must immediately precede tk0 in w0.
These requirements can be expressed by non-simple trigger rules with intervals in Intv (0;1) similar to the ones de ned for the equality requirement. Trigger rules for the decrement requirement. For capturing the decrement requirement, it su ces to enforce the following conditions for each counter c 2 f1; 2g, where Vsdeecc denotes the set of secondary states ( ; c; t) 2 Vsec such that to( ) 6= qhalt and op( ) = (dec; c): (i) each token tk with a (Vcbeg \Vsdeecc)-value is eventually followed by a token tk0 with a Vcbeg-value such that s(tk0) e(tk) = 1 (i.e., the di erence between the start time of token tk0 and the end time of token tk is exactly 1); (ii) each token tk with a (Vc# \ Vsdeecc)-value is eventually followed by a token tk0 with a Vct-value where t 2 fbeg; #g such that s(tk0) s(tk) = 1 and e(tk0) e(tk) = 1 (i.e., the di erence of start times and end times is exactly 1). (iii) each token tk with a (Vcend \ Vsdeecc)-value is eventually followed by a token tk0 with a Vcend-value such that s(tk0) s(tk) = 1 (i.e., the di erence of start times is exactly 1); Analogously, (i) and (ii) produce an e ect which is symmetric w.r.t. the case of increment.
Again, these requirements can be easily expressed by non-simple trigger rules with intervals in Intv (0;1) as done before for expressing the equality requirement.
By construction, the untimed part of a future plan of P = (fxM g; RM ) is an initial and halting well-formed computation-code. Vice versa, by exploiting denseness of the temporal domain, the existence of an initial and halting well-formed computation-code implies the existence of a future plan of P . This concludes the proof of Proposition 1. 4
In this paper, we solved a problem left open in [
We glimpse two directions for future research. On the one hand, we would like to compare expressive power and complexity of action- and timeline-based planning over dense time in a systematic way. On the other hand, we would like to study the e ects of applying to the discrete case the same restrictions we imposed to timeline-based planning over dense time.
We would like to acknowledge the support from the GNCS project Strategic Reasoning and Automatic Synthesis of Multi-Agent Systems.