=Paper=
{{Paper
|id=Vol-2756/paper15
|storemode=property
|title=Undecidability of Future Timeline-based Planning over Dense Temporal Domains?
|pdfUrl=https://ceur-ws.org/Vol-2756/paper_15.pdf
|volume=Vol-2756
|authors=Laura Bozzelli,Alberto Molinari,Angelo Montanari,Adriano Peron
|dblpUrl=https://dblp.org/rec/conf/ictcs/BozzelliMMP20
}}
==Undecidability of Future Timeline-based Planning over Dense Temporal Domains?==
https://ceur-ws.org/Vol-2756/paper_15.pdf
Undecidability of Future Timeline-based
Planning over Dense Temporal Domains?
Laura Bozzelli1 , Alberto Molinari2 , Angelo Montanari2 , and Adriano Peron1
1
University of Napoli “Federico II”, Napoli, Italy
lr.bozzelli@gmail.com; adrperon@unina.it
2
University of Udine, Udine, Italy
molinari.alberto@gmail.com; angelo.montanari@uniud.it
Abstract. 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 finally 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 suit-
able 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 PSPACE-
completeness). In this paper, we proved that restricting to the future
fragment is not enough to get decidability.
Keywords: Automated planning· Timeline-based planning · Dense time
· Decidability.
1 Introduction
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 Com-
mons License Attribution 4.0 International (CC BY 4.0).
2 L. Bozzelli et al.
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 artificial discretization of the domain.
In [4], Gigante et al. showed that (discrete) timeline-based planning (TP for
short) with bounded temporal relations and token durations, and no temporal
horizon, is EXPSPACE-complete and expressive enough to capture action-
based temporal planning. Later, Gigante et al. proved that TP with unbounded
interval relations is still EXPSPACE-complete [5] (if an upper bound to the
temporal horizon is added, the problem becomes NEXPTIME-complete), and
that the same holds for TP with recurrent goals [3].
Even though the potentialities of automated planning over dense time, in
terms of both naturalness and expressiveness, are commonly recognized, its sys-
tematic investigation has been undertaken only very recently.
The computational complexity of action-based temporal planning, as rep-
resented by PDDL 2.1, over dense time has been addressed in [7] (the prob-
lem is known to be EXPSPACE-complete over discrete time). The problem
has been shown to be PSPACE-complete when self-overlap is forbidden (self-
overlap means that actions are allowed to overlap already running instances of
themselves), whereas, when allowed, it becomes EXPSPACE-complete with
-separation (a minimum amount of separation between mutually exclusive
events is guaranteed) and undecidable without -separation (separation is sim-
ply required to be non-zero).
TP over dense time has been studied in depth in [1]. The general problem
has been shown to be undecidable even when a single state variable is used.
Decidability can be recovered by suitably constraining the logical structure of
synchronization rules. In general, synchronization rules allow a universal quan-
tification over the tokens of a timeline (triggers). By disallowing it and retaining
only rules in purely existential form (trigger-less rules), the TP problem becomes
NP-complete. In [1], various intermediate cases have been investigated.
A first 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 (fu-
ture semantics of trigger rules). In [1], it has been shown that the TP problem
restricted to simple trigger rules remains undecidable. Decidability can be re-
covered by adding the future semantics to simple trigger rules: future TP with
simple trigger rules has been proved to be non-primitive recursive-hard. Better
complexity results can be obtained by restricting also the type of intervals used
Undecidability of future timeline-based planning 3
in the simple trigger rules to compare tokens. In particular, future TP with sim-
ple trigger rules without singular intervals (an interval is called singular if it has
the form [a, a], for a ∈ N) is EXPSPACE-complete, PSPACE-complete if one
only allows intervals of the forms [0, a] and [b, +∞[ are considered.
The decidability status of the TP problem with arbitrary trigger rules under
the future semantics was left open in [1] (it was only shown that it is at least
non-primitive recursive even under the assumption that the intervals in the rules
have the forms [0, a] and [b, +∞[). In this paper, we negatively answer the open
issue: future TP over dense time is undecidable.
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 Preliminaries
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 [6] and follow-up publications.
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 ∪ {∞}.
Moreover, let us denote by Intv (0,∞) the set of intervals I ∈ 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 ∈ N and ∼∈ {<, ≤, >, ≥}.
Let w be a finite word over some alphabet. By |w| we denote the length of w.
For all 0 ≤ i < |w|, 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 [2, 4]. In TP, domain
knowledge is encoded by a set of state variables, whose behaviour over time is
described by transition functions and synchronization rules.
Definition 1. A state variable x is a triple x = (Vx , Tx , Dx ), where Vx is the
finite domain of the variable x, Tx : Vx → 2Vx is the value transition function,
which maps each v ∈ Vx to the (possibly empty) set of successor values, and
Dx : Vx → Intv is the constraint function that maps each v ∈ Vx to an interval.
A token for a variable x is a pair (v, d) consisting of a value v ∈ Vx and a
duration d ∈ R+ such that d ∈ 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 specified by means of timelines which are non-empty sequences
of tokens π = (v0 , d0 ) . . . (vn , dn ) consistent with the value transition function
4 L. Bozzelli et al.
Tx , that is, such that vi+1 ∈ Tx (vi ) for all 0 ≤ i < n. The start time s(π, i) and
the end time e(π, i) of the i-th token (0 ≤ i ≤ n) of the timeline π are defined
Xi i−1
X
as follows: e(π, i) = dh and s(π, i) = 0 if i = 0, and s(π, i) = dh otherwise.
h=0 h=0
See Figure 1 for an example.
x=a x=b x=c x=b
x
t =0 t =7 t = 10 t = 13.9
Fig. 1. An example of timeline (a, 7)(b, 3)(c, 3.9) · · · for the state variable x =
(Vx , Tx , Dx ), where Vx = {a, b, c, . . .}, b ∈ Tx (a), c ∈ Tx (b), b ∈ Tx (c). . . and
Dx (a) = [5, 8], Dx (b) = [1, 4], Dx (c) = [2, ∞[. . .
Given a finite set SV of state variables, a multi-timeline of SV is a mapping
Π assigning to each state variable x ∈ SV a timeline for x. Multi-timelines of
SV can be constrained by a set of synchronization rules, which relate tokens,
possibly belonging to different timelines, through temporal constraints on the
start/end-times of tokens (time-point constraints) and on the difference between
start/end-times of tokens (interval constraints). The synchronization rules ex-
ploit 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.
Definition 2. An atom is either a clause of the form o1 ≤Ie1 ,e2 o2 ( interval
atom), or of the forms o1 ≤eI1 n or n ≤eI1 o1 ( time-point atom), where o1 , o2 ∈
Σ, I ∈ Intv , n ∈ N, and e1 , e2 ∈ {s, e}.
An atom ρ is evaluated with respect to a Σ-assignment λΠ for a given multi-
timeline Π which is a mapping assigning to each token name o ∈ Σ a pair
λΠ (o) = (π, i) such that π is a timeline of Π and 0 ≤ i < |π| is a position along
π (intuitively, (π, i) represents the token of Π referenced by the name o). An
interval atom o1 ≤eI1 ,e2 o2 is satisfied by λΠ if e2 (λΠ (o2 )) − e1 (λΠ (o1 )) ∈ I. A
point atom o ≤eI n (resp., n ≤eI o) is satisfied by λΠ if n − e(λΠ (o)) ∈ I (resp.,
e(λΠ (o)) − n ∈ I).
Definition 3. An existential statement E for a finite set SV of state variables
is a statement of the form:
E := ∃o1 [x1 = v1 ] · · · ∃on [xn = vn ].C
where C is a conjunction of atoms, oi ∈ Σ, xi ∈ SV , and vi ∈ Vxi for each
i = 1, . . . , n. The elements oi [xi = vi ] are called quantifiers. A token name
used in C, but not occurring in any quantifier, is said to be free. Given a Σ-
assignment λΠ for a multi-timeline Π of SV , we say that λΠ is consistent with
Undecidability of future timeline-based planning 5
the existential statement E if for each quantified token name oi , λΠ (oi ) = (π, h)
where π = Π(xi ) and the h-th token of π has value vi . A multi-timeline Π of
SV satisfies E if there exists a Σ-assignment λΠ for Π consistent with E such
that each atom in C is satisfied by λΠ .
Definition 4. A synchronization rule R for a finite set SV of state variables is
a rule of one of the forms
o0 [x0 = v0 ] → E1 ∨ E2 ∨ . . . ∨ Ek , > → E1 ∨ E2 ∨ . . . ∨ Ek ,
where o0 ∈ Σ, x0 ∈ SV , v0 ∈ Vx0 , and E1 , . . . , Ek are existential statements. In
rules of the first form ( trigger rules), the quantifier 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 quantifier, 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 non-
trigger reference time-event. The semantics of synchronization rules is formally
defined as follows.
Definition 5. Let Π be a multi-timeline of a set SV of state variables. Given a
trigger-less rule R of SV , Π satisfies R if Π satisfies some existential statement
of R. Given a trigger rule R of SV with trigger o0 [x0 = v0 ], Π satisfies 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 λΠ satisfies 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.
Definition 6. A multi-timeline Π of SV satisfies under the future semantics
a trigger rule R = o0 [x0 = v0 ] → E1 ∨ E2 ∨ . . . ∨ Ek if Π satisfies the trigger
rule obtained from R by replacing each existential statement Vn Ei = ∃o1 [x1 =
v1 ] · · · ∃on [xn = vn ].C with ∃o1 [x1 = v1 ] · · · ∃on [xn = vn ].C ∧ i=1 o0 ≤s,s
[0,+∞[ oi .
A TP domain P = (SV, R) is specified by a finite set SV of state variables
and a finite set R of synchronization rules modeling their admissible behaviors.
Trigger-less rules can be used to express initial conditions and the goals of the
6 L. Bozzelli et al.
problem, while trigger rules are useful to specify invariants and response re-
quirements. A plan of P is a multi-timeline of SV satisfying all the rules in R. A
future plan of P is defined in a similar way, but we require that the fulfillment 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 Undecidability of the future TP problem
In this section, we establish the following result.
Theorem 1. Future TP with one state variable is undecidable even if the in-
tervals are in Intv (0,∞) .
Theorem 1 is proved by a polynomial-time reduction from the halting problem
for Minsky 2-counter machines [8]. Such a machine is a tuple M = (Q, qinit , qhalt ,
∆), where Q is a finite set of (control) locations, qinit ∈ Q is the initial location,
qhalt ∈ Q is the halting location, and ∆ ⊆ Q × L × Q is a transition relation over
the instruction set L = {inc, dec, zero} × {1, 2}.
We adopt the following notational conventions. For an instruction op =
( , c) ∈ L, let c(op) := c ∈ {1, 2} be the counter associated with op. For a
transition δ ∈ ∆ of the form δ = (q, op, q 0 ), we define from(δ) := q, op(δ) := op,
c(δ) := c(op), and to(δ) := q 0 . Without loss of generality, we make these assump-
tions:
– for each transition δ ∈ ∆, 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 -configuration is a pair (q, ν) consisting of a location q ∈ Q and a
counter valuation ν : {1, 2} → N. M induces a transition relation, denoted by
−→, over pairs of M -configurations defined as follows. For configurations (q, ν)
and (q 0 , ν 0 ), (q, ν) −→ (q 0 , ν 0 ) if for some instruction op ∈ L, (q, op, q 0 ) ∈ ∆
and the following holds, where c ∈ {1, 2} 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 finite sequence C1 , . . . , Ck of configura-
tions such that Ci −→ Ci+1 for all 1 ≤ i < k. M halts if there is a computation
starting at the initial configuration (qinit , νinit ), where νinit (1) = νinit (2) = 0,
and leading to some halting configuration (qhalt , ν). The halting problem is to de-
cide whether a given machine M halts, and it is was proved to be undecidable [8].
We prove the following result, from which Theorem 1 directly follows.
Proposition 1. One can construct (in polynomial time) a TP instance (do-
main) P = ({xM }, RM ) where the intervals in P are in Intv (0,∞) such that M
halts iff there exists a future plan for P .
Undecidability of future timeline-based planning 7
Proof. First, we define a suitable encoding of a computation of M as the untimed
part of a timeline (i.e., neglecting tokens’ durations and accounting only for their
values) for xM . For this, we exploit the finite set of symbols V := Vmain ∪ Vsec
corresponding to the finite domain of the state variable xM . The set of main
values Vmain is the set of M -transitions, i.e. Vmain = ∆. The set of secondary
values Vsec is defined as Vsec := ∆ × {1, 2} × {#, beg, end}, where #, beg, and
end are three special symbols used as markers. Intuitively, in the encoding of an
M -computation a main value keeps track of the transition used in the current
step of the computation, while the set Vsec is used for encoding counter values.
For c ∈ {1, 2}, a c-code for the main value δ ∈ ∆ is a finite 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 |wc | − 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 configuration-code w for a main value δ ∈ ∆ is a finite word over V of
the form w = δ · w1 · w2 such that for each counter c ∈ {1, 2}, wc is a c-code
for the main value δ. The configuration-code w encodes the M -configuration
(from(δ), ν), where ν(c) = |wc |−2 for all c ∈ {1, 2}. Note that if op(δ) = (zero, c),
then ν(c) = 0.
A computation-code is a non-empty sequence of configuration-codes π =
wδ1 · · · wδk , where for all 1 ≤ i ≤ k, wδi is a configuration-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 first configuration-code wδ1
has the main value δinit and encodes the initial configuration, and it is halting
if for the last configuration-code wδk in π, it holds that to(δk ) = qhalt . For all
1 ≤ i ≤ k, let (qi , νi ) be the M -configuration encoded by the configuration-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 iff there exists an initial and halting well-formed computation-
code.
Definition of xM and RM . We now define a state variable xM and a set RM of
synchronization rules for xM with intervals in Intv (0,∞) such that the untimed
part of every future plan of P = ({xM }, 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 ∈ V , D(v) =]0, ∞[. 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.
8 L. Bozzelli et al.
Claim. The untimed parts of the timelines for xM whose first token has value
δinit correspond to the prefixes of initial computation-codes. Moreover, δinit ∈
/
T (v) for all v ∈ V .
By construction, it is a trivial task to define T so that the previous require-
ment is fulfilled.
Let Vhalt = {δ ∈ ∆ | to(δ) = qhalt }. By Claim 3 and the assumption that
from(δ) 6= qhalt for each transition δ ∈ ∆, in order to enforce the initialization
and halting requirements, it suffices to ensure that a timeline has a token with
value δinit and a token with value in W Vhalt . This is captured by the trigger-less
rules > → ∃o[xM = δinit ].> and > → v∈Vhalt ∃o[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 define. 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.
=1 =1
=1
w w0
(δ
(δ
(δ
(δ
(δ
(δ
(δ
(δ
(δ
(δ
(δ
(δ,
(δ
0 ,1
0 ,2
0 1,
0 2,
0
,1
,2
0 ,1
0 ,1
,1
,2
,
,
0
,1
,
δ δ
2,
,e
,e
2, #
,b
,b
,b
,b
,#
en
en
,#
,#
#)
nd
nd
eg
eg
eg
eg
d)
d)
)
)
)
)
)
)
)
)
)
)
=1
Fig. 2. The figure shows two adjacent configuration-codes, w (highlighted in cyan)
and w0 (in green), the former for δ = (q, (inc, 1), q 0 ) ∈ ∆ and the latter for δ 0 =
(q 0 , . . . ) ∈ ∆; w encodes the M -configuration (q, ν) where ν(1) = ν(2) = 1, and w0 the
M -configuration (q 0 , ν 0 ) where ν 0 (1) = 2 and ν 0 (1) = 1.
The “1-Time distance between consecutive main values requirement” (represented by
black lines with arrows) forces a token with a main value to be followed, after exactly
one time instant, by another token with a main value.
Since op(δ) = (inc, 1), the value of counter 2 does not change in this computation step,
and thus the values for counter 2 encoded by w and w0 must be equal. To this aim
the “equality requirement” (represented by blue lines with arrows) sets a one-to-one
correspondence between pairs of tokens associated with counter 2 in w and w0 (more
precisely, a token tk with value (δ, 2, ) in w is followed by a token tk0 with value (δ 0 , 2, )
in w0 such that s(tk0 ) − s(tk) = 1 and e(tk0 ) − e(tk) = 1).
Finally, the “increment requirement” (red lines) performs the increment of counter 1
by doing something analogous to the previous case, but with a difference: the token
tk0 with value (δ 0 , 1, #) is in w0 in the place where the token tk with value (δ, 1, beg)
was in w (i.e., s(tk0 ) − s(tk) = 1 and e(tk0 ) − e(tk) = 1). The token tk00 with value
(δ 0 , 1, beg) is “anticipated”, in such a way that e(tk00 ) − s(tk) = 1 (this is denoted by
the dashed red line): the token with main value δ 0 in w0 has a shorter duration than
that with value δ in w, leaving space for tk00 , so as to represent the unit added by δ to
counter 1. Clearly density of the time domain plays a fundamental role here.
3
Such punctual constrains are expressed by pairs of conjoined atoms whose intervals
are in Intv (0,∞) .
Undecidability of future timeline-based planning 9
Trigger rules for 1-Time distance between consecutive main values. We define
non-simple trigger rules requiring that the overall duration of the sequence of
tokens corresponding to a configuration-code amounts exactly to two time units.
By Claim 3, strict time monotonicity, and the halting requirement, it suffices to
ensure that each token tk having a main value in Vmain \ Vhalt is eventually
followed by a token tk 0 such that tk 0 has a main value and s(tk 0 ) − s(tk) = 1
(this denotes—with a little abuse of notation—that the difference of start times
is exactly 1). To this aim, for each v ∈ Vmain \ Vhalt , we write the non-simple
trigger rule with intervals in Intv (0,∞) :
_ s,s
o[xM = v] → ∃o0 [xM = u]. o ≤[1,+∞[ o0 ∧ o ≤s,s 0
[0,1] o .
u∈Vmain
Trigger rules for the equality requirement. In order to ensure the equality re-
quirement, 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 Vsec be the set of
secondary states (δ, c, t) ∈ Vsec such that to(δ) 6= qhalt , and either c 6= c(δ) or
op(δ) = (zero, c). Moreover, for a counter c ∈ {1, 2} and a tag t ∈ {beg, #, end},
let Vct ⊆ Vsec be the set of secondary states given by ∆ × {c} × {t}. We require
the following:
(*) each token tk with a (Vct ∩ Vsec =
)-value is eventually followed by a token tk 0
t 0
with a Vc -value such that s(tk ) − s(tk) = 1 (i.e., the difference of start times
is exactly 1). Moreover, if t 6= end, then e(tk 0 ) − e(tk) = 1 (i.e., the difference
of end times is exactly 1).
Condition (*) is captured by the following non-simple trigger rules with intervals
in Intv (0,∞) :
=
– for each v ∈ Vct ∩ Vsec and t 6= end,
o[xM = v] →
W 0 s,s 0 s,s 0 e,e 0 e,e 0
u∈Vct ∃o [xM = u]. o ≤[1,+∞[ o ∧ o ≤[0,1] o ∧ o ≤[1,+∞[ o ∧ o ≤[0,1] o ;
– for each v ∈ Vcend ∩ Vsec
=
,
_
o[xM = v] → ∃o0 [xM = u]. o ≤s,s 0 s,s 0
[1,+∞[ o ∧ o ≤[0,1] o .
u∈Vcend
We now show that Condition (*) together with strict time monotonicity
and 1-Time distance between consecutive main values ensure the equality re-
quirement. Let π be a timeline of xM satisfying all the rules defined so far,
wδ and wδ0 two adjacent configuration-codes along π with wδ preceding wδ0
(note that to(δ) 6= qhalt ), and c ∈ {1, 2} a counter such that either c 6= c(δ) or
op(δ) = (zero, c). Let tk0 · · · tk`+1 (resp., tk00 · · · tk`0 0 +1 ) be the sequence of to-
kens 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`0 0 +1 have value in
Vcend , and for all 1 ≤ i ≤ ` (resp., 1 ≤ i0 ≤ `0 ), tki has value in Vc# (resp.,
10 L. Bozzelli et al.
tki00 has value in Vc# ). Then strict time monotonicity, 1-Time distance between
consecutive main values, and Condition (*) guarantee the existence of an injec-
tive mapping g : {tk0 , . . . , tk`+1 } → {tk00 , . . . , tk`0 0 +1 } such that g(tk0 ) = tk00 ,
g(tk`+1 ) = tk`0 0 +1 , and for all 0 ≤ i ≤ `, if g(tki ) = tkj0 (note that j < `0 + 1),
0
then g(tki+1 ) = tkj+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 = `.
inc
Trigger rules for the increment requirement. Let Vsec be the set of secondary
states (δ, c, t) ∈ 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 suffices to enforce the following conditions for each
counter c ∈ {1, 2}:
(i) each token tk with a (Vcbeg ∩Vsec inc
)-value is eventually followed by a token tk 0
with a Vc -value such that e(tk 0 ) − s(tk) = 1 (i.e., the difference between
beg
the end time of token tk 0 and the start time of token tk is exactly 1);
(ii) for each t ∈ {beg, #}, each token tk with a (Vct ∩ Vsec inc
)-value is eventually
followed by a token tk with a Vc -value such that s(tk 0 ) − s(tk) = 1 and
0 #
e(tk 0 ) − e(tk) = 1 (i.e., the difference of start times and end times is exactly
1). Observe that the token with a (Vcbeg ∩ Vsec inc
)-value is associated with a
#
token with Vc -value anyway;
(iii) each token tk with a (Vcend ∩ Vsec inc
)-value is eventually followed by a token
tk with a Vc -value such that s(tk 0 ) − s(tk) = 1 (i.e., the difference of
0 end
start times is exactly 1);
Intuitively, if w and w0 are two adjacent configuration-codes along a timeline of
xM , with w preceding w0 , (i) and (ii) force a token tk 0 with a Vc# -value in w0 to
“take the place” of the token tk with (Vcbeg ∩ Vsec inc
)-value in w (i.e., they have the
same start and end times). Moreover a token with Vcbeg -value must immediately
precede tk 0 in w0 .
These requirements can be expressed by non-simple trigger rules with inter-
vals in Intv (0,∞) similar to the ones defined for the equality requirement.
Trigger rules for the decrement requirement. For capturing the decrement re-
quirement, it suffices to enforce the following conditions for each counter c ∈
dec
{1, 2}, where Vsec denotes the set of secondary states (δ, c, t) ∈ Vsec such that
to(δ) 6= qhalt and op(δ) = (dec, c):
(i) each token tk with a (Vcbeg ∩Vsec dec
)-value is eventually followed by a token tk 0
with a Vc -value such that s(tk 0 ) − e(tk) = 1 (i.e., the difference between
beg
the start time of token tk 0 and the end time of token tk is exactly 1);
(ii) each token tk with a (Vc# ∩ Vsec dec
)-value is eventually followed by a token
tk with a Vc -value where t ∈ {beg, #} such that s(tk 0 ) − s(tk) = 1 and
0 t
e(tk 0 ) − e(tk) = 1 (i.e., the difference of start times and end times is exactly
1).
(iii) each token tk with a (Vcend ∩ Vsec dec
)-value is eventually followed by a token
tk with a Vc -value such that s(tk 0 ) − s(tk) = 1 (i.e., the difference of
0 end
start times is exactly 1);
Undecidability of future timeline-based planning 11
Analogously, (i) and (ii) produce an effect 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,∞) as done before for expressing the equality requirement.
By construction, the untimed part of a future plan of P = ({xM }, RM )
is an initial and halting well-formed computation-code. Vice versa, by exploit-
ing 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 Conclusion and future work
In this paper, we solved a problem left open in [1] by showing that future
timeline-based planning with arbitrary trigger rules is undecidable over dense
temporal domains.
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 effects of applying to the discrete case the same restrictions we
imposed to timeline-based planning over dense time.
Acknowledgements
We would like to acknowledge the support from the GNCS project Strategic
Reasoning and Automatic Synthesis of Multi-Agent Systems.
References
1. Bozzelli, L., Molinari, A., Montanari, A., Peron, A., Woeginger, G.J.:
Timeline-based planning over dense temporal domains. Theor. Com-
put. Sci. 813, 305–326 (2020). https://doi.org/10.1016/j.tcs.2019.12.030,
https://doi.org/10.1016/j.tcs.2019.12.030
2. Cialdea Mayer, M., Orlandini, A., Umbrico, A.: Planning and Execution with
Flexible Timelines: a Formal Account. Acta Informatica 53(6–8), 649–680 (2016).
https://doi.org/10.1007/s00236-015-0252-z
3. Della Monica, D., Gigante, N., Montanari, A., Sala, P.: A novel automata-
theoretic approach to timeline-based planning. In: Thielscher, M., Toni, F.,
Wolter, F. (eds.) Principles of Knowledge Representation and Reasoning: Pro-
ceedings of the Sixteenth International Conference, KR 2018, Tempe, Ari-
zona, 30 October - 2 November 2018. pp. 541–550. AAAI Press (2018),
https://aaai.org/ocs/index.php/KR/KR18/paper/view/18024
4. Gigante, N., Montanari, A., Cialdea Mayer, M., Orlandini, A.: Timelines are Expres-
sive Enough to Capture Action-based Temporal Planning. In: Proc. of TIME. pp.
100–109. IEEE Computer Society (2016). https://doi.org/10.1109/TIME.2016.18
5. Gigante, N., Montanari, A., Cialdea Mayer, M., Orlandini, A.: Complexity of
timeline-based planning. In: Proc. of ICAPS. pp. 116–124. AAAI (2017)
12 L. Bozzelli et al.
6. Gigante, N.: Timeline-based Planning: Expressiveness and Complexity.
Ph.D. thesis, University of Udine, Italy (2019), available on arXiv at:
https://arxiv.org/abs/1902.06123
7. Gigante, N., Michieli, A., Montanari, A., Scala, E.: Decidability and complexity of
action-based temporal planning over dense time. In: Proceedings of the 34th AAAI
Conference on Artificial Intelligence. AAAI Press (2020)
8. Minsky, M.L.: Computation: Finite and Infinite Machines. Automatic Computation,
Prentice-Hall, Inc. (1967)