Planning for Temporally Extended Goals in Pure-Past Linear Temporal Logic (Extended Abstract)

1 Introduction

In AI Planning, a temporally extended goal is a (possibly complex) property that the state-trace induced by a plan has to satisfy. Planning for temporally extended goals has a long tradition in AI Planning, including pioneering work in the late '90s [Bacchus et al., 1996; Bacchus and Kabanza, 1996; Bacchus et al., 1997; Bacchus and Kabanza, 2000], work on planning via Model Checking [Cimatti et al., 1997; De Giacomo and Vardi, 1999; Giunchiglia and Traverso, 1999], and work on declarative and procedural constraints [Baier and McIlraith, 2006; Baier et al., 2008b]. Also, recent works focus on handling the subset of temporally extended goals defined by PDDL3 [Gerevini et al., 2009], interpreting them as preferences [Percassi and Gerevini, 2019], state-trajectory constraints [Bonassi et al., 2021; Bonassi et al., 2022b; Bonassi et al., 2024], or over action sequences [Bienvenu et al., 2011; Bonassi et al., 2022a].

∗Extended abstract of the paper [Bonassi et al., 2023b] published in ICAPS 2023.

†Views and opinions expressed here are of the author's own and are not representative of the Bank of Italy's official position.

In this scenario, a powerful formalism to express temporally extended goals is Linear-time Temporal Logic (LTL), which has been advocated as an excellent tool to express properties of processes in Formal Methods [Baier et al., 2008a]. Given that tasks in AI planning are inherently of finite nature, a finite-trace variant of LTL, namely LTLf , has often been employed [Bacchus and Kabanza, 1996; Baier and McIlraith, 2006; De Giacomo and Vardi, 2013]. Notably, an alternative to LTLf is the Pure-Past Linear Temporal Logic, or PPLTL [Lichtenstein et al., 1985], which has been attractive in expressing non-Markovian rewards in MDPs [Bacchus et al., 1996], normative properties in multi-agent systems [Fisher and Wooldridge, 2005; Knobbout et al., 2016; Alechina et al., 2018], explanations in dynamical systems [Sohrabi et al., 2011], synthesis specifications [Cimatti et al., 2020], or in the context of plan/goal recognition [Fraga Pereira et al., 2024]. PPLTL looks at the trace backward instead of forward as LTLf and does so by expressing properties on traces using past operators only. PPLTL and LTLf have the same expressive power, but translating a formula from one into the other (and vice versa) can be prohibitive since the best-known algorithms are 3EXPTIME [De Giacomo et al., 2020].

In this paper, we study the problem of planning for PPLTL temporally extended goals in deterministic domains. Similarly to planning for LTLf goals, which has already been studied in, e.g., [Baier and McIlraith, 2006; De Giacomo and Vardi, 2013; Torres and Baier, 2015], planning for PPLTL goals requires reaching a certain state satisfying the PPLTL goal, i.e., the state-trace produced to reach such a state satisfies the goal formula.

From the literature, it is well-known that LTL formulas have a fixpoint characterization that allows splitting any formula into a propositional formula to be checked at the current instant and a temporal formula to be checked at the next instant [Gabbay et al., 1980; Manna, 1982; Emerson, 1990]. This property has already been exploited in AI, e.g., in the MetateM approach [Barringer et al., 1989], and later by Bacchus and Kabanza [1996], one of the most influential work on planning for temporally extended goals. Analogously, when we consider PPLTL formulas, such a fixpoint characterization splits the formula into a propositional formula on the current instant and a temporal formula on the past to be checked at the previous instant. In this paper, similarly to what was done by [Bacchus et al., 1997] in the context of (factorized) MDPs with PPLTL rewards, we exploit the fixpoint characterization of PPLTL formulas to show that planning for PPLTL goals can be polynomially encoded into classical planning and without adding any spurious actions. The use of PPLTL is crucial to obtain such nice results, as encoding LTLf goals into classical planning problems results either in worst-case exponential encodings [Baier and McIlraith, 2006] or in encodings that include additional spurious actions significantly increasing the plan length [Torres and Baier, 2015].

Finally, we developed our approach in a tool called Plan4Past that can be used along with state-of-the-art classical planners and experimentally showed its practical effectiveness by comparing it against techniques for LTLf goals.

2 Classical Planning with Pure-Past Linear Temporal Logic Goals

We model a classical planning domain as a tuple D = ⟨F,A, Pre, Eff ⟩, where F is a set of fluents (i.e., a set of positive literals), A is a set of action labels, and Pre and Eff are two functions denoting the preconditions and effects of each action a ∈ A. A planning state s is a collection of atoms from F, meaning that f is true in s if f ∈ s and f is false in s otherwise. Both functions Pre and Eff take an action label a ∈ A as input and return a propositional formula over F and a set of conditional effects, respectively. A conditional effect is a pair c ▷ e, where c is a formula, and e is a set of literals. An action a can be applied in a state s only if Pre(a) holds true in s, and applying a in s induces a new state s′ , denoted with s[a], that is defined following the standard definition of conditional effects [R¨oger et al., 2014]. Intuitively, a conditional effect c ▷ e specifies that if the condition c holds in the current state, then the effect e needs to be applied.

A classical planning problem is a tuple Γ = ⟨D, s0,G⟩, where D is a domain model, s0 is the initial state, and G is a formula over F representing the goal to achieve. A solution to a planning problem Γ is a sequence of actions a ∈ A called plan π = a0, . . . , an-1 such that, when executed, induces a finite state-trace τ = s0, . . . , sn, where si satisfies Pre(a) and si+1 = s[a] for i = 0, . . . , n-1, and sn satisfies G.

Usually, G is a reachability goal as it represents a property that must hold in the final state. Many real-world scenarios require achieving more general goals than just reachability goals. In most cases, realistic goals require properties to hold over a sequence of planning states. These types of temporal goals, also called temporally extended goals, are often expressed using temporal logics on finite or infinite sequences of states. In particular, this paper focuses on temporally extended goals expressed in Pure-Past Linear Temporal Logic (PPLTL). PPLTL is the variant of LTLf that talks about the past instead of the future. Given a set P of propositions, PPLTL is defined as:

where p ∈ P, Y is the yesterday operator and S is the since operator. PPLTL formulas are interpreted on finite nonempty traces, also called histories, τ = s0 · · · sn where si at instant i is a propositional interpretation over the alphabet 2P . We define the satisfaction relation τ, i |= φ, stating that φ holds at instant i, as follows:

• τ, i |= p iff p holds in si (for p proposition);
• τ, i |= ¬φ iff τ, i does not satisfy φ;
• τ, i |= φ1 ∧φ2 iff both φ1 and φ2 hold at instant i;
• τ, i |= Yφ iff φ held at the previous instant i - 1 with i ≥ 1. If i = 1, then Yφ is false.
• τ, i |= φ1 Sφ2 iff φ2 held at some previous instant k, and φ1 held in every subsequent instant j with k < j ≤ i.

The entire trace τ satisfies φ, denoted with τ |= φ, when φ holds in the last instant of τ. From the primitive PPLTL operators, one can easily derive other operators, such as φ1 ∨ φ2 ≡ ¬(φ1 ∧ φ2), the once operator Oφ ≡ true Sφ and the historically operator Hφ ≡ ¬O¬φ. Intuitively, Oφ specifies that φ held true sometimes in the past, while Hφ requires φ to always hold in each past state. We denote by sub(φ) the set of all subformulas of φ obtained from the syntax tree of φ [De Giacomo and Vardi, 2013].

If we specify planning goals using PPLTL, a planning problem becomes a tuple Γ = ⟨D, s0, φ⟩, where φ is a PPLTL goal formula. In the case of planning with a temporally extended goal φ, a plan π is a solution to Γ if the sequence of states τ = s0, . . . , sn induced by π satisfies φ. The following example shows two properties that are naturally expressed in PPLTL. Further examples can be found in Fuggitti [2023].

Example 1. The goal "We are now at location l1 and have passed through location l2" in PPLTL is l1 ∧O(l2). Another interesting property is "Every time I took the bus, I bought a new ticket beforehand", which translates as H(Bus =⇒ Y(¬Bus S T icket)) [De Giacomo et al., 2020].

3 Handling PPLTL Goals

Our approach exploits three main observations: (i) to evaluate the PPLTL goal formula we only need the truth value of its subformulas; (ii) every PPLTL formula can be put in a form where its evaluation depends only on the current state and the evaluation of a key set of PPLTL subformulas at the previous instant; (iii) one can recursively compute the value of such a small set of formulas and keep track of them with additional propositional variables in the state of the planning domain.

The well-known fixpoint characterization of LTL and variants [Gabbay et al., 1980; Manna, 1982; Emerson, 1990] is key to our approach. For PPLTL, such a fixpoint characterization splits the formula into a propositional formula on the current instant and a temporal formula on the past to be checked at the previous instant. In particular, PPLTL formulas can be decomposed into present and past components, given the fixpoint characterization of the since operator: ϕ1 Sϕ2 ≡ ϕ2∨(ϕ1∧Y(ϕ1 Sϕ2)). Exploiting this equivalence, the formula decomposition can be computed by recursively applying the following transformation function pnf(·):

• pnf(p) = p;
• pnf(Yϕ) = Yϕ;
• pnf(ϕ1 Sϕ2) = pnf(ϕ2) ∨ (pnf(ϕ1) ∧Y(ϕ1 Sϕ2));
• pnf(ϕ1 ∧ ϕ2) = pnf(ϕ1) ∧ pnf(ϕ2);
• pnf(¬ϕ) = ¬pnf(ϕ).

A formula resulting from the application of pnf(·) is in Previous Normal Form (PNF). Note that formulas in PNF have proper temporal subformulas (i.e., subformulas whose main construct is a temporal operator) appearing only in the scope of the Y operator. Also, observe that the formulas of the form Yϕ in pnf(φ) are such that ϕ ∈ sub(φ). It is easy to see that every PPLTL formula φ can be converted to its PNF form pnf(φ) in linear-time in the size of the formula (i.e., |sub(φ)|) and that pnf(φ) is equivalent to φ.

Example 2. As a running example, we use the formula φ = t ∧ ¬r Sm, which enforces scenarios where an agent finishes the task t without using the resource r since activating the machine m. The pnf of φ is:

Notably, the PNF transformation allows us to determine the truth value of a PPLTL formula by knowing the truth of some atomic propositions at the current instant and the truth of some key subformulas at the previous instant. In particular, the key subformulas that we need to consider are those appearing within the Y-scope in the PNF. Therefore, we interpret these specific subformulas as atomic propositions, denoting them with quotes, and collecting them in a set denoted as Σφ. These propositions are:

1. "Yϕ" for each subformula of φ of the form Yϕ;
2. "Y(ϕ1 Sϕ2)" for each subformula of φ of the form ϕ1 S ϕ2;

Example 3. For φ = t ∧ ¬r Sm we have Σφ = {"Y(¬r Sm)"}. Therefore, to evaluate φ, we only need to keep track of the subformula Y(¬r Sm) using the propositional variable "Y(¬r Sm)".

To evaluate the truth value of propositions in Σφ, we introduce the interpretation σ : Σφ → {⊤,⊥}, and characterize the evaluation of subformulas at a certain instant i ≤ n with σi. Intuitively, given an instant i, σi tells us which propositions related to the previous instant (i.e., in Σφ) are true at the instant i. Therefore, a PPLTL formula φ can be simply evaluated considering the propositional interpretation in the current instant i and the truth value assigned by σi to propositions related to the previous instant. We can easily do so by introducing an evaluation procedure denoted by val(φ, σi, si). Essentially, val(·) takes as input a PPLTL formula φ, the current interpretation si of the propositional symbols, and the current interpretation σi of the "Y(ϕ)" atoms, and evaluates the (propositional) formula obtained by swapping every Y(ϕ) with "Y(ϕ)" in the recursive computation of pnf(φ). An example of this procedure is shown below.

Example 4. We have that val(t ∧ ¬r Sm, si, σi) evaluates whether the formula:

holds true given the interpretations si and σi. For instance, val(t ∧ ¬r Sm, si, σi) is true when σi("Y(¬r Sm)") = ⊤ and si satisfy both t and ¬r.

Note that, the same procedure can be applied to determine val(ϕ, σi, si) for every subformula ϕ ∈ sub(φ). With this approach, we can use val(φ, σi, si) to capture the truth of φ at any instant i (i.e., val(φ, σi, si) is true iff τ, i |= φ). Clearly, computing val(·) for some instant i requires the interpretation σi. Luckily, given a trace τ = s0, s1, . . . sn, we can easily construct σi for every i ∈ {0, 1, . . . n} as follows. At the beginning of the trace, we know that, by definition of PPLTL, every formula of the form Y(ϕ) is false. Hence, we set σ0("Yϕ") .= ⊥ for each "Yϕ" ∈ Σφ, enabling the computation of val(ϕ, s0, σ0) for every ϕ ∈ sub(φ). Then, since Y(ϕ) holds at instant i iff ϕ holds at the previous instant i-1, we can iteratively set σi("Yϕ") .= val(ϕ, σi-1, si-1) for every i = {1, . . . n}. By doing so, we can evaluate any PPLTL formula at any instant i without considering the entire history produced so far.

4 Encoding PPLTL Goals in Planning

Intuitively, given a goal formula φ, we introduce a set of fresh atoms to keep track of the interpretation σ. Then, we simulate the construction of σi and the computation of val(φ, σi, si) for every instant i of the state trace as actions are applied. We do so by modifying the effect function and by employing axioms and derived predicates [Thi´ebaux et al., 2005]. Given a problem Γ = ⟨D, s0, φ⟩, in the following we describe how to encode Γ into Γ′ = ⟨D′ , s′0 , G′ ⟩, where G′ is a reachability goal, and D′ = ⟨F ′ ,X ′ ,A, Pre, Eff ′ ⟩ is the new planning domain extended with a set of axioms X ′ .

Fluents. F ′ contains the fluents of F, as well as one fluent for each proposition "Yϕ" in Σφ to keep track of propositional interpretations σi, and the set of predicates Pder defined below. Formally, F ′ = F ∪ Σφ ∪ Pder.

Axioms. We employ axioms to elegantly determine val(ϕ, σi, si) in every state si. Axioms have the form d ← ψ, where d ∈ Pder is a positive literal called derived predicate, and ψ is a propositional formula over a set of predicates. Let s be a state, axiom d ← ψ determines that the derived predicate d holds in s if and only if s |= ψ.

We include an axiom valϕ ← ψ for every subformula ϕ ∈ sub(φ), and Pder is defined as the set of all derived predicates valϕ, i.e., Pder = {valϕ | ϕ ∈ sub(φ)}. By mimicking the recursive computation of pnf(·), we get the following axioms:

• valp ← p;
• valYϕ ← "Yϕ";
• valϕ1 S ϕ2 ← (valϕ2 ∨ (valϕ1 ∧ "Y(ϕ1 S ϕ2)"));
• valϕ1∧ϕ2 ← (valϕ1 ∧ valϕ2 );
• val¬ϕ ←¬valϕ.

Clearly, we have that valϕ captures the evaluation of val(ϕ, σi, si). We add to D′ a set of axioms for every subformula ϕ in sub(φ), i.e., X ′ = {valϕ ← ϕ | ϕ ∈ sub(φ)}.

Initial State. The initial state assigns each fluent "Yϕ" ∈ Σφ to the truth value given by σ0. That is, s′0 = (σ0, s0).

Effects. The effect of every action is modified by adding a way to update the assignments of propositions in Σφ. For each "Yϕ" ∈ Σφ, we model the assignment σi("Yϕ") .= val(ϕ, σi-1, si-1) using two conditional effects of the form:

These effects specify that the fluent "Yϕ" is set to true (false, resp.) in the state si iff valϕ is true (false, resp.) in si-1. The effect of each action is extended with the same set of conditional effects. Formally, for all a ∈ A, Eff ′ (a) = Eff (a) ∪ {valϕ ▷ "Yϕ", ¬valϕ ▷ ¬"Yϕ" | "Yϕ" ∈ Σφ}.

Goal. The new goal is G′ = valφ. That is, we require the derived predicate associated with the original PPLTL goal formula φ to hold in the last instant.

The encoding is polynomially related to the original problem. In addition, every plan π for Γ is also a plan for Γ′ and vice versa, making the encoding sound and complete.

Theorem 1 (Bonassi et al. 2023b). Let Γ be a planning problem with a PPLTL goal φ, and Γ′ be the corresponding encoded planning problem. The size of Γ′ is polynomial in the size of Γ. In particular, the additional fluents introduced are linear in the size of the PPLTL goal φ of Γ. Moreover, every plan π is a plan for Γ iff π is a plan for Γ′ .

5 Experiments

This section briefly summarizes the experimental analysis presented in Bonassi et al. [2023b]. The novel approach has been implemented in a tool called Plan4Past (P4P), which is available at https://github.com/whitemech/Plan4Past.

The experimental analysis compares P4P with the two state-of-the-art compilations Exp [Baier and McIlraith, 2006] and Poly [Torres and Baier, 2015] for LTLf temporally extended goals. In particular, Exp explicitly uses NFAs to represent the LTLf formula, whereas Poly implicitly constructs the NFA for the goal formula. As a result, the Exp encoding is worst-case exponential in the size of the LTLf formula, while the Poly encoding remains polynomial in the size of the LTLf goal at the cost of a polynomial increase in the size of solution plans. On the other hand, the P4P encoding is polynomial in the size of the PPLTL goal and preserves the plan length.

We evaluated all compilation systems over a set of semantically equivalent LTLf and PPLTL goals. In total, our benchmark suite features 152 instances across the planning domains BLOCKSWORLD, ELEVATOR, ROVERS, and OPENSTACKS. The instances resulting from each compilation system were solved using the LAMA [Richter and Westphal, 2010] classical planner with runtime and memory limits of 1800s and 8GB, respectively.

Table 1 reports on the coverage (number of instances solved) of all compilations across all domains. We observe that P4P performs equally to or better than both Poly and Exp in all domains. In many cases, the Poly encoding forces LAMA to schedule many spurious actions after each original planning action taken. For example, the biggest instance of BLOCKSWORLD solved by Poly requires 6402 actions, of which 104 are actions of the original domain. Instead, the Exp encoding blows up during compilation or produces problems that cannot be handled by LAMA. The compilation time seems to be an issue for both LTLf compilations. Indeed, if we look at Figure 1 (right), P4P compiles 94.7% instances within 10s, while both Poly and Exp converge much more slowly. Figure 1 (left) displays the number of benchmark instances solved with a given timeout. All systems achieve their maximum coverage quite quickly, with P4P leaving the others well behind right after the start.

6 Conclusion

This paper summarizes the results presented in Bonassi et al. [2023b] on classical planning for PPLTL goals. In particular, our work shows that planning for PPLTL goals can be encoded into classical planning for reachability goals with minimal overhead and without increasing the plan length. Handling PPLTL goals is remarkably simple and elegant, given the direct mapping between the theoretical formulation and the encoding compilation without sacrificing efficiency. Moreover, we practically show that the novel encoding is able to solve a broader range of problems compared to the state-ofthe-art encodings for LTLf goals. Interestingly, the proposed encoding can be seamlessly extended to Fully Observable Non-Deterministic (FOND) planning domains [Bonassi et al., 2023a]. Also, our findings have already paved the way for the use of PPLTL in other applications, such as plan selection through natural language [Fuggitti and Chakraborti, 2023; Chakraborti et al., 2024], suggesting that PPLTL may definitely become a promising candidate to be the mainstream language to express temporal goals in planning. Future work concerns handling more expressive formalisms such as PurePast Linear Dynamic Logic (PPLDL) [De Giacomo et al., 2020], developing planners that can natively handle PPLTL goals, and exploring PPLTL-aware heuristics.

Acknowledgments

This work has been partially supported by the EU H2020 project AIPlan4EU (No. 101016442), the ERC-ADGWhiteMech (No. 834228), the EU ICT-48 2020 project TAILOR (No. 952215), the PRIN project RIPER (No. 20203FFYLK), and the PNRR MUR project FAIR (No. PE0000013).