Polynomial-Time Reformulations of LTL Temporally Extended Goals into Final-State Goals

1 Introduction

Linear Temporal Logic (LTL) [Pnueli, 1977] is a compelling language for the specification of goals in AI planning, because it allows defining constraints on state trajectories which are more expressive than simple final-state goals, such as "deliver priority packages before non-priority ones", or "while moving from the office to the kitchen, make sure door D becomes closed some time after it is opened". It was first proposed as the goal specification language of TLPlan system [Bacchus and Kabanza, 1998]. Currently, a limited but compelling subset of LTL has been incorporated into PDDL3 [Gerevini et al., 2009] for specifying hard and soft goals.

While there are some systems that natively support the PDDL3 subset of LTL [e.g., Coles and Coles, 2011], when planning for general LTL goals, there are two salient approaches: goal progression [Bacchus and Kabanza, 1998]

and compilation approaches [Rintanen, 2000; Cresswell and Coddington, 2004; Edelkamp, Jabbar, and Naizih, 2006; Baier and McIlraith, 2006]. Goal progression has been shown to be extremely effective when the goal formula encodes some domain-specific control knowledge that prunes large portions of the search space [Bacchus and Kabanza, 2000]. In the absence of such expert knowledge, however, compilation approaches are more effective at planning for LTL goals since they produce an equivalent classical planning problem, which can then be fed into optimized off-the-shelf planners.

State-of-the-art compilation approaches to planning for LTL goals exploit the relationship between LTL and finitestate automata (FSA) [Edelkamp, 2006; Baier and McIlraith, 2006]. As a result, the size of the output is worst-case exponential in the size of the LTL goal. Since deciding plan existence for both LTL and classical goals is PSPACE-complete [Bylander, 1994; De Giacomo and Vardi, 1999], none of these approaches is optimal with respect to computational complexity, since they rely on a potentially exponential compilation. From a practical perspective, this worst case is also problematic since the size of a planning instance has a direct influence on planning runtime.

In this paper, we present a novel approach to compile away general LTL goals into classical goals that runs in polynomial time on the size of the input that is thus optimal with respect to computational complexity. Like existing FSA approaches, our compilation exploits a relation between LTL and automata, but instead of FSA, we exploit alternating automata (AA), a generalization of FSA that does not seem to be efficiently compilable with techniques used in previous approaches. Specifically, our compilation handles each non deterministic choice of the AA with a specific action, hence leaving non-deterministic choices to be decided at planning time. This differs substantially from both Edelkamp's and Baier and McIlraith's approaches, which represent all runs of the automaton simultaneously in a single planning state.

We propose variants of our method that lead to performance improvements of planning systems utilizing relaxedplan heuristics. Finally, we evaluate our compilation empirically, comparing it against Baier and McIlraith's-who below we refer to as B&M. We conclude that our translation has strengths and weaknesses: it outperforms B&M's for classes of formulas that require very large FSA, while B&M's seems stronger for shallower, simpler formulas.

In the rest of the paper, we outline the required background, we describe our AA construction for finite LTL logic, and then show the details of our compilation approach. We continue describing the details of our empirical evaluation. We finish with conclusions.

2 Preliminaries

The following sections describe the background necessary for the rest of the paper.

2.1 Propositional Logic Preliminaries

Given a set of propositions F , the set of literals of F , Lit(F ), is defined as Lit(F) = F ∪ {¬p | p ∈ F}. The complement of a literal ℓ is denoted by ℓ, and is defined as ¬p if ℓ = p and as p if ℓ = ¬p, for some p ∈ F . L denotes {ℓ | ℓ ∈ L}.

Given a Boolean value function π : P → {false, true}, and a Boolean formula ϕ over P, π |= ϕ denotes that π satisfies ϕ, and we assume it defined in the standard way. To simplify notation, we use s |= ϕ, for a set s of propositions, to abbreviate πs |= ϕ, where πs = {p → true | p ∈ s}∪{p → false | p ∈ F \ s}. In addition, we say that s |= R, when R is a set of Boolean formulas, iff s |= r, for every r ∈ R.

2.2 Deterministic Classical Planning

Deterministic classical planning attempts to model decision making of an agent in a deterministic world. We use a standard planning language that allows so-called negative preconditions and conditional effects. A planning problem is a tuple 〈F,O, I,G〉, where F is a set of propositions, O is a set of action operators, I ⊆ F defines an initial state, and G ⊆ Lit(F ) defines a goal condition.

Each action operator a is associated with the pair (prec(a), eff (a)), where prec(a) ⊆ Lit(F) is the precondition of a and eff (a) is a set of conditional effects, each of the form C → ℓ, where C ⊆ Lit(F ) is a condition and literal ℓ is the effect. Sometimes we write ℓ as a shorthand for the unconditional effect {} → ℓ.

We say that an action a is applicable in a planning state s iff s |= prec(a). We denote by ρ(s, a) the state that results from applying a in s. Formally,

if s ∈ F and a is applicable in s; otherwise, δ(a, s) is undefined. If α is a sequence of actions and a is an action, we define ρ(s, αa) as ρ(δ(s, α), a) if ρ(s, α) is defined. Furthermore, if α is the empty sequence, then ρ(s, α) = s.

An action sequence α is applicable in a state s iff ρ(s, α) is defined. If an action sequence α = a1a2 . . . an is applicable in s, it induces an execution trace σ = s1 . . . sn+1 in s, where si = ρ(I, a1 . . . ai-1), for every i ∈ {1, . . . , n + 1}.

An action sequence is a plan for problem 〈F, O, I, G〉 if α is applicable in I and ρ(I, α) |= G.

2.3 Alternating Automata

Alternating automata (AA) are a natural generalization of non-deterministic finite-state automata (NFA). At a definitional level, the difference between an NFA and an AA is the transition function. For example, if A is an NFA with transition function δ, and we have that δ(q, a) = {p, r}, then this intuitively means that A may end up in state p or in state r as a result of reading symbol a when A was previously in state q. With an AA, transitions are defined as formulas. For example, if δ′ is the transition function for an AA A′ , then δ′ (q, a) = p ∨ r means, as before, that A′ ends up in p or r after reading an a in state q. Nevertheless, formulas provide more expressive power. For example δ′ (q, b) = (s ∧ t) ∨ r can be intuitively understood as A′ will end up in both s and t or (only) in r after reading a b in state q. In this model, only positive Boolean formulas are allowed for defining δ.

Definition 1 (Positive Boolean Formula) The set of positive formulas over a set of propositions P-denoted by B+(P)-is the set of all Boolean formulas over P and constants ⊥ and ⊤ that do not use the connective "¬".

The formal definition for AA that we use henceforth follows.

Definition 2 (Alternating Automata) An alternating automata (AA) over words is a tuple A = (Q, Σ, δ, I, F), where Q is a finite set of states, Σ, the alphabet, is a finite set of symbols, δ : Q×Σ → B+(Q) is the transition function, I ⊆ Q are the initial states, and F ⊆ Q is a set of final states.

As suggested above, any NFA is also an AA. Indeed, given an NFA with transition function δ, we can generate an equivalent AA with transition function δ′ by simply defining δ′ (q, a) = ∨p∈P p, when δ(q, a) = P. We observe that this means δ′ (q, a) = ⊥ when P is empty.

As with NFAs, an AA accepts a word w whenever there exists a run of the AA over w that satisfies a certain property. Here is the most important (computational) difference between AAs and NFAs: a run of an AA is a sequence of sets of states rather than a sequence of states. Before defining runs formally, for notational convenience, we extend δ for any subset T of Q as δ(T, a) = ∧q∈T δ(q, a) if T ̸= ∅ and δ(T, a) = ⊤ if T = ∅.

Definition 3 (Run of an AA over a Finite String) A run of an AA A = (Q,Σ, δ, I,F) over word x1x2 . . . xn is a sequence Q0Q1 . . .Qn of subsets of Q, where Q0 = I, and Qi |= δ(Qi-1, xi), for every i ∈ {1, . . . , n}.

Definition 4 A word w is accepted by an AA A iff there is a run Q0 . . . Qn of A over w such that Qn ⊆ F .

For example, if the definition of an AA A is such that δ′ (q, b) = (s ∧ t) ∨ r, and I = {q}, then both {q}{s, t} and {q}{r} are runs of A over word b.

2.4 Finite LTL

The focus of this paper is planning with LTL interpreted over finite state sequences [Baier and McIlraith, 2006; De Giacomo and Vardi, 2013]. At the syntax level, the finite LTL we use in this paper is almost identical to regular LTL, except for the addition of a "weak next" modality (ffl). The definition follows.

Definition 5 (Finite LTL formulas) The set of finite LTL formulas over a set of propositions P, fLTL(P), is inductively defined as follows:

• p is in fLTL(P), for every p ∈ P.

• If ϕ and ψ are in fLTL(P) then so are ¬ϕ, (ϕ ∧ ψ), (ϕ∨ψ), Ωϕ, fflϕ, (ϕUψ), and (ϕRψ).

The truth value of a finite LTL formula is evaluated over a finite sequence of states. Below we assume that those states are actually planning states.

Definition 6 Given a sequence of states σ = s0 . . . sn and a formula ϕ ∈ fLTL(P), we say that σ satisfies ϕ, denoted as σ |= ϕ, iff it holds that σ, 0 |= ϕ, where, for every i ∈ {0, . . . , n}:

1. σ, i |= p iff si |= p, when p ∈ P.
2. σ, i |= ¬ϕ iff σ, i ̸|= ϕ
3. σ, i |= ψ ∧χ iff σ, i |= ψ and σ, i |= χ
4. σ, i |= ψ ∨χ iff σ, i |= ψ or σ, i |= χ
5. σ, i |= Ωψ iff i < n and σ, (i + 1) |= ψ
6. σ, i |=fflψ iff i = n or σ, (i +1) |= ψ

7. σ, i |= ψUχ iff there exists k ∈ {i, ..., n} such that σ, k |= χ and for each j ∈ {i, ..., k - 1}, it holds that σ, j |= ψ

1. σ, i |= ψRχ iff for each k ∈ {i, ..., n} it holds that σ, k |= χ or there exists a j ∈ {i, ..., k - 1} such that σ, j |= ψ

We sometimes use the macros true def = p∨¬p, false def = ¬true, and ϕ → ψ as ¬ϕ ∨ ψ. Additionally, Ψϕ, pronounced as "eventually ϕ" is defined as true Uϕ, and Φϕ, pronounced as "always ϕ" is defined as ¬Ψ¬ϕ.

2.5 Deterministic Planning with LTL goals

A planning problem with a finite LTL goal is a tuple P = 〈F,O, I,G〉, where F, O, and I are defined as in classical planning problems, but where G is a formula in fLTL(F). An action sequence α is a plan for P if α is applicable in I, and the execution trace σ induced by the execution of α in I is such that σ |= G.

There are two approaches to compiling away LTL via nondeterministic finite-state automata [Edelkamp, Jabbar, and Naizih, 2006; Baier and McIlraith, 2006]. B&M's approach compiles away LTL formulas exploiting the fact that for every finite LTL formula ϕ it is possible to build an NFA that accepts the finite models of ϕ. To illustrate this, Figure 1 shows an NFA for Φ(p → ΩΨq). B&M represent the NFA within the planning domain using one fluent per automaton state. In the example of Figure 1, this means that the new planning problem contains fluents Eq1 and Eq2 . The translation is such that if α is a sequence of actions that induces the execution trace σ = s1 . . . sn, then Eq is true in sn iff there is some run of the automaton over σ that ends in state q. B&M's translation has the following property.

Theorem 1 (Follows from [Baier, 2010]) Let P be a classical planning problem, ϕ be a finite LTL formula, and P ′ be the instance that results from applying the B&M translation to P. Moreover, let α be a sequence of actions applicable in the initial state of P, and let σ be the sequence of (planning) states induced by the execution of α in P ′ . Finally, let Aϕ be the NFA for ϕ. Then the following are equivalent statements.

1. There exists a run ρ of Aϕ ending in q.
2. Eq is true in the last state of σ.

As a corollary of the previous theorem, one obtains that satisfaction of finite LTL formulas can be determined by checking whether or not the disjunction ∨f∈F Ef holds, where F denotes the set of final states of Aϕ.

Unfortunately, B&M's translation is worst-case exponential [Baier, 2010]; for example, an NFA for ∧ni=1Ψpi has 2n states. Baier [2010] proposes a formula-partitioning technique that allows the method to generate more compact translations for certain formulas. The method, however, is not applicable to any formula.

Edelkamp's approach is similar to B&M's: it builds a B¨uchi automaton (BA), whose states are represented via fluents, compactly representing all runs of the automaton in a single planning state. The main difference is that the state of the automaton is updated via specific actions-a process that they call synchronized update. We modify this idea in the compilation we give below; however, our compilation is significantly different since it does not represent all runs of the automaton in the same planning state. It is important to remark that the use of BA interpreted as NFA does not yield a correct translation for general LTL goals, although it is correct for the PDDL3 subset of LTL [De Giacomo, Masellis, and Montali, 2014].

3 Alternating Automata and Finite LTL

A central part of our approach is the generation of an AA from an LTL formula. To do this we modify Muller, Saoudi, and Schupp's AA [1988] for infinite LTL formulas. Our AA is equivalent to a recent proposal by De Giacomo, Masellis, and Montali [2014]. The main difference between our construction and De Giacomo, Masellis, and Montali's is that we do not assume a distinguished proposition becomes true only in the final state. On the other hand, we require a special state (qF ) that indicates the sequence should finish. The use of such a state is the main difference between our AA for finite LTL and Muller, Saoudi, and Schupp's AA for infinite LTL.

We require the LTL input formula to be written in negation normal form (NNF); i.e., a form in which negations can be applied only to atomic formula. This transformation can be done in linear time [Gerth et al., 1995].

Let ϕ be in fLTL(S) and sub(ϕ) be the set of the subformulas of ϕ, including ϕ. We define Aϕ = (Q, 2S , δ, qϕ, {qF}), where Q = {qα | α ∈ sub(ϕ)}∪{qF}

and:

Theorem 2 Given an LTL formula ϕ and a finite sequence of states σ, Aϕ accepts σ iff σ |= ϕ.

Proof sketch: Suppose that σ = x1x2 . . . xn ∈ Σ∗ , where Σ = 2S . The proof of the theorem is straightforward from the following lemma: ϕ: σ, i |= ϕ if and only if there exists a sequence r = Qi-1Qi . . .Qn, such that: (1) Qi-1 = {qϕ}, (2) Qn ⊆ {qF}, (3) For each subset Qj in the sequence r it holds that Qj ⊆ sub(ϕ) ∪ {qF } and (4) For each j ∈ {i, i + 1, . . . , n} it holds that Qj |= δ(Qj-1, xj). The proof for the lemma follows. It is inductive on the construction of ϕ.

• ⇒) Suppose that σ, i |= ϕ. To prove this direction, it suffices to provide a sequence r = Qi-1Qi . . . Qn satisfying the aforementioned properties. Below we show each sequence. We do not show that they satisfy the four properties; we leave this as an exercise to the reader.

Suppose that the lemma holds for any ϕ with less than m operators and that for any α and β with less than m operators, their respective sequences are r′ = Q′i-1Q′iQ′′ i+1 . . .Q′n and r′′ = Q′′ i-1Q′′ i Q′′ i+1 . . .Q′′n . Now, let ϕ be a formula with m operators:

• ϕ = α ∨ β. Then σ, i |= α or σ, i |= β. Without loss of generality, suppose that σ, i |= α. Then r = ({qϕ}, Q′i , Q′i+1 , . . . , Q′n ).
• ϕ = α ∧ β. Then r = ({qϕ}, (Q′i ∪ Q′′ i ), (Q′i+1 ∪ Q′′ i+1 ), . . . , (Q′n ∪ Q′′n ).
• ϕ = Ωα. Then σ, (i+1) |= α. In this case, the sequence for α is r′ = Q′iQ′′ i+1 . . .Q′n . With this, the sequence r for Ωα is r = ({qϕ}, {qα}, Q′′ i+1 , . . . , Q′n ).
• ϕ = fflα. Then i = n or σ, (i + 1) |= α. If i = n, the sequence r = (Qn-1,Qn) = ({qϕ}, {qF}). If i < n, consider the same sequence r for the case Ωα.
• ϕ = αUβ. Then, there exists k ≥ i such that σ, k |= β and for every j ∈ {i, . . . , k - 1} it holds that σ, j |= α. For β, assume its sequence is rk = (Qkk-1 , Qkk , . . . , Qkn ) and for each α that is satisfied by σ, j, assume its sequence is rj = (Qjj-1 ,Qjj , . . . ,Qjn ). The sequence r = Qi-1Qi . . . Qn is given by:

• ϕ = αRβ. Then, for each k ∈ {i, . . . , n} it holds that σ, k |= β or there exists a j ∈ {i, . . . , k - 1} such that σ, j |= α. If there is no such j, then σ, k |= β for every k ∈ {i, . . . , n} and for each one of them, assume their sequence will correspond to rk = (Qkk-1 , Qkk , . . . , Qkn ). The sequence r = Qi-1Qi . . . Qn is given by:

If there is a j ∈ {i, . . . , k - 1} such that σ, j |= α, consider the minimum such j and assume its sequence is r′ = (Aj-1,Aj, . . . ,An). For k ∈ {i, . . . , j}, the sequences for β will be rk = (Bk k-1 , Bk k , . . . ,Bkn ). The sequence r = Qi-1Qi . . . Qn is given by:

⇐) Suppose that there exists a sequence r = Qi-1Qi . . .Qn for ϕ that satisfies the four properties. To prove that σ, i |= ϕ, it should be straightforward for ϕ = ℓ. For the inductive steps, where α is a direct subformula of ϕ, the sequence r must be used to create a new sequence r′ for α (ensuring that r′ satisfies the four properties) and use the implication of σ, i |= α. This finishes the proof for the lemma. ■

4 Compiling Away finite LTL Properties

Now we propose an approach to compiling away finite LTL properties using the AA construction described above.

First, we argue that the idea underlying both Edelkamp's and B&M's translations would not yield an efficient translation if applied to AA. Recall in both approaches if Eq1 , . . . ,Eqn are true in a planning state s, then there are n runs of the automaton, each of which ends in q1, . . . , qn (Theorem 1). In other words, the planning state keeps track of all of the runs of the automaton. To apply the same principle to AA, we would need to introduce one fluent for each subset of states of the AA, therefore generating a number of fluents exponential on the size of the original formula. This is because runs of AA are sequences of sets of states, so we would require states of the form ER, where R is a set of states.

To produce an efficient translation, we renounce the idea of representing all runs of the automaton in a single planning state. Our translation will then only keep track of a single run.

4.1 Translating LTL via LTL Synchronization

Our compilation approach takes as input an LTL planning problem P and produces a new planning problem P ′ , which is is like P but contains additional fluents and actions. Like previous compilations, AG is represented in P ′ with additional fluents, one for each state of the automaton for G. Like in Edelkamp's compilation P ′ contains specific actionsbelow referred to as synchronization actions-whose only purpose is to update the truth values of those additional fluents. A plan for P ′ alternates one action from the original problem P with a number of synchronization actions. Unlike any other previous compilation, P ′ does not represent all possible runs of the automaton in a single planning state.

Synchronization actions update the state of the automaton following the definition of the δ function. The most notable characteristic that distinguishes synchronization from the Edelkamp' s translation is that non-determinism inherent to the AA is modeled using alternative actions, each of which represents the different non-deterministic options of the AA. As such if there are n possible non-deterministic choices, via the applications of synchronization actions there will be n reachable planning states, each representing a single run.

Given a planning problem P = 〈F,O, I,G〉, our translation generates a problem P ′ in which there is one (new) fluent q for each state q of the AA AG. The compilation is such that the following property holds: if α = a1a2 . . . an is applicable in the initial state of P, then there exists a set Aα of action sequences of the form α0a1α1a2α2 . . . anαn, where each αi is a sequence of synchronization actions whose sole objective is to update the fluents representing AG's state.

Our theoretical result below says that our compilation can represent all runs, but only one run at a time. Specifically, each of the sequences of Aα corresponds to some run of AG over the state sequence induced by α over P. Moreover, if α′ ∈ Aα, Eq is true in the state resulting from performing sequence α′ in P ′ iff q is contained in the last element of a run that corresponds to α′ .

We we are ready to define P ′ . Assume the AA for G has the form AG = (Q, Σ, δ, q0, {qf }).

Fluents P ′ has the same fluents as P plus fluents for the representation of the states of the automaton (Q), flags for controlling the different modes (copy, sync, world), and a special fluent ok, which becomes false if the goal has been falsified. Finally, it includes the set QS = {qS | q ∈ Q} which are "copies" of the automata fluents, which we describe in detail below. Formally, F ′ = F ∪ Q ∪ QS ∪ {copy, sync, world, ok}.

The set of operators O′ is the union of the sets Ow and Os.

World Mode Set Ow contains the same actions in O, but preconditions are modified to allow execution only in "world mode". Effects, on the other hand are modified to allow the execution of the copy action, which initiates the synchronization phase, and which is described below. Formally, Ow = {a′ | a ∈ O}, and for all a′ in Ow:

Synchronization Mode The synchronization mode can be divided in three consecutive phases. In the first phase, we execute the copy action which in the successor states adds a copy qS for each fluent q that is currently true, deleting q. Intuitively, during synchronization, each qS defines the state of the automaton prior to synchronization. The precondition of copy is simply {copy, ok}, while its effect is defined by:

As soon as the sync fluent becomes true, the second phase of synchronization begins. Here the only executable actions are those that update the state of the automaton, which are defined in Table 1. Note that one of the actions deletes the ok fluent. This can happen, for example while synchronizing a formula that actually expresses the fact that the action sequence has to conclude now.

When no more synchronization actions are possible, we enter the third phase of synchronization. Here only action world is executable; its only objective is to reestablish world mode. The precondition of world is {sync, ok} ∪ QS , and its effect is {world, ¬sync}.

The set Os is defined as the one containing actions copy, world, and all actions defined in Table 1.

New Initial State The initial state of the original problem P intuitively needs to be "processed" by AG before starting to plan. Therefore, we define I ′ as I ∪ {qG, copy, ok}.

NewGoal Finally, the goal of the problem is to reach a state in which no state fluent in Q is true, except for qf , which may be true. Therefore, we define G′ = {world, ok} ∪ (Q \ {qF }).

4.2 Properties

There are two important properties that can be proven about our translation. First, our translation is correct.

Theorem 3 (Correctness) Let P = 〈F,O, I,G〉 be a planning problem with an LTL goal and P ′ = 〈F ′ ,O′ , I ′ ,G′ 〉 be the translated instance. Then P has a plan a1a2 . . . an iff P ′ has a plan α0a1α1a2α2 . . . anαn, in which for each i ∈ {0, . . . , n}, αi is a sequence of actions in Os.

Proof sketch: We show each sequence of actions αi simulates the behavior of the automata, i.e., whenever t is a planning state whose next action must be copy and qβ ∈ t, then ρ(t, αi) satisfies δ(qβ, t).

For this, let's define tS as the subset of all the automata fluents QS that are added during the execution of the sequence of actions αi. We will prove the following lemma by induction on the construction of ϕ: If qS ϕ ∈ tS , then ρ(t, αi) |= δ(qϕ, t): Observe that if qS ϕ ∈ tS , then there must be an action trans(qS ϕ ) that was executed in αi. This is because ρ(t, αi) ∩ QS = ∅ and only trans(qS ϕ ) can delete qS ϕ from the current state. The second observation is: If some action trans adds qS α , then qS α ∈ tS . This is by definition of tS . If the action adds qψ, then qψ ∈ ρ(t, αi), because the only action that deletes fluents in Q is copy.

• ϕ = ℓ. Assume ℓ is positive literal. Then there is a planning state s in which trans(qS ℓ ) was executed. Since the precondition requires ℓ ∈ s and ℓ can only be added by an action from Ow, then ℓ ∈ t. By definition, δ(qℓ, t) = ⊤, and it is clear that ρ(t, αi) |= δ(qϕ, t). The argument is analogous for a negative literal ℓ.

We will not consider the case for qF . It is never desirable to synchronize that state, because the special fluent ok is removed, leading to a dead end. Now, assume that qS ϕ ∈ tS implies ρ(t, αi) |= δ(qϕ, t) for every ϕ with less than m operators. The proof sketch for each case can be verified by the reader as follows:

• For each ϕ, it is clear that a version of trans(qS ϕ ) is executed due to the first observation.
• If qψ is added by trans, then qψ ∈ ρ(t, αi) due to the second observation. This implies that ρ(t, αi) |= qψ.
• If qS α is added by trans, then qS α ∈ tS . By induction hypothesis, ρ(t, αi) |= δ(qα, t), because α is a strict subformula of ϕ and has less than m operators.
• Finally, using entailment (for positive boolean formulae) and the definition of the transitions for the alternating automata Aϕ, it can be verified that ρ(t, αi) |= δ(qϕ, t).
• The argument is similar for the other versions of trans.

To conclude our theorem, note that if t is a planning state, qβ ∈ t and the next action to execute is copy, then qS β ∈ tS . Using the lemma, this implies ρ(t, αi) |= δ(qϕ, t). ■

Second, the size of the plan for P ′ is linear on the size of the plan for P .

Theorem 4 (Bounded synchronizations) If T is a reachable planning state from I ′ and T ∩QS ̸= ∅, then there is a sequence of trans actions σ such that δ(T, copy ·σ)∩QS = ∅ and |σ| ∈ O(|G|).

Proof: Note that T is a state in world mode getting ready to go into synchronization mode after the copy action has been executed. The main idea of the proof is to choose the order of the subformulae to be synchronized, where the first one corresponds to the largest subformula of the current state, the second one corresponds to the second largest subformula and so on. Note that when an action trans(qS α ) is executed, it always happens that at most two fluents qS β and qS γ are added, and the formulae β and γ are strict subformulae of α. This means that a subformula will never get synchronized twice in a single synchronization phase σ. Since the number of subformulae is linear on |G|, this means that the length of σ must be O(|G|). ■

4.3 Towards More Efficient Translations

The translation we have presented above can be modified slightly for obtaining improved performance. The following are modifications that we have considered.

An Order for Synchronization Actions Consider the goal formula is α ∧ β and that currently both qα and qβ are true. The planner has two equivalent ways of completing the synchronization: by executing first trans(qα) and then trans(qβ), or by inverting this sequence. By enforcing an order between these synchronizations, we can reduce the branching factor at synchronization phase. Such an order is simple to enforce by modifying preconditions and effects of synchronization actions so that states are synchronized following a topological order of the parse tree of G.

PositiveGoals The goal condition of the translated instance requires being in and every q ∈ Q to be false. On the other hand, action copy, which has to be performed after each world action, has precisely the effect of making every q ∈ Q false. This may significantly hurt performance if search relies on heuristics that relax negative effects of actions, like the FF heuristic [Hoffmann and Nebel, 2001], which is key to the performance of state-of-the-art planning systems [Richter and Helmert, 2009]. To improve heuristic guidance, we define a new fluent qD , for each q ∈ Q, with the intuitive meaning that qD becomes true when trans(q) cannot be executed in the future. For every action trans(qS α ) that does not add qα, we include the conditional effect {qβ | β ∈ super(α)} → qD α , where super(α) is the set of subformulas of G that are proper superformulas of α. Using a function f that takes a fLTL(F) formula and generates a propositional formula, the new goal f(G) can be recursively written as follows:

• If ϕ = p and p ∈ Lit(F), then f(p) = qD p .
• If ϕ = α∧ β, then f(ϕ) = qD ϕ ∧ f(α) ∧ f(β)
• If ϕ = α∨ β, then f(ϕ) = qD ϕ ∧ (f(α) ∨ f(β))
• If ϕ = Ωβ or ϕ =fflβ, then f(ϕ) = qD ϕ ∧ f(β)
• If ϕ = α⋆β, where ⋆ ∈ {U, R}, then f(ϕ) = qD ϕ ∧f(β)

5 Empirical Evaluation

The objective of our evaluation was to compare our approach with existing translation approaches, over a range of general LTL goals, to understand when it is convenient to use one or other approach. We chose to compare to B&M's rather than Edelkamp's because the former seems to yield better performance [Baier, Bacchus, and McIlraith, 2009]. We do not compare against other existing systems that handle PDDL3 natively, such as LPRPG-P [Coles and Coles, 2011], because efficient translations for the (restricted) subset of LTL of PDDL3 into NFA are known [Gerevini et al., 2009].

We considered both LAMA [Richter, Helmert, and Westphal, 2008] and FFX [Thi´ebaux, Hoffmann, and Nebel, 2005], because both are modern planners supporting derived predicates (required by B&M). We observed that LAMA's preprocessing times where high, sometimes exceeding planning time by 1 to 2 orders of magnitude, and thus decided to report results we obtained with FFX . We used an 800MHzCPU machine running Linux. Processes were limited to 1 GB of RAM and 15 min. runtime.

There are no planning benchmarks with general LTL goals, so we chose two of the domains (rovers and openstacks) of the 2006 International Planning Competition, which included Openstacks Domain LTL preferences (but not goals), and generated our own problems, with some of our goals inspired by the preferences. In addition, we considered the blocksworld domain.

Our translator was implemented in SWI-Prolog. It takes a domain and a problem in PDDL with an LTL goal as input and generates PDDL domain and problem files. It also receives an additional parameter specifying the translation mode which can be any of the following: simple, OSA, PG, and OSA+PG, where simple is the translation of Section 4, and OSA, PG are the optimizations described in Section 4.3. OSA+PG is the combination of OSA and PG.

Table 2 shows a representative selection of the results we obtained. It shows translation time (TT), plan length (PL), planning time (PT), the number of planning states that were evaluated before the goal was reached (PS). Times are displayed in seconds. For our translators we also include the length of the plan without synchronization actions (WPL). NR means the planner/translator did not return a plan. For each problem, a special name of the form x0n was assigned, where x corresponds to a specific family of formula and n its parameter (i.e. For the problem a04, the goal formula α ∪ ∧ni=1 βi was used, with n = 4).

Each family of formulae corresponds to: a: α ∪ ∧ni=1 βi, b: ∨ni=1 Ψpi UΨq, c: Ψ(α ∧ ∧ni=1 Ψβi), d: ∧ni=1 (αUβi), e: Ψ(∧ni=1 Ψβi), f : ∧ni=1 Ψpi, g: ∧3i=1 Ψpi ∧ ∧n-3 i=1 qi Uri, h: αUβ, where α or β has n nested operators U or R, i: Ψ(∨ni=1 Ψβi) and j: Ψ(∨ni=1 Φβi).

We observe mixed results. B&M yields superior results on some problems; e.g., f03 and f05 of openstacks (of the form ∧ni=1 Ψpi). The performance gap is probably due to the fact that (1) the B&M problem requires fewer actions in the plan and (2) B&M's output for these goals is quite compact on the size of the formula. On the other hand, there are other goal formulas in which our approach outperforms B&M. For example, problems of the form a0n in openstacks and blocksworld, and of the form b0n in blocksworld. In those cases, the B&M translator is forced to generate the whole automaton, because it has to deal with nested subformulae in which the distributive property does not hold. As a consequence, B&M generates an output exponential in n, which results in higher translation time and eventually in the the planner running out of memory.

By observing the rest of the data, we conclude that B&M returns an output that is significantly larger than our approaches for the following classes of formulas: αU(∧ni=1 Ψβi), αU(∧ni=1 βi Uγi), (∨ni=1 Φαi)Uβ, and (∨ni=1 αi Rβi)Uβ, with n ≥ 4, yielding finally an "NR". Being polynomial, our translation handles these formulas reasonably well: low translation times, and a compact output. In many cases, this allows the planner to return a solution.

The use of positive goals has an important influence in performance possibly because the heuristic is more accurate, leading to fewer expansions. OSA, on the other hand, seems to negatively affect planning performance in FFX . The reason is the following: FFX will frequently choose the wrong synchronization action and therefore its enforced hill climbing algorithm will often fail. This behavior may not be observed in planners that use complete search algorithms.

6 Conclusions

We proposed polynomial-time translations of LTL into finalstate goals, which, unlike existing translations are optimal with respect to computational complexity. The main difference between our approach and state-of-the-art NFA-based translations is that we use AA, and represent a single run of the AA in the planning state. We conclude from our experimental data that it seems more convenient to use an our AA translation precisely when the output generated by the NFA-based translation is exponentially large in the size of the formula. Otherwise, it seems that NFA-based translations are more efficient because they do not require synchronization actions, which require longer plans, and possibly higher planning times. Obviously, a combination of both translation approaches into one single translator should be possible. Investigating such a combination is left for future work.

Acknowledgements

We thank the anonymous reviewers and acknowledge funding from the Millennium Nucleus Center for Semantic Web Research under Grant NC120004, and from Fondecyt Grant 1150328, both from the Republic of Chile.