In timeline-based planning|an approach which is more declarative than standard, action-based planning|the domain is described by a nite set of independent, but interacting, state variables. The temporal behavior of each variable is governed by a transition function, and the sequence of values it takes over time is represented by a timeline. A set of temporal constraints, called synchronization rules, impose suitable conditions on the evolution of the values of variables. The temporal domain is commonly assumed to be discrete, and the dense case is dealt with by introducing an arti cial discretization. Here, we address the problem of timeline-based planning over dense temporal domains, without discretizing them. However, since the unrestricted version of the problem has been recently proved to be undecidable, we focus on the case in which all synchronization rules are trigger-less, and prove its NP-completeness.
In this paper, we study the problem of timeline-based planning. Unlike the standard action-based planning, that focuses on the series of actions an agent has to perform to reach a goal from the initial state of the world, timeline-based one describes in a more declarative fashion what has to happen in order to satisfy the goal. The domain is represented by a set of state variables, each one ? The work by Bozzelli, Molinari, Montanari, and Peron has been supported by the GNCS project Formal methods for veri cation and synthesis of discrete and hybrid systems. The work by Molinari and Montanari has also been supported by the project (PRID) ENCASE|E orts in the uNderstanding of Complex interActing SystEms. modeling a component. State variables are independent of each other, but a set of synchronization rules constrain the temporal relations among them. The evolution of the value of each state variable over time is controlled by a transition function, and described by means of a timeline (a sequence of tokens).
Timeline-based planning has been applied in several contexts [
In this paper, we address the timeline-based planning problem over dense
temporal domains, without resorting to any form of discretization. Since the
problem in its full generality is known to be undecidable over dense domains [
The Timeline-Based Planning Problem
In this section, we give an account of timeline-based planning (TP). We refer the
reader to [
In TP, domain knowledge is encoded by a set of state variables, whose behaviour over time is described by transition functions and synchronization rules. 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 x takes value v. In the following we will also denote (v; d) as (x; v; d) to make x explicit. The behavior of x is speci ed by means of a timeline which is a non-empty sequence of tokens = (v0; d0) (vn; dn) consistent with Tx, i.e., vi+1 2 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 de ned as e( ; i) = Pih=0 dh and s( ; i) = 0 if i = 0, and s( ; i) = Pih=10 dh otherwise.
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 = fo; o0; : : :g 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 t or o1 Ie1 t (time-point atom), where o1; o2 2 , I 2 Intv , t 2 Q+, and e1; e2 2 fs; eg.
An atom is evaluated with respect to a -assignment for a given multi-timeline 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 t (resp., o Ie t) is satis ed by if t e( (o)) 2 I (resp., e( (o)) t 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, we have (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; or > ! 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.
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 x0 takes the value v0, at least one of the existential statements Ei must be satis ed. Trigger-less rules simply assert the satisfaction of some existential statement.
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 (i) = (v0; d), there is an existential statement E of R and a -assignment for consistent with E such that (o0) = ( ; i) and satis es all the atoms of E .
A TP domain P = (SV; S) is speci ed by a nite set SV of state variables and a nite set S of synchronization rules modeling their admissible behaviors. Trigger-less rules can be used to express initial and intermediate conditions, and the goals of the problem, while trigger rules are useful to specify invariants and response requirements. A plan for P is a multi-timeline of SV satisfying all the rules in S. The end time of the token ending last in P is said the horizon of P . The TP problem is to decide if, given a TP domain P , there is a plan for P . 3
Timed Automata and Finite Bounds for Plans
TP over dense temporal domains is, in its full generality, undecidable [
We call k-MWTA the composition of TAs accepting k-multiwords encoding plans. We will show at the end of the section how to derive from k-MWTAs a pair of bounds, on the number of tokens of a plan, and on its horizon, which will be at the basis of the NP algorithm of the next section.
Let us recall some basic notions. Let w be a nite or in nite word over some alphabet. An in nite timed word w over a nite alphabet is an in nite word w = (a1; 1)(a2; 2) over R+ (intuitively, i is the time at which the event ai occurs) such that the sequence = 1; 2; : : : of timestamps satis es: (1) i i+1 for all i 1 (monotonicity), and (2) for all t 2 R+, i t for some i 1 (divergence/progress). The timed word w is also denoted by the pair ( ; ), where is the (untimed) in nite word a1a2 and is the sequence of timestamps. An !-timed language over is a set of in nite timed words over .
Let C be a set of clocks. A clock valuation val : C ! R+ is a function assigning a real value to each clock in C. A clock constraint over C is a Boolean combination of atomic formulas of the form c c0 + cst or c cst, where 2 f ; g, c; c0 2 C, and cst 2 Q+ is a constant. We will often use the interval-based notation, for instance, c 2 [2; 7:4]. We denote by (C) the set of clock constraints over C. Given a clock valuation val for C and a clock constraint over C, we say that val satis es if evaluates to true replacing each occurrence of a clock c in by val (c), and interpreting Boolean connectives in the standard way. Given t 2 R+, (val + t) denotes the valuation such that, for all c 2 C, (val + t)(c) = val (c) + t. For Res C, val [Res](c) = 0 if c 2 Res, and val [Res](c) = val (c) otherwise. a cx 2[1; 1]; cx :=0 q0;x : : : x = c cx 2[2; 8]; cx :=0 c x = a x = b
De nition 6 ([
A con guration of A is a pair (q; sval ), where q 2 Q, and sval is a clock valuation for C. A run of A on w = ( ; ) is an in nite sequence of con gurations = (q0; sval 0)(q1; sval 1) such that q0 2 Q0, sval 0(c) = 0 for all c 2 C (initialization requirement), and the following constraint holds (consecution): for all i 1, for some (qi 1; i; ; Res; qi) 2 , sval i = (sval i 1 + i i 1)[Res] and (sval i 1 + i i 1) j= (we let 0 = 0). The run is accepting if there are in nitely many i 0 such that qi 2 F . The timed language LT (A) of A is the set of in nite timed words w over s.t. there is an accepting run of A on w.
Let us now introduce the encoding of a timeline by a timed word, and the TA
for a state variable. Hereafter, we will assume that, for every x and every v 2 Vx,
we have Tx(v) 6= ;; however, this constraint can easily be relaxed [
In the following, we introduce the formalism of k-multiword TA (k-MWTA). A k-MWTA accepts a language of timed k-multiwords, formally de ned as follows. For k 1 pairwise disjoint alphabets 1; : : : ; k, and the symbol 2= S1 i k i, k- denotes the multialphabet f(a1; : : : ; ak) j ai 2 i [ f g; for 1 i kg n f( ; : : : ; )g. A k-multiword is a word over k- . Intuitively, a k-multiword !a 1 !a 2 is a synchronization of k words over the alphabets 1; : : : ; k; in
x = a11 !a j = (aj1; : : : ajk), for j 1, all the symbols aij such that aij 6= , with 1 i k, occur at the same instant of time, and if aij = , the intended meaning is that no symbol (event) of the i-th alphabet i occurs at that time. A timed k-multiword is just a timed word ( ; ) where the untimed word is a k-multiword.
The notion of timeline encoded by a timed word can be extended to the multi-timeline encoded by a timed k-multiword.
De nition 9. Let x1; : : : ; xk, with xi = (Vxi ; Txi ; Dxi ), be k state variables. The timeline for xj encoded by a timed k-multiword (!a 1; 1)(!a 2; 2) is the timeline encoded by d (!a 1 [j]; 1)(!a 2 [j]; 2) , where d (( ; )) is the timed word obtained from ( ; ) removing occurrences of symbols ( ; 0), for any 02 R+. See Fig. 3 for an example. A k-MWTA can be viewed as a suitable parallel composition of TAs communicating via shared clocks.
De nition 10. For 1 i k, let Ai = ( i; Qi; Q0;i; Ci; i; Fi) be a TA. A k-multiword TA (k-MWTA) for A1; : : : ; Ak is a TA k-A = (k- ; Q; Q0; C; ; F ): { Q = (Q1 : : : Qk) [ fqf g, qf being an (optional) auxiliary nal state, { Q0 = Q0;1 : : : Q0;k, C = C1 [ : : : [ Ck, F = (F1 : : : Fk) [ fqf g, { if (q1; : : : ;qk);(a1; : : : ;ak); ; Cl;(q10; : : : ;qk0) 2 and (q1; : : : ;qk);(q10; : : : ;qk0) 2 Q n fqf g, then = Vik=1 i, Cl = Sik=1 Resi, and, for all i = 1; : : : ; k, if ai 6= , then there exists (qi; ai; i; Resi; qi0) 2 i, if ai = , then it holds qi = qi0, i = >, and Resi = ;.
Notice that more than one k-MWTA can be generated from given A1; : : : ; Ak. The ones we are interested in are those of De nition 11 and De nition 13 below.
We now instantiate De nition 10 over the TA for x1; : : : ; xk.
(q1; : : : ; qk); (a1; : : : ; ak); ; Cl; (q10; : : : ; qk0) 2 De nition 11. Let x1; : : : ; xk be k state variables and, for 1 i k, let Axi = ( i = Vxi ; Qi; fq0;ig; fcig; i; Qi). A k-MWTA for Ax1 ; : : : ; Axk is the k-MWTA k-Ax1;:::;xk = (k- ; Q; fq0g; C; 0 [ 00 ; F ), where: { Q = Q1 : : : Qk, q0 = (q0;1; : : : ; q0;k), C = fc1; : : : ; ckg, F = Q1 : : : Qk, { = 0 i (q1; : : : ; qk) 6= q0, {
Vik=1 i, Cl = Sik=1 Resi, and, for all i = 1; : : : ; k, if ai 6= , then there exists (qi; ai; i; Resi; qi0) 2 i, if ai = , then it holds qi = q0, i = >, and Resi = ;.
i 00=f(q0;(a1; : : : ; ak);Vik=1ci2[1; 1];Sik=1fcig;(a1; : : : ;ak))j(a1; : : : ;ak)2 1 : : : kg { { Proposition 1. Let x1; : : : ; xk be k state variables, with k 1. LT (k-Ax1;:::;xk ) is a set of k-multiwords, each one encoding a timeline for each of x1; : : : ; xk.
Let us now introduce the k-MWTA for the synchronizations rules. Since each rule has the form E1 _ : : : _ En, we focus on a single Ei, the automaton for the rule being just the union of the automata for E1; : : : ; En. Ei has the form 9o1[x1 = v1;j1 ] 9on[xn = vn;jn ]:C, where C is a conjunction of atoms. We associate two clock variables with each quanti er oi[xi = vi;ji ]|named coi;S and coi;E |which, intuitively, are reset when the token chosen for oi starts and ends, respectively. In order to select a suitable token along the timeline, coi;S and coi;E are non-deterministically reset when xi takes the value vi;ji 2 Vxi . Moreover, to deal with atoms involving a time constant (time-point atoms), we introduce a clock variable cglob, which measures the current time and is never reset. For technical reasons, we assume that the start of activities is at time 1 and, consequently, the reset of any coi;S and coi;E cannot happen before 1 time unit has passed from the beginning of the timed word/plan. In fact, in De nition 8, we have cx 2 [1; 1] on all the transitions from q0;x (for this reason, we must also add 1 to all time constants in all time-point atoms). This assumption implies that the value of coi;S is equal to that of cglob if coi;S has never been reset, and less otherwise. Since only one token for each quanti er is chosen in a timeline, coi;S must be reset only once: a transition resetting coi;S is enabled only if the constraint coi;S = cglob is satis ed (likewise for coi;E ).
We now de ne a TA for a state variable x, suitably resetting the clocks associated with all the quanti ers over x. For a set of token names O, we denote by (O; x; v) the subset of names o 2 O such that o[x = v] for a variable x and a value v 2 Vx, and by (O; x) = Sv2Dx (O; x; v). Moreover CS (O) (resp., CE (O)) represents the set fco;S j o 2 Og (resp., fco;E j o 2 Og).
De nition 12. Given x = (Vx; Tx; Dx) and quanti ers o1[x = v1]; : : : ; o`[x = v`], a TA for x; o1; : : : ; o` is Ax;o1;:::;o` = (Vx; Q; fq0g; C; 0 [ 00 ; ;); where: { Q = Vx [ fq0g and C = fcglobg [ fcoi;S ; coi;E j i = 1; : : : ; `g, 0 is the set of tuples v; a; ^ co;S = cglob ^ o2P ^ (co;S < cglob ^ co;E = cglob)^ o2R ^(co;S = cglob _ co;E < cglob); CS (P ) [ CE (R); a o2 (fo1;:::;okg;x;v)nR where v 2 Vx, P (fo1; : : : ; o`g; x; a) and R 00 = f(q0; a; cglob 2 [1; 1]; CS (P ); a) j a 2 Vx; P (fo1; : : : ; o`g; x; v); (fo1; : : : ; o`g; x; a)g.
In De nition 12, R (resp., (fo1; : : : ; okg; x; v)nR) is the set of token names whose end clock must (resp., must not) be reset. The next k-MWTA is a synchronization of TA (each one for the tokens over the same variable) for quanti ers in E . De nition 13. Let x1; : : : ; xk be k variables and E = 9o1[xj1= v1] 9on[xjn= vn]:C, with fj1; : : : ; jng f1; : : : ; kg. A k-MWTA for x1; : : : ; xk; o1; : : : ; on, and E is a k-MWTA for the TA Axi; (fo1;:::;ong;xi) = ( i = Vxi ; Qi; fq0;ig; Ci; i; ;), with 1 i k, k-Ax1;:::;xk;E = (k- ; Q; fq0g; C; 0 [ 00 [ 000 [ 0000 ; fqf g); where: { Q = (Q1 : : : Qk)[fqf g; q0 = (q0;1; : : : ; q0;k); C = fcglobg[fcoi;S ; coi;E ji 2 [1; n]g, k { 0 is the set of tuples (v1; : : : ; vk); (a1; : : : ; ak); ^ ^ co;S = cglob^ i=1 o2Pi ^ (co;S < cglob ^ co;E = cglob) ^ o2Ri ^ (co;S = cglob _ co;E < cglob) ; o2Ri k [ (CS (Pi) [ CE (Ri)); (v10; : : : ; vk0) i=1 { { { satisfying, for all i = 1; : : : ; k, the following conditions: if ai = , then vi = vi0, Pi = ;, and Ri = Ri = ;, if ai 6= , ai = vi0 2 Dxi ; Pi (fo1; : : : ; ong; xi; vi0), Ri [_Ri = (fo1; : : : ; ong;xi;vi) 00 = f(q0; (a1; : : : ; ak); cglob 2 [1; 1]; Sk
i=1 CS(Pi); (a1; : : : ; ak)) j (a1; : : : ; ak) 2 Vx1 : : : Vxk ; Pi (fo1; : : : ; ong; xi; ai) for 1 i kg,
000 = f(q; (a1; : : : ; ak); C ^ Vik=1(coi;S < cglob ^ coi;E < cglob); ;; qf ) j q 2 Vx1 : : : Vxk ; (a1; : : : ; ak) 2 k- g, where C is the translation of C into a (conjunction of ) TA clock constraint(s),
0000 = f(qf ; (a1; : : : ; ak); >; ;; qf ) j (a1; : : : ; ak) 2 k- g.
Note that k-Ax1;:::;xk;E can enter qf only when all token clocks have been reset (Vik=1(coi;S < cglob ^ coi;E < cglob)) and all C's conditions are veri ed.
The TA A~ for a TP domain P = (fx1; : : : ; xkg; S) is built by exploiting the
standard union and intersection operations for TA: A~ is obtained by intersecting
(i) the k-MWTA k-Ax1;:::;xk for the state variables (De nition 11) with (ii) a TA
k-Ax1;:::;xk;R for each trigger-less rule R = > ! W1 i m Ei in S, which is the
disjunction of m k-MWTAk-Ax1;:::;xk;Ei (De nition 13), one for each Ei.
Proposition 2. LT (A~) is the set of plans for P = (fx1; : : : ; xkg; S).
Theorem 1. Let P = (SV; S) be a TP domain with trigger-less rules only. The
problem of checking the existence of a plan for P is in PSPACE.
The theorem is proved by inspecting the standard PSPACE emptiness checking
algorithm for TA, in order to verify that the space complexity remains polynomial
also for k-MWTA. For details we refer the reader to [
Exploiting this result, we can derive a nite horizon for the plans of a (any) problem, that is, if a TP domain P = (SV; S) has a solution plan, then P also 4 I.e., an upper/lower bound of an interval of a token duration, a time constant in an atom, or a bound at the subscript of an atom. We assume they are encoded in binary. has a solution plan whose horizon is no greater than a given bound. Analogously, we calculate a bound on the maximum number of tokens in a plan.
In order to check the emptiness of the previous Buchi automaton of g states, it is enough to nd a nite word uv, where: (i) juj; jvj g, and (ii) there is a run of the automaton that, from an initial state, upon reading u, reaches a state q, and upon reading v from q reaches a nal state and gets ultimately back to q. Finally, we observe that each transition of the Buchi automaton corresponds to the start point of at least a token in some timeline of (a plan for) P , and at most a token for each timeline (when all these tokens start simultaneously). This yields a bound on the number of tokens: 2 g jSV j. We can also derive a bound on the horizon of the plan: 2 g jSV j (K + 1). As a matter of fact, every transition taken in the timed automaton may let at most K + 1 time units pass, as K accounts in particular for the maximum constant to which a (any) clock is compared (clearly, an unbounded quantity of time units may pass, but after K + 1 the last region of the region automaton will certainly have been reached).
By exploiting this pair of bounds, we now describe an NP algorithm. 4
TP with Trigger-less Rules is NP-complete To start with, we provide an example showing that there is no polynomial-size plan for some TP domains. Thus, an explicit enumeration of all tokens across all timelines does not represent a suitable polynomial-size certi cate. Let p(i) be the i-th prime number, assuming p(1) = 1, p(2) = 2, p(3) = 3, p(4) = 5, and so on. For 1 i n, let xi = (fvig; f(vi; vi)g; Dxi ), with Dxi (vi) = [p(i); p(i)]. The rule > ! 9o1[x1 = v1] 9on[xn = vn]: Vin=11oi [e0;e;0] oi+1 is asking for the existence of a \synchronization point", where n tokens (one for each variable) have their ends aligned. Due to the allowed token durations, the rst such time point is Qin=1 p(i) 2n 1. Hence, in any plan, the timeline for x1 features at least 2n 1 tokens: no explicit polynomial-time enumeration of such tokens is possible. It follows that there is no trivial guess-and-check NP algorithm.
We now present a non-deterministic polynomial-time algorithm, proving that the TP problem with trigger-less rules is in NP. At the end of the section, we will see that such problem is in fact NP-complete. The algorithm is structured in 3 phases, whose description follows.
(Phase 1) Preprocessing. As a preliminary preprocessing phase, we consider all rational values occurring in the input TP domain P = (SV; S)|be either upper/lower bounds of an interval of a token duration, a time constant in an atom, or upper/lower bounds (u or `) at the subscript of an atom|and convert them into integers by multiplying them by the lcm of all denominators. This involves a quadratic blowup in the input size, being constants encoded in binary. Given a plan for P 0 (where all values are integers), we can obtain one for the original P by dividing the start/end times of all tokens in each timeline by .
(Phase 2) Non-deterministic token positioning. The algorithm then nondeterministically guesses, for every trigger-less rule in S, a disjunct|and deletes all the others. Moreover, for each (left) quanti er oi[xi = vi], it guesses the integer part of both the start and the end time of the token for xi to which oi is mapped. We call such time instants, respectively, sint(oi) and eint(oi).5 We observe that all start/end times sint(oi) and eint(oi), being less than or equal to 2 g jSV j (K + 1) (the nite horizon bound), have an integer part that can be encoded with polynomially many bits (and thus can be generated in polynomial time). Let us now consider the fractional parts of the start/end time of the tokens associated with quanti ers (we denote them by sfrac(oi) and efrac(oi)). The algorithm non-deterministically guesses an order of all such fractional parts. It has to specify, for every token start/end time, whether it is integer (sfrac(oi) = 0, efrac(oi) = 0) or not (sfrac(oi) > 0, efrac(oi) > 0). Every possibility can be generated in polynomial time. Some trivial tests should be performed, i.e., for all oi, sint(oi) eint(oi), each token is assigned an end time equal or greater than its start time, and no two tokens for the same variable are overlapping.
It is routine to check that if we change the start/end time of (some of the) tokens associated with quanti ers, but we leave unchanged (i) all the integer parts, (ii) zeroness/non-zeroness of fractional parts, and (iii) the order of the fractional parts, then the satisfaction of the (atoms in the) trigger-less rules does not change. This is due to all the constants being integers, as a result of the preprocessing step.6 Therefore we can now check whether all rules are satis ed.
(Phase 3) Enforcing legal token durations and timeline evolutions. We now conclude by checking that: (i) all tokens associated with a quanti er have an admissible duration, and that (ii) there exists a legal timeline evolution between pairs of adjacent such tokens over the same variable (two tokens are adjacent if there is no other token associated with a quanti er in between). We will enforce all these requirements as constraints of a linear problem, which can be solved in deterministic polynomial time (e.g., using the ellipsoid algorithm). When needed, we use strict inequalities, which are not allowed in linear programs. We will show later how to convert these into non-strict ones.
We start by associating non-negative variables oi;s; oi;e with the fractional parts of the start/end times sfrac(oi), efrac(oi) of every token for a quanti er oi[xi = vi]. First, we add the linear constraints 0 oi;s < 1; 0 oi;e < 1: Then, we also need to enforce that the values of oi;s; oi;e respect the decided order of the fractional parts, e.g., 0 = oi;s = oj;s < ok;s < < oj;e < oi;e = ok;e < . To enforce requirement (i), we set, for all oi[xi = vi], a (eint(oi) + oi;e) (sint(oi) + oi;s) b, where Dxi (vi) = [a; b]. Clearly, strict (<) inequalities must be used for a left/right open interval. To enforce (ii), i.e., the existence of a legal timeline evolution between each pair of adjacent tokens for the same state variable, say oi[xi = vi] and oj [xi = vj ], we proceed as follows (analogous considerations hold for an evolution between t = 0 and the rst token). 5 W.l.o.g., we can assume that all quanti ers refer to distinct tokens in timelines. As a matter of fact, the algorithm can non-deterministically choose to force two (or more) quanti ers oi[xi = vi] and oj [xi = vi], over the same variable and value, to refer to the same token just by rewriting all occurrences of oj as oi in the atoms of the rules. 6 We observe that, by leaving unchanged all integer parts, fractional parts' zeroness and order, the region of the region graph of the timed automaton does not change.
Let us consider each state variable xi = (Vi; Ti; Di) as a directed graph G = (Vi; Ti), where Di associates with each vertex v 2 Vi a duration interval. We have to decide whether there is (a) a path in G, possibly with repeated vertices and edges, v0 v1 vn 1 vn, where v0 2 Ti(vi) and vn, with vj 2 Ti(vn), are non-deterministically generated, and (b) a list of non-negative reals d0; : : : ; dn s.t. Pin=0 di = (sint(oj ) + oj;s) (eint(oi) + oi;e) and, for all 0 s n, ds 2 Di(vs).
To this aim, we guess a set of integers f u0;v j (u; v) 2 Tig. Intuitively, u0;v is the number of times the solution path traverses (u; v). Since every time an edge is traversed a new token starts, each u0;v is bounded by the number of tokens, i.e., by 2 g jSV j. Hence the binary encoding of u0;v can be generated in polynomial time. Then, we perform the following deterministic steps. 1. We consider the set E0 := f(u; v) 2 Ti j u0;v > 0g (subset of the edges of G), and we check whether it induces an (undirected) connected subgraph of G. 2. Check (a) P(u;v)2E0 u0;v = P(v;w)2E0 v0;w for v 2 Vinfv0; vng (b) P(u;v0)2E0 u0;v0 = P(v0;w)2E0 v00;w 1 (c) P(u;vn)2E0 0u;vn = P(vn;w)2E0 0vn;w + 1. 3. For all v 2 Vi n fv0g, we de ne yv := P(u;v)2E0 u0;v (yv is the number of times the solution path gets into v); moreover, yv0 := P(v0;u)2E0 v00;u. 4. We de ne the real non-negative variables zv, for every v 2 Vi (zv is the total waiting time of the path on the node v), subject to the following constraints: a yv zv b yv; where Di(v) = [a; b] (the constraint is analogous for open intervals). Finally, we set Pv2Vi zv = (sint(oj ) + oj;s) (eint(oi) + oi;e).
Steps 1. and 2. together check that the values u0;v for the edges specify a
directed Eulerian path from v0 to vn in a multigraph. The following indeed holds.
Theorem 2 ([
Steps 3. and 4. evaluate the waiting times of the path in some vertex v with duration interval [a; b]. If the solution path visits v yv times, then each single visit must take at least a and at most b units of time. Hence, the overall visitation time is in between a yv and b yv. Vice versa, if the total visitation time is in between a yv and b yv, then it can be split into yv intervals each falling into [a; b].
The algorithm concludes by solving the linear program given by the variables oi;s and oi;e for each quanti er oi[xi = vi], and, for each pair of adjacent tokens in the same timeline, say for xi, for each v 2 Vi, the variables zv subject to their constraints. However, in order to conform to linear programming, we have to replace all strict inequalities with non-strict ones. All constraints involving strict inequalities we have written so far are of (or can easily be converted into) the following forms: s < q + k or s > q + k, where s and q are variables, and , , k are constants. We replace them, respectively, by s q k + t 0 and s q k t 0, where t is an additional fresh non-negative variable, which is local to a single constraint. The original inequality and the new one are equivalent if and only if t is a small enough positive number. Moreover, we add another non-negative variable, say r, which is subject to a constraint r t, for each of the introduced variables t (i.e., r is less than or equal to the minimum of all t's). Finally, we maximize the value of r when solving the linear program. We have that max r > 0 if and only if there is an admissible solution where the values of all t's are positive (and thus the original strict inequalities hold true).
We conclude with the next result (that holds even for a single state variable). Theorem 3. Let P be a TP domain with trigger-less rules only. Checking the existence of a plan for P is an NP-complete problem.
Proof. For NP-hardness, there is a reduction from the problem of the existence of a Hamiltonian path in a directed graph G. Given G = (V; E), with jV j = n, we de ne x = (V; E; Dx), where Dx(v) = [1; 1] for each v 2 V . We add the following trigger-less rules, one for each v 2 V : >! 9o[x = v]:o [s0;n 1] 0: The rule for v 2 V requires that there is a token (x; v; 1) on the timeline for x, starting no later than n 1. G has a Hamiltonian path i there is a plan for the planning problem.
Conclusions and Future Work
In this paper, we studied TP restricted to trigger-less rules, over dense temporal
domains, proving its NP-completeness. We analyzed this case as the unrestricted
version of the problem is known to be undecidable [
In future work, we will focus on decidability and complexity of intermediate fragments of TP, namely, where forms of synchronization rules in between the general ones and trigger-less are considered. For instance, we may allow only rules for future, and/or non-singular intervals in the atoms of trigger-rules.