--- title: "Temporalising Separation Logic for Planning with Search Control Knowledge" authors: - "Xu Lu" - "Cong Tian" - "Zhenhua Duan" doi: "10.24963/ijcai.2017/162" url: "https://ijcai.org/proceedings/2017/162" pdf: "https://ijcai.org/proceedings/2017/0162.pdf" venue: "Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence" year: 2017 pages: "1167-1173" track: "Main track" keywords: - "Planning and Scheduling: Other approaches to planning" - "Knowledge Representation, Reasoning, and Logic: Logics for Knowledge Representation" - "Constraints and Satisfiability: Satisfiability" - "Knowledge Representation, Reasoning, and Logic: Geometric, Spatial, and Temporal Reasoning" --- # Temporalising Separation Logic for Planning with Search Control Knowledge Xu Lu, Cong Tian, Zhenhua Duan *Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence*, pages 1167-1173. DOI: [10.24963/ijcai.2017/162](https://doi.org/10.24963/ijcai.2017/162) ## Abstract Temporal logics are widely adopted in Artificial Intelligence (AI) planning for specifying Search Control Knowledge (SCK). However, traditional temporal logics are limited in expressive power since they are unable to express spatial constraints which are as important as temporal ones in many planning domains. To this end, we propose a two-dimensional (spatial and temporal) logic namely PPTL^SL by temporalising separation logic with Propositional Projection Temporal Logic (PPTL). The new logic is well-suited for specifying SCK containing both spatial and temporal constraints which are useful in AI planning. We show that PPTL^SL is decidable and present a decision procedure. With this basis, a planner namely S-TSolver for computing plans based on the spatio-temporal SCK expressed in PPTL^SL formulas is developed. Evaluation on some selected benchmark domains shows the effectiveness of S-TSolver. ## Full text ## 1 Introduction Artificial Intelligence (AI) planning [Ghallab et al., 2004] has been studied for decades and become even more attractive in recent years. However, existing planners still suffer from a difficult problem: explosion of the search space. One of the most powerful approaches to cope with it is to provide planners with additional Search Control Knowledge (SCK) in specific domains such that the planner can get rid of irrelevant parts of the search space. Techniques for applying SCK in planning have received much attention. It has been proved that SCK is helpful in improving efficiency of the domainindependent planners [Huang et al., 1999]. Even with the basic search strategy, e.g. depth-first search, and proper SCK, planners are able to achieve surprising effectiveness in a range of benchmark problems. Several planners such as TLPlan [Bacchus and Kabanza, 2000], TALplanner [Kvarnstr¨om and Magnusson, 2003], and SHOP2 [Nau et al., 2003], have successfully exploited SCK ∗This research is supported by the NSFC Grant Nos. 61420106004 and 91418201. †Corresponding authors. All authors are joint first authors. to guide planning. Concretely, the forward-chaining planner, TLPlan, provides a first-order Linear Temporal Logic (LTL) with bounded quantification based platform for reasoning about SCK. With this approach, we can specify, for instance, what can or cannot happen at the next time step by using the "next" operator in LTL. TALplanner, another forward-chaining planner, supports a unified planning framework where SCK and other information relevant to planning domain and problem instance are all represented as logic formulas in a member of Temporal Action Logics (TAL) family. Compared with TLPlan, TALplanner uses the same planning paradigm, but it is capable of producing parallel plans. In SHOP2, SCK is expressed with Hierarchical Task Network (HTN) [Georgievski and Aiello, 2015] to guide the search. A transition-based SCK inspired by finite state automata is introduced in [Chrpa and Bart´ak, 2016] where knowledge about dependencies between planning operators is represented with transitions of an automaton so as to restrict the number of operator instances during the planning process. Additionally, several research groups investigate advanced mechanisms on the topic of learning SCK in a given domain [Fern et al., 2004; Yoon et al., 2008]. SCK based planning approaches are proved to be effective in practice. Our observation is that despite temporal constraints in SCK, consideration of spatial constraints will be of equal importance. In many circumstances, just temporal SCK is not enough to guarantee a planner to perform effectively as expected. However, temporal logics employed in the existing logic-based planning frameworks are unable to describe spatial structures at each time step. Thus, this paper is motivated to propose a two-dimensional (spatial and temporal) logic namely PPTL SL for describing spatio-temporal SCK. To do so, we temporalise separation logic [Reynolds, 2002] with PPTL (Propositional Projection Temporal Logic) [Duan, 1996] to express both spatial and temporal dimensions of SCK. PPTL is a powerful linear time based temporal logic which facilitates to describe full regular language that goes beyond both LTL and CTL [Tian and Duan, 2008]. Separation logic is a spatial logic for reasoning about dynamic allocated data structures, e.g. linked lists, trees and DAGs (Directed Acyclic Graph). Within PPTL SL , a decidable fragment of separation logic is used to describe the spatial structure at a point of time and temporal operators of PPTL are adopted to capture the evolution of spatial structures over time. The main contributions of this paper are twofold: on one hand, we propose a two-dimensional logic system for both spatial and temporal constraints in planning; on the other hand, we prove the decidability of the proposed logic and implement a planner running on benchmarks to demonstrate its effectiveness. With the best of our knowledge, our work is the first use of separation logic in planning. Related work: Spatio-temporal logic MTLA presented in [Merz et al., 2003] is specialized for mobile systems. It augments Temporal Logic of Actions with spatial modalities to express the topology of configurations in tree structures. But description of other non-tree structures cannot be supported. SpaTel is a spatio-temporal logic [Haghighi et al., 2015] which can describe a property such as "power consumption in city A and city B never exceed 150 MW for longer than 20 minutes". The spatial dimension here is represented by static individual locations instead of spatial structures. The approach in [Belouaer and Maris, 2010] defines SMT encoding rules for spatio-temporal planning by allowing synchronization of non-instantaneous actions in space. In this approach, the temporal and spatial dimensions are independent. The Spatio-Temporal Planning System (STPS) proposed in [Boukharrou et al., 2015] provides a formal description of possible plan actions of an ambient intelligent agent including timing constraints, action duration and spatial requirements of an agent plan. However, only limited spatial knowledge such as "an agent is at some location" can be described in STPS. Compared with the existing spatio-temporal logics, our logic reflects the evolution of a variety of spatial structures especially spatial non-interference features in AI planning. For example, the property "two spatial structures (e.g. linked lists) are always disjoint" can be expressed in PPTL SL , but cannot be expressed by other relevant logics. ## 2 AMotivating Example CityCar domain encoded in PDDL (Planning Domain Definition Language) standard [Fox and Long, 2003] is a newly introduced benchmark in International Planning Competition (IPC) 2014 [Vallati et al., 2015]. It aims to simulate the impact of road building/demolition in traffic networks. A city is represented as a graph, in which each node is a junction and edges are roads. Some cars start from different positions (identified as garages) and have to reach their final destinations as soon as possible. There are a finite number of one-way roads available, which can be built for connecting two neighbor junctions and allowing a car to move between them. If it is necessary, roads can also be removed and placed somewhere else. Each action has a different cost. Figure 1 shows a problem instance of the CityCar domain with 2 garages (g0, g1), 9 junctions (j0, . . . , j8), 5 roads (r0, . . . , r4) and 2 cars (c0, c1). Car c0 is at garage g0, and c1 is at g1. The goal junctions of c0 and c1 are j6 and j8, respectively. At the moment, roads r0 and r3 are used. In this domain, we can express the SCK "if any road is available, do not destroy a road which has already been built" in LTL formula □(∀r : (in place(r)∧∃r1 : ¬in place(r1)) → ©in place(r)). Here in place(r) is a predicate which means road r has been put in place. However, with only temporal specifications, we still cannot find a plan of good quality. Actually, the network topology can be shaped in a variety of ways and a road can be built between any two neighbor junctions at each step (120 alternative ways in total in Figure 1). A mechanism is required to express both spatial and temporal SCK to guide or control the search. For example, a spatiotemporal SCK "each newly-built road should be reachable from some car (§)" will avoid substantial bad road building plans inappropriate for a car to move as early as possible. Under this restriction, only 33 road building actions are feasible in Figure 1. As another example, the spatio-temporal SCK "two disjoint paths (no common locations except the starting and ending points of the paths) between any two junctions do not exist (‡)" is also useful for the sake of pruning plans where redundant roads appear. With this SCK, 12 road building actions can be further reduced. The red dashed-line arrows indicate the places where a road can be built under the guidance of (§) and (‡). Figure 1: A problem instance of the CityCar domain ![Image](https://ijcai.org/proceedings/2017/fulltext/162/image_000000_b7923d4d0e2f929414099af3de26071e59412d06796cf68b314fbb1a1d2497d4.png) ## 3 Preliminary This section presents a decidable fragment of separation logic. Let Var be a countable set of spatial variables, Π a countable set of atomic propositions, Loc a finite set of spatial locations, Val = Loc ∪ {nil } the set including the unfilled location nil and locations in Loc, and B the boolean domain { true, false }. A term e can be nil, a variable x ∈ Var or a location l ∈ Loc. A decidable fragment of separation logic (SL for short) is defined by the following grammar: where π ∈ Π. SL is a variation of the one presented in [Brochenin et al., 2012] by extending single field formula e ↦→ {e′ } to multiple fields e0 ↦→ {e1, . . . , en } such that a variety of spatial structures can be described other than singly-linked lists. A state is a triple (Iπ, Iv, Is), where Iπ : Π ⇀ B, Iv : Var ⇀ Val and Is : Loc ⇀ ⋃ni=1 Val i . Here, ⇀ is the notation for partial mapping. Iπ, Iv and Is serve as the evaluations of propositions, spatial variables and spatial cells, respectively. We call Is the spatial container and use dom(f) to denote the domain of mapping f. Given two mappings f1 and f2, f1 ⊥ f2 means that f1 and f2 have disjoint domains, and f1 · f2 denotes the union of f1 and f2 with disjoint domains. The evaluation of a term e relative to a state s = (Iπ, Iv, Is) is written as s[e] ∈ Val: s[nil] = nil, s[l] = l, s[x] = Iv(x). The semantics of SL formulas is defined as follows: Intuitively, e0 ↦→ { e1, . . . , en } means there are links between e0 and every ei (1 ≤ i ≤ n). Formula φ#φ′ describes a space which can be separated into two disjoint parts, one makes φ true and the other makes φ′ true. The following shows some useful derived formulas: Formula e ↦→ ei denotes there is a link between e and ei. lsn (e1, e2) precisely describes a path from e1 to e2 of length n without any other locations (e2 is also excluded). e1 →+ e2 and e1 →∗ e2 indicate that e2 is reachable from e1. ## 4 Spatio-Temporal Logic PPTL SL This section presents the spatio-temporal logic PPTL SL and shows how spatio-temporal SCK can be expressed with PPTL SL formulas. ## 4.1 Temporalising SL with PPTL where φ denotes an SL formula. © (next), prj (projection) and ∗ (star) are basic temporal operators in PPTL [Duan, 1996; Duan et al., 2008]. A formula is called a state formula if it does not contain any temporal operators, otherwise it is a temporal formula. An interval σ = 〈s0, s1, . . .〉 is a non-empty sequence of states, possibly finite or infinite. The length of σ, denoted by |σ|, is ω if σ is infinite, otherwise it is the number of states minus one. We consider the set N0 of non-negative integers, define Nω = N0 ∪ {ω }, and extend the comparison operators, =, <, ≤, to Nω by considering ω = ω, and for all i ∈ N0, i < ω. Moreover, we define ⪯ as ≤ \{ (ω, ω) }. With such a notation, σ(i...j)(0 ≤ i ⪯ j ≤ |σ|) denotes the sub-interval 〈si, . . . , sj〉. The concatenation of σ with another interval σ′ is denoted by σ · σ′ . Let σ = 〈sk, . . . , s|σ|〉 be an interval and r1, . . . , rn be integers (n ≥ 1) such that 0 ≤ r1 ≤ r2 ≤ · · · ≤ rn ⪯ |σ|. The projection of σ onto r1, . . . , rn is the interval, σ ↓ (r1, . . . , rn) = 〈st1 , . . . , stm 〉, where t1, . . . , tm are obtained from r1, . . . , rn by deleting all duplicates. An interpretation of a PPTL SL formula is a triple I = (σ, k, j) where σ = 〈s0, s1, . . .〉 is an interval, k a nonnegative integer and j an integer or ω such that 0 ≤ k ⪯ j ≤ |σ|. We write (σ, k, j) |= P to mean that a formula P is interpreted over a sub-interval σ(k...j) of σ with the current state being sk. The notation sk = (I k π , I k v , I k s ) indexed by k represents the k-th state of an interval σ. The satisfaction relation |= for PPTL SL formulas is defined by: Table 1: Predicates for the CityCar Domain | Predicate | Description | |--------------------------------------------------------------------------|---------------------------------------------------------------------------------------------------------------| | arrived(c, j) at car jun(c, j) at car road(c, r) road connect(r, j1, j2) | Car c arrives at junction j. Car c is at junction j. Car c is at road r. Road r connects junctions j1 and j2. | and k = r0 ≤ r1 ≤ · · · ≤ rm ⪯ j such that (σ, ri-1, ri) |= Pi for all 1 ≤ i ≤ m and (σ′ , 0, |σ′ |) |= P for one of the following σ′ : A formula P is satisfied over an interval σ, written as σ |= P, if (σ, 0, |σ|) |= P holds. We also have some derived formulas: Here, ε denotes an interval with zero length, □ and ♦ have the standard meanings as in LTL. Formula P1; P2 requires that P1 holds from now on until some point in the future, and from that point on, P2 holds. Additionally, we borrow the GOAL modality from TLPlan, and only allow it to apply to state formulas. For example, suppose arrived(c0, j6) is true in the goal state, then the formula GOAL(arrived(c0, j6)) will be evaluated to true, otherwise to false. ## 4.2 Specifying Spatio-Temporal SCKwith PPTL SL For the CityCar domain, the predicates involved are listed in Table 1. Despite the common temporal SCK, we can describe several interesting and practical spatio-temporal SCK by PPTL SL . First we define a predicate at car jun road(c, j) indicating that car c is either at junction j or a road with the ending junction being j. - The spatio-temporal SCK (§) mentioned in the motivating example can be expressed by: - The spatio-temporal SCK (‡) can be described by: If there are two connections from j1 to j3 and j4 (road connect(r1, j1, j3) ∧ road connect(r2, j1, j4)), we must ensure shared locations from j3 to j2 and j4 to j2 are nonexistent (¬(j3 →∗ j2#j4 →∗ j2)). ## · There is another important spatio-temporal SCK: which can be read as "if a car can reach its goal junction via a path, then the car must move through the path". In this SCK, j1 is the junction where car c at. Suppose there is a path from j1 to the car's goal j2 (j1 →+ j2) and j3 is the next junction of j1 in the path (road connect(r, j1, j3) ∧ j3 →∗ j2). The car cannot go anywhere but move on the road from j1 to j3. ## 5 FromPPTL SL to PPTL In this section, an equisatisfiable translation from PPTL SL to its restricted form called RPPTL SL is presented. Then, based on it, a decision procedure of PPTL SL is obtained. ## 5.1 Equisatisfiable Translation Similar to the method in [Calcagno et al., 2005], we first encode SL into a quantifier-free first-order logic. Definition 1. A bounded variable (proposition) assignment written as Iv[X](Iπ[Y ]) denotes the set of variable (proposition) assignments such that Iv ∈ Iv[X] iff dom(Iv) = X (Iπ ∈ Iπ[Y ] iff dom(Iπ) = Y ), where X ⊆ V ar(Y ⊆ Π). A bounded spatial container written as Is[n] denotes the set of spatial container such that Is ∈ Is[n] iff |dom(Is)| ≤ n, where n ∈ N. Given a spatial container Is ∈ Is[n], we will use a vector c of n tuples of values, ((c1,1, . . . , c1,m1 ), . . . , (cn,1, . . . , cn,mn )), to represent Is. If ci,1 = nil, the i-th tuple does not represent an active spatial cell. Otherwise if ci,1 = li, the i-th tuple represents that the location li contains ci,2, . . . , and ci,mi . For instance, Is[2] is a set consisting of spatial containers with the domain size no more than 2. In addition, a vector that allows the same location occurring more than once should be avoided. For example, ((l1, l2), (l1, l2)) or ((l1, l2), (l1, l3)) does not represent a valid spatial container. The partial function vhn : (⋃i∈{m1,...,mn } V ali )n ⇀ Is[n] is employed to overcome this problem. Let C denote a vector of n tuples of variables. If a vector c with the same size is assigned to C, C will also potentially represent a spatial container. Given a vector of values c = ((c1,1, . . . , c1,m1 ), . . . , (cn,1, . . . , cn,mn )) and a vector of variables C = ((C1,1, . . . , C1,m1 ), . . . , (Cn,1, . . ., Cn,mn )), we write [C ⇐ c] to denote the pointwise assignment of c to C which can be considered as a set of tuples { (Ci,j, ci,j) | 1 ≤ i ≤ n and 1 ≤ j ≤ |Ci| }. The notation |C|(|c|) denotes the number of the tuples in C(c), and |Ci|(|ci|) the number of variables (values) in the i-th tuple. In the sequel, a set of pairs D = { (x1, y1), (x2, y2), . . . } with ∄(x, y), (x, z) ∈ D and y ̸= z is implicitly interpreted as a function. Conversely, a function f can be interpreted as a set of pairs { (x, f(x)) | x ∈ dom(f) }. The standard notation ∨x∈{ l1,...,ln } φ is used to represent φ[l1/x] ∨ · · · ∨ φ[ln/x], which can be lifted to vectors, i.e., ∨C∈Valn φ. Similarly, ∧x∈{ l1,...,ln } φ. fv(φ)(fp(φ)) denotes the set of free variables (propositions) that appear in φ. C = C ′ #©C ′′ defined below is adopted for capturing the semantics of "#". The function f(φ, C) takes φ and C as two parameters and produces a non-spatial state formula φs which is defined by: φs ::= π | e1 = e2 | ¬φs | φs1 ∨ φs2 . where both C ′ and C ′′ are vectors of fresh variables. Lemma 1. For any state formula φ, variable vector C and value vector c where |C| = |c| = n, (Iπ, Iv, Is) ∈ (Iπ[fp(φ)], Iv[fv(φ)], Is[n]), vhn(c) = Is and fv(φ) ∩ fv(C) = ∅, (Iπ, Iv, Is) |=SL φ iff (Iπ, Iv ∪ [C ⇐ c], ∅) |=SL f(φ,C) Proof sketch. The proof proceeds by induction on φ. The difficulty lies in the case φ1#φ2. In f(φ1#φ2,C) where vector C is employed to simulate the spatial container, the key is to prove C = C ′ #©C ′′ that makes [C ′ ⇐ c′ ] and [C ′′ ⇐ c′′ ] correspond to two separate spatial containers whose union equals to the spatial container represented by [C ⇐ c]. This obeys the semantics of #. Further, (Iπ, Iv, Is) |=SL φ1 iff (Iπ, Iv ∪ [C ′ ⇐ c′ ], ∅) |=SL f(φ1,C ′ ) and (Iπ, Iv, Is) |=SL φ2 iff (Iπ, Iv ∪ [C ′′ ⇐ c′′ ], ∅) |=SL f(φ2,C ′′ ) hold by induction hypothesis. This proof is similar to the one for Theorem 1 in [Calcagno et al., 2005]. We now translate PPTL SL formulas to its restricted form RPPTL SL whose syntax is given below. Compared with PPTL SL , atomics of RPPTL SL are in φs instead of φ. Ps ::= φs | ¬Ps | Ps1 ∨Ps2 | ©Ps | (Ps1 , . . . , Psm ) prj Ps | P ∗ s The translation function F defined below will map a PPTL SL formula and a variable vector to a RPPTL SL formula. Also, this function preserves the satisfaction of P. Theorem 1. For any PPTL SL formula P, interval σ and vectors C, c1 , . . ., c|σ| where fv(P) ∩ fv(C) = ∅, it has Here, σ′ = σ[(I iπ , I iv ∪[C ⇐ ci ], ∅)/(I iπ , I iv , I is )] is an interval obtained from σ by replacing (I iπ , I iv , I is ) with (I iπ , I iv ∪[C ⇐ ci ], ∅), (I iπ , I iv , I is ) ∈ (Iπ[fp(P)], Iv[fv(P)], Is[n]), |C| = |ci | = n, and vhn(ci ) = I is (1 ≤ i ≤ |σ|). Proof sketch. By Lemma 1, the translation f preserves the satisfiability of state formulas. The rest cases are straightforward to be proved based on a structural induction on P . Theorem 1 enables one to only concentrate on RPPTL SL instead of PPTL SL for easily attaining a decision procedure. ## 5.2 ADecision Procedure Since RPPTL SL and PPTL have the same syntax structures except for atomic formulas, we are inspired to reuse the decision procedure of PPTL for RPPTL SL . To do so, similar to PPTL, we define normal form of where Pej and Pci are conjunctions of atomic formulas or their negations, and P ′ i is a general RPPTL SL formula. Informally, the normal form of a formula Ps decomposes itself into current states (Pej , Pci ) and future formulas (P ′ i ) that shows which parts of Ps are still to be satisfied after reaching the current states. One can derive that any RPPTL SL formula is able to be written to its normal form. Theorem 2. Any RPPTL SL formula Ps can be rewritten into its normal form. Proof sketch. The normal form translation of PPTL formulas is mainly based on logic laws relevant to temporal operators. Since the only difference between RPPTL SL and PPTL is the state formulas which are free of temporal operators, RPPTL SL inherits all the temporal laws in PPTL [Duan, 1996; Duan et al., 2008]. Hence we can translate Ps to its normal form in the same way for translating a PPTL formula to normal form. Consequently, the decision procedure of PPTL which relies heavily on normal form can be reused for checking the satisfiability of both RPPTL SL and PPTL SL formulas. The progression algorithm of [Bacchus and Kabanza, 2000] decomposes an LTL formula into current state formulas and future temporal formulas. The idea of normal form of RPPTL SL is somewhat similar. This allows to directly use an incremental way to check SCK as the progression algorithm in [Bacchus and Kabanza, 2000] by evaluating state formulas attained during normal form translation at each time stamp. ## 6 Implementation and Experiments We have implemented a planner S-TSolver which handles SCK in collaborating with the classical forward chaining algorithm and SMT solver Z3 [De Moura and Bjørner, 2008]. To plan with S-TSolver, a domain, an instance and SCK expressed in PPTL SL formulas are taken as input. At each step, the forward chaining algorithm responds for exploring the current world of the instance by executing an action, while the equisatisfiable translation (Theorem 1) and the progression technique (Theorem 2) are employed to transform each SCK into its normal form. The current world of the instance and the current state formulas of SCK which are both within the scope of SMT [Barrett et al., 2009] are encoded into SMT-LIB format [Barrett et al., 2010] and fed to Z3 for satisfiability checking. If Z3 returns "sat", the action is added to the plan sequence which is empty initially; otherwise the forward chaining algorithm randomly chooses another action which can be executed to repeat the above process until the goal is achieved or all the worlds are explored. We evaluate the performance of S-TSolver in planning on two domains: CityCar and Transport. We choose these two domains because they are typical domains with both spatial and temporal constraints such that spatio-temporal SCK can be used for planning. Moreover, the two domains are representative: the spatial structure changes over time for the CityCar domain and is fixed for the Transport domain. We compare the results of S-TSolver with the top three planners [Vallati et al., 2014] in IPC2014 on the two domains, respectively. All the experiments are conducted on a PC running Ubuntu 16.04 on an Intel® Core TM i3-550 CPU 3.20GHz and 8Gb of RAM. Original from IPC2008, the Transport domain is a variant of the well-known domain logistics. The task of this domain is to transport several packages from the initial locations to the desired destinations. A package is transported from one location to another one by loading it into a truck, driving the truck to the destination, and unloading the truck. Analogous to the CityCar domain, there is a network for trucks to move. Therefore, we can specify some spatio-temporal SCK for this domain, e.g. "each truck must move to the nearest location which is the goal of some package loaded by the truck or where some package is required to be transported". Note that "nearest" means the minimum steps for a truck to move. We select some instances from this domain. The experiment results are demonstrated in Table 2. The first column shows the problem instances. The column "cost" presents the lowest plan cost among the plans found by a planner. The column "time" is the search time and the column "len" is the length of the plan. Usually the higher the cost, the longer the length. "S-TSolver(T)" is the result of S-TSolver with only temporal SCK, and "S-TSolver(S-T)" is the result with both temporal and spatio-temporal SCK. "time-out" indicates a planner cannot provide a plan within 10 minutes. Every lowest cost and best time are highlighted in bold. For the CityCar domain, the top three tools performed well in IPC2014 are arvandherd, jasper and uniform. From Table 2, it is observed that both S-TSover(T) and S-TSover(S-T) are capable of solving all the problem instances, but arvandherd, jasper and uniform can only solve part of them. With regard to search time, the time spent by S-TSolver(T) is less than S-TSolver(S-T) since extra time is consumed to deal with spatio-temporal SCK. The time spent by uniform is less than 30s for the solved instances as a preset time limitation (≈30s) is given in this tool for each search iteration. If no plans are found within the limitation, another search will be started. arvandherd and jasper give no solutions to some difficult instances. They spend even hundreds of seconds to search for a plan. For the plan cost, the plans generated by S-TSolver(S-T) have better quality than other tools. This is because the strategies expressed by spatio-temporal SCK can easily guide a car to its goal without doing many useless actions. Table 2: Experiment results: CityCar Domain and Transport Domain | CityCar instances | S-TSolver(T) - cost | S-TSolver(T) - time(s) | S-TSolver(T) - len | S-TSolver(S-T) - cost | S-TSolver(S-T) - time(s) | S-TSolver(S-T) - len | arvandherd - cost | arvandherd - time(s) | arvandherd - len | jasper - cost | jasper - time(s) | jasper - len | uniform - cost | uniform - time(s) | uniform - len | |---------------------|-----------------------|--------------------------|----------------------|-------------------------|----------------------------|------------------------|-----------------------|------------------------|-----------------------|-----------------|--------------------|----------------|------------------|---------------------|-----------------| | p01 | 102 | 0.04 | 30 | 70 | 0.68 | 17 | 70 | 2.07 | 17 | 70 | 2.03 | 17 | 70 | 0.18 | 17 | | p02 | 152 | 0.17 | 35 | 128 | 4.6 | 29 | 136 | 12.89 | 28 | 549 | 2.55 | 55 | 118 | 0.74 | 29 | | p03 | 106 | 0.34 | 27 | 116 | 2 | 28 | 116 | 16.2 | 28 | 100 | 13.84 | 32 | 100 | 1.26 | 32 | | p04 | 264 | 0.31 | 67 | 136 | 8.48 | 41 | 202 | 11.19 | 39 | 298 | 8.89 | 51 | 142 | 20.12 | 37 | | p05 | 86 | 0.05 | 39 | 126 | 5.22 | 41 | 100 | 9.31 | 33 | 492 | 4.21 | 67 | 86 | 2.02 | 39 | | p06 | 594 | 1.08 | 92 | 138 | 8.11 | 28 | 184 | 18.78 | 26 | 287 | 48.92 | 34 | 176 | 26.22 | 26 | | p07 | 542 | 0.87 | 62 | 158 | 7.86 | 28 | 174 | 29.39 | 25 | 214 | 31.36 | 27 | - | time-out | - | | p08 | 294 | 0.37 | 30 | 114 | 4.79 | 22 | 124 | 27.6 | 22 | 194 | 20.18 | 26 | - | time-out | - | | p09 | 322 | 0.57 | 46 | 128 | 5.71 | 28 | 158 | 57.74 | 29 | 342 | 175.12 | 44 | - | time-out | - | | p10 | 206 | 0.51 | 42 | 188 | 16.04 | 30 | 182 | 30.91 | 35 | - | time-out | - | - | time-out | - | | p11 | 438 | 0.75 | 64 | 192 | 11.8 | 36 | 292 | 59.97 | 40 | 211 | 84.43 | 35 | - | time-out | - | | p12 | 348 | 0.66 | 48 | 146 | 19.5 | 38 | 344 | 14.53 | 47 | 320 | 19.24 | 41 | 146 | 27.68 | 38 | | p13 | 754 | 1.89 | 138 | 232 | 19.88 | 60 | 432 | 152.5 | 62 | 467 | 323 | 57 | - | time-out | - | | p14 | 250 | 0.3 | 48 | 164 | 16.82 | 48 | - | time-out | - | - | time-out | - | - | time-out | - | | p15 | 1226 | 2.16 | 150 | 264 | 28.23 | 54 | 355 | 34.9 | 50 | 453 | 275.84 | 63 | - | time-out | - | | p16 | 524 | 0.82 | 110 | 150 | 10.07 | 44 | 209 | 83.7 | 45 | - | time-out | - | - | time-out | - | | p17 | 2784 | 5.62 | 412 | 204 | 57.48 | 50 | 444 | 174.97 | 66 | - | time-out | - | - | time-out | - | | p18 | 334 | 0.49 | 90 | 170 | 43.05 | 56 | - | time-out | - | - | time-out | - | - | time-out | - | | p19 | 1530 | 3.48 | 242 | 304 | 35.43 | 76 | 503 | 250.35 | 67 | - | time-out | - | - | time-out | - | | p20 | 610 | 1.15 | 100 | 230 | 33.08 | 48 | - | time-out | - | - | time-out | - | - | time-out | - | | Transport | S-TSolver(T) | S-TSolver(T) | S-TSolver(T) | S-TSolver(S-T) yahsp3 | S-TSolver(S-T) yahsp3 | S-TSolver(S-T) yahsp3 | S-TSolver(S-T) yahsp3 | S-TSolver(S-T) yahsp3 | S-TSolver(S-T) yahsp3 | mercury | mercury | mercury | dae yahsp | dae yahsp | dae yahsp | | instances | cost | time(s) | len | cost | time(s) | len | cost | time(s) | len | cost | time(s) | len | cost | time(s) | len | | p01 | 1841 | 1.86 | 121 | 680 | 6.35 | 55 | 1696 | 0.13 | 114 | 617 | 66.16 | 55 | 954 | 157.54 | 69 | | p02 | 1524 | 1.35 | 98 | 633 | 8.28 | 54 | 1163 | 572.6 | 85 | 639 | 52.36 | 56 | 892 | 35.55 | 71 | | p03 | 4198 | 7.13 | 248 | 1084 | 24.16 | 78 | 2018 | 0.67 | 150 | 848 | 170.9 | 69 | 1422 | 179.84 | 102 | | p04 | 5819 | 31.17 | 368 | 890 | 21.59 | 76 | 2308 | 0.51 | 200 | 800 | 148.34 | 71 | 1774 | 90.15 | 127 | | p05 | 3952 | 10.18 | 291 | 837 | 41.77 | 79 | 2443 | 551.42 | 233 | 907 | 147.26 | 92 | 1877 | 109.74 | 156 | | p06 | 11569 | 34.04 | 802 | 1088 | 70.84 | 107 | 2569 | 265.45 | 240 | 1040 | 102.04 | 104 | 2452 | 204.5 | 206 | | p07 | 3961 | 26.75 | 316 | 1131 | 145.36 | 118 | 3031 | 1.36 | 298 | 1220 | 107.86 | 124 | 2895 | 69.41 | 236 | | p08 | 1975 | 0.42 | 64 | 990 | 13.07 | 34 | 1684 | 75.96 | 52 | 1003 | 80.18 | 34 | 1141 | 109.11 | 40 | | p09 | 6141 | 2.49 | 227 | 691 | 8.38 | 55 | 2032 | 524.17 | 73 | 1211 | 31.5 | 47 | 1833 | 123.34 | 62 | | p10 | 21113 | 24.29 | 845 | 1817 | 83.82 | 70 | 3550 | 108.58 | 131 | 1836 | 98.42 | 69 | 2512 | 132.92 | 91 | | p11 | 31871 | 20.48 | 1317 | 1869 | 111.29 | 69 | 4997 | 0.24 | 198 | 2001 | 87.12 | 76 | 4693 | 85.09 | 174 | | p12 | 61059 | 73.51 | 2481 | 2296 | 133.66 | 82 | 6034 | 0.39 | 222 | 3393 | 56.58 | 108 | 4470 | 162.98 | 157 | | p13 | 1429 | 0.39 | 52 | 1054 | 1.86 | 35 | 2723 | 0.07 | 69 | 1031 | 70.48 | 39 | 1632 | 14.26 | 54 | | p14 | 4098 | 2.01 | 56 | 1287 | 5.57 | 44 | 3551 | 19.66 | 101 | 1073 | 117.8 | 40 | 2277 | 34.43 | 64 | | p15 | 6316 | 6.61 | 165 | 2201 | 17.66 | 60 | 3904 | 542.81 | 97 | 1899 | 67.74 | 60 | 2549 | 19.86 | 82 | | p16 | 4937 | 1.38 | 121 | 1286 | 7.87 | 49 | 3026 | 412.28 | 92 | 1173 | 64.8 | 48 | 2155 | 61.27 | 67 | | p17 | 4962 | 25.88 | 156 | 1532 | 21.01 | 54 | 2429 | 0.7 | 97 | 1591 | 102.12 | 58 | 2130 | 264.08 | 83 | | p18 | 2644 | 11.81 | 75 | 930 | 11.14 | 33 | 1349 | 235.7 | 49 | 868 | 11.78 | 33 | 1093 | 213.57 | 38 | | p19 | 11657 | 29.78 | 370 | 3131 | 62.02 | 94 | 6479 | 0.57 | 227 | 2540 | 104.78 | 91 | 5268 | 252.02 | 146 | | p20 | 20682 | 30.14 | 797 | 2211 | 143.39 | 90 | 5982 | 0.83 | 190 | 3073 | 96.64 | 112 | 5369 | 283.23 | 166 | For the Transport domain, yahsp3, mercury and dae yahsp are the best three tools in IPC2014. When running yahsp3, it is able to give a quick plan in a short time. However, it will further take a long time to improve the plan. Sometimes S-TSolver(S-T) takes more time than mercury because of the overhead in analyzing the spatio-temporal SCK. Consider the plan cost, S-TSolver(T) produces plans with poor quality since a truck does not know where to go and just attempts to move randomly. The plan costs of S-TSolver(S-T) are much better than those of yahsp3 and dae yahsp, but in the same level with mercury. This is because the spatio-temporal SCK we use is a little coarse. As mentioned earlier, "nearest" path means the minimum steps from one location to another, not the length of roads in the path. For example, lsn-1 (e1, e2) is "nearer" than lsn (e1, e2). Although this is true in most situations, special cases may still occur that makes a "nearer" path has longer length. A potential way to solve it is to add data field in the model of our logic. As an example, l0 ↦→ { (d1, l1), (d2, l2) } not only denotes the link between l0 and l1 (l0 and l2), but also the data property d1 (d2), e.g. length, of the link. As a summary, our approach is helpful in finding plans of good quality and speeding up planning for the domains with both temporal and spatial constraints. ## 7 Conclusion In this paper, an expressive two-dimensional logic PPTL SL is formalized for specifying both spatial and temporal dimensions of SCK. Satisfiability of PPTL SL is proved decidable based on an equisitisfiable translation from PPTL SL to RPPTL SL . Based on it, a planner is implemented and evaluated on two benchmark domains. Experiments demonstrate that our method prunes substantial irrelevant search space and finds plans of good quality. In the future, we plan to do more experiments on the planning domains (e.g. Tidybot-IPC2011, TPP-IPC2006, and DriverLog-IPC2002 etc.) that are suitable for spatio-temporal SCK. Also, we would like to adopt the advanced heuristic algorithms in order to further improve efficiency of the tool. Another research direction is to relate our work to other study that has a richer notion of space, e.g. first-order theories of spatio-temporal change such as [Hazarika, 2005]. ## References 1. [Bacchus and Kabanza, 2000] Fahiem Bacchus and Frodu- ald Kabanza. Using temporal logics to express search control knowledge for planning. Artificial Intelligence, 116(1):123-191, 2000. 2. [Barrett et al., 2009] Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modu- lo theories. In Handbook of Satisfiability, pages 825-885. 2009. 3. [Barrett et al., 2010] Clark Barrett, Pascal Fontaine, and Ce- sare Tinelli. The smt-lib standard version 2.6. 2010. 4. [Belouaer and Maris, 2010] Lamia Belouaer and Frédéric Maris. Smt spatio-temporal planning. nd Int, 209:6, 2010. 5. [Boukharrou et al., 2015] Radja Boukharrou, Jean-Michel Ilié, and Djamel Eddine Saïdouni. Spatio-temporal plan- ning for mobile ambient agents. Procedia Computer Sci- ence, 56:96-103, 2015. 6. [Brochenin et al., 2012] Rémi Brochenin, Stéphane Demri, and Etienne Lozes. On the almighty wand. Information and Computation, 211:106-137, February 2012. 7. [Calcagno et al., 2005] Cristiano Calcagno, Philippa Gard- ner, and Matthew Hague. From separation logic to first- order logic. In Vladimiro Sassone, editor, FOSSACS, vol- ume 3441 of Lecture Notes in Computer Science, pages 395-409, Edinburgh, UK, April 4-8 2005. Springer Berlin Heidelberg. 8. [Chrpa and Barták, 2016] Lukáš Chrpa and Roman Barták. Guiding planning engines by transition-based domain con- trol knowledge. In Fifteenth International Conference on the Principles of Knowledge Representation and Reason- ing, 2016. 9. [De Moura and Bjørner, 2008] Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In In- ternational conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. 10. [Duan et al., 2008] Zhenhua Duan, Cong Tian, and Li Zhang. A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica, 45(1):43-78, 2008. 11. [Duan, 1996] Zhenhua Duan. An Extended Interval Tempo- ral Logic and a Framing Technique for Temporal Logic Programming. PhD thesis, University of Newcastle upon Tyne, 1996. 12. [Fern et al., 2004] Alan Fern, Sung Wook Yoon, and Robert Givan. Learning domain-specific control knowledge from random walks. In ICAPS, pages 191-199, 2004. 13. [Fox and Long, 2003] Maria Fox and Derek Long. PDDL2.1: an extension to PDDL for expressing temporal planning domains. J. Artif. Intell. Res. (JAIR), 20:61-124, 2003. 14. [Georgievski and Aiello, 2015] Ilche Georgievski and Mar- co Aiello. Htn planning: Overview, comparison, and be- yond. Artificial Intelligence, 222:124-156, 2015. 15. [Ghallab et al., 2004] Malik Ghallab, Dana Nau, and Paolo Traverso. Automated planning: theory & practice. Elsevi- er, 2004. 16. [Haghighi et al., 2015] Iman Haghighi, Austin Jones, Zhao- dan Kong, Ezio Bartocci, Radu Grosu, and Calin Belta. Spatel: a novel spatial-temporal logic and its application- s to networked systems. In HSCC'15, Seattle, WA, USA, April 14-16, 2015, pages 189-198, 2015. 17. [Hazarika, 2005] Shyamanta M Hazarika. Qualitative spa- tial change: space-time histories and continuity. PhD the- sis, The University of Leeds, 2005. 18. [Huang et al., 1999] Yi-Cheng Huang, Bart Selman, Henry Kautz, et al. Control knowledge in planning: benefits and tradeoffs. In AAAI/IAAI, pages 511-517, 1999. 19. [Kvarnström and Magnusson, 2003] Jonas Kvarnström and Martin Magnusson. Talplanner in ipc-2002: Extensions and control rules. Journal of Artificial Intelligence Re- search, 20:343-377, 2003. 20. [Merz et al., 2003] Stephan Merz, Martin Wirsing, and Júlia Zappe. A spatio-temporal logic for the specification and refinement of mobile systems. In FASE 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, pages 87-101, 2003. 21. [Nau et al., 2003] Dana S Nau, Tsz-Chiu Au, Okhtay Ilgha- mi, Ugur Kuter, J William Murdock, Dan Wu, and Fusun Yaman. Shop2: An htn planning system. J. Artif. Intell. Res.(JAIR), 20:379-404, 2003. 22. [Reynolds, 2002] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th Annual IEEE Symposium on Logic in Computer Science, 2002., pages 55-74, Washington, DC, USA, 2002. IEEE Com- puter Society. 23. [Tian and Duan, 2008] Cong Tian and Zhenhua Duan. Propositional projection temporal logic, büchi automata and ω-regular expressions. In Manindra Agrawal, Ding- Zhu Du, Zhenhua Duan, and Angsheng Li, editors, Theory and Applications of Models of Computation, volume 4978 of Lecture Notes in Computer Science, pages 47-58, X- i'an, China, April 25-29 2008. Springer Berlin Heidelberg. 24. [Vallati et al., 2014] M Vallati, L Chrpa, and TL Mc- Cluskey. The eighth international planning competition. Description of Participant Planners of the Deterministic Track, 2014. 25. [Vallati et al., 2015] Mauro Vallati, Lukáš Chrpa, Marek Grzes, Thomas L McCluskey, Mark Roberts, and Scot- t Sanner. The 2014 international planning competition: Progress and trends. AI Magazine, 36(3):90-98, 2015. 26. [Yoon et al., 2008] Sungwook Yoon, Alan Fern, and Robert Givan. Learning control knowledge for forward search planning. Journal of Machine Learning Research, 9(Apr):683-718, 2008.