Strong Fully Observable Non-Deterministic Planning with LTL and LTLf Goals

1 Introduction

We are concerned with the synthesis of strategies in discrete, dynamical environments that are fully observable and where the outcomes of actions are non-deterministic (FOND). FOND planning provides a computational core for many applications and sequential decision-making problems including two-player games, web-service composition, and the synthesis of controllers for devices and systems. In FOND planning, two classes of solutions are commonly considered: strong solutions guarantee eventual satisfaction of the goal, whereas in strong-cyclic solutions such guarantee is predicated on the assumption that the dynamics of the system is fair (e.g., [Cimatti et al., 2003]).

The focus of this paper is on the development of algorithms for the synthesis of solutions to FOND planning with temporally extended goals - in particular, strong solutions. Different languages have been used for the specification of temporally extended goals in planning. In this paper, we follow on recent work in so-called LTL FOND and LTLf FOND planning that use Linear Temporal Logic (LTL) and LTL interpreted over finite traces (LTLf ), respectively (e.g. [Patrizi et al., 2013; Camacho et al., 2017;

De Giacomo and Rubin, 2018; Camacho et al., 2019]). Our techniques complement early work on FOND planning with temporally extended goals expressed in CTL [Pistore et al., 2001]. Note, CTL and LTL are non-equivalent languages, although both can be transformed into automata. Our techniques exploit automata transformations of the goal specification, and can therefore be extended for use with any goal specification language that can be transformed into automata - e.g. PSL, CTL, Past LTL (PLTL), and (finite) Linear Dynamic Logic (LDLf ) [De Giacomo and Vardi, 2013], as well as PDDL3.0 temporal operators [Gerevini et al., 2009].

The complexity of LTL FOND and LTLf FOND planning is now well understood [De Giacomo and Rubin, 2018; Camacho et al., 2019]. The latter paper provides a clear correspondence with LTL synthesis and game structures, and identifies fragments of LTL and LTLf for which planning can be done more efficiently. Despite increasing interest in the area, the number of algorithmic approaches to LTL FOND and LTLf FOND planning remains limited. To date, existing tools have focused on the computation of strong-cyclic solutions whose validity is predicated on the fairness assumption (cf. Table 1). The synthesis of strong solutions had remained elusive, and is the focus of this paper.

We provide the first algorithmic approach to strong LTL FOND and LTLf FOND planning. Our approach exploits automata transformations of the goal formula, and compiles the problem into a standard goal-oriented FOND planning problem that can be solved with off-the-shelf planners. We further provide an analysis of the different sources of algorithmic complexity. Whereas we adopt LTL and LTLf as goal specification languages, our techniques can be extended to any language that can be transformed into automata. This includes PSL, CTL, PLTL, LDLf , and PDDL3.0 temporal operators.

Our algorithms have been implemented and evaluated empirically. Experiments demonstrate the effectiveness of our approach to computing strong solutions. They also suggest that assuming fairness and computing strong-cyclic solutions via existing approaches can ease the burden of computation.

2 Preliminaries

2.1 Linear Temporal Logic

Linear Temporal Logic (LTL) over a finite set of atomic propositions AP extends propositional logic with temporal operators next ( ) and until (U). Namely,

where p ∈ AP. Other operators are usually considered, such as eventually (♦ϕ := ⊤Uϕ) and always (□ϕ := ¬♦¬ϕ). LTL was initially conceived for model checking of properties of logical circuits [Pnueli, 1977], and over the years it has been used in a myriad of applications: from specification language for the synthesis of programs [Pnueli and Rosner, 1989], to goal specification language for automated planning [Bacchus and Kabanza, 1998]. In automated planning in particular, variants of LTL interpreted over finite traces have been widely studied. Here, we use LTLf . The syntax of LTLf is the same as for LTL, and differs in the semantics.

A finite trace ρ = s1 · · · sn is a model of LTLf formula (and we write ρ |= ϕ) ϕ if ρ, 1 |= ϕ, where

• ρ, i |= p if p ∈ AP and p ∈ si
• ρ, i |= ϕ if ϕ is a propositional formula and si |= ϕ
• ρ, i |= ¬ϕ if ρ, i ̸|= ϕ, i.e., it is not the case that ρ, i |= ϕ
• ρ, i |= ϕ∧ϕ2 if ρ, i |= ϕ1 and ρ, i |= ϕ2
• ρ, i |= ϕ if i +1 ≤ |ρ| and ρ, i +1 |= ϕ
• ρ, i |= ϕ1Uϕ2 if ρ, j |= ϕ2 for some i ≤ j ≤ |ρ| and ρ, k |= ϕ1 for every i ≤ k ≤ j

The semantics of LTL is similar, with the exception that formulae are evaluated over infinite traces (i.e., |ρ| =∞). In the sequel, we refer to the size of an LTL or LTLf formula ϕ as the number of temporal and logical operators, plus the number of atomic propositions in ϕ.

2.2 LTL and Automata

LTL and LTLf have a well-known correspondence with automata, that we review here (cf. [Baier and McIlraith, 2006b; Kupferman and Vardi, 2005]). An automaton is a tuple A = 〈Q,Σ, q0, T, α〉, where Q is a finite set of automaton states, Σ is a finite alphabet of input symbols (in this paper, Σ = 2AP ), q0 ∈ Q is the initial state, and T ⊆ Q×Σ×Q is the transition relation. The transition relation is deterministic when a unique triplet (q, s, q′ ) ∈ T exists for each pair (q, s) ∈ Q × Σ. A run of A on an infinite word w = s0s1 · · · ∈ Σω is a (possibly infinite) sequence q0q1 · · · where (qi, si, qi+1) ∈ T for each i ≥ 0. The set α ⊆ Q serves to characterize the set of runs that are accepting. Different types of automata exist according to their acceptance condition. Here, we are interested in Universal Co-B¨uchi Word (UCW) and Non-deterministic Finite Word (NFW) automata.

A UCW automaton accepts an infinite word w if all the runs on w hit a finite number of states in α. In contrast, a NFW automaton accepts a finite word w if some run on w has the same length as w and finishes in one of the states in α. NFW automata with deterministic transition relation are called Deterministic Finite Word (DFW) automata. We say that automaton A is a transformation of an LTL (resp. LTLf ) formula ϕ if A accepts all and only the models of ϕ.

Property 1. LTL (resp. LTLf ) formulae can be transformed into UCW (resp. NFW) automata in worst-case exponential time, and so that the number of states is worst-case exponential in the size of the formula.

Property 2. LTLf formulae can be transformed into DFW automata in worst-case double exponential time, and so that the number of states is worst-case double exponential in the size of the formula.

3 Planning with Temporally Extended Goals

Automated planning is a popular model-based approach to sequential decision-making. The world dynamics - i.e., the dynamics of the system under observation - is assumed to be given to the agent by means of a planning domain that describes how the world reacts in response to the agent's actions. The objective in a planning problem is to synthesize an agent strategy that guarantees satisfaction of a prescribed goal. We formalize these concepts below.

3.1 Planning Domains

In this paper we focus on planning domains that are fully observable and non-deterministic (FOND). We represent FOND domains compactly (Definition 1), following the notation in Ghallab et al. [2016]. The set of fluents, F, represents properties of the world. A planning state is a complete truth assignment over the set of fluent variables, and is usually represented with the subset of fluents s ⊆ F that hold true in such state. Regarding the dynamics, an action a ∈ A is applicable in a state s if (s, a) ∈ Poss. The result of applying action a in state s is a state s′ ∈ δ(s, a). We say an action a is deterministic when |δ(s, a)| = 1 in all states s for which a is applicable. Note that, in general, the result of applying an action is non-deterministic and cannot be predicted in advance.

Definition 1. A FOND planning domain is a tuple 〈F,A, δ, Poss〉, where F is a finite set of fluent symbols, A is a finite set of action symbols, Poss ⊆ 2F × A, and δ : 2F ×A→ 22F . The size of the domain is |F|.

Fairness over Executions. Executions of a planning domain D = 〈F,A, δ, Poss〉 from state s0 are (possibly infinite) sequences of state-action pairs (s0, a0)(s1, a1) · · · such that (sn, an) ∈ Poss and sn+1 ∈ δ(sn, an). It is common in FOND planning to presume fairness over executions, that is, that all the non-determinism of the actions manifests infinitely in the limit (cf. [Cimatti et al., 2003]). An execution π is unfair if |π| = ∞ and there exists s, a and s′ ∈ δ(s, a) such that the pair (s, a) appears infinitely often in π, but the number of occurrences of consecutive pairs (s1, a1)(s2, a2) with s1 = s, a1 = a, and s2 = s′ is finite. Fair executions are those that are not unfair.

3.2 Planning Problems

A FOND planning problem is a tuple 〈D, ϕI , ϕG〉, where: D is a FOND domain; ϕI is a formula that describes the (complete) initial state of the world 1 ; and ϕG is a formula that describes the objective of the agent.

Compact Problem Representations. Planning problems are commonly encoded with a compact representation of states, actions, and state transitions. For the reader not familiar with STRIPS-like languages, such as PDDL, a planning problem is a tuple 〈F, I,O,G〉, where F is the set of fluents, I is the initial state, O is the set of operators, and G is the goal condition. For final-state goals, G is usually the set of literals that hold true in a goal state. States are sets of fluents that represent what holds true in the world. For a fluent f, we write s |= f if f ∈ s, and s |= ¬f if f ̸∈ s. For a set of literals Φ, we write s |= Φ if s |= l for each l ∈ Φ. An action a ∈ O is defined in terms of its preconditions (Prea) and effects (Eff a). The preconditions are a set of literals that need to hold true in a state s for a to be applied, that is, s |= Prea. The result of applying action a in s is a state s′ characterised non-deterministically by one of the Eff ia in Eff a = {Eff 1a , . . . , Eff na }. Each Eff ia contains a set of conditional effects that add and delete fluents from s. More formally, each Eff ia contains pairs c → e. A fluent f holds in s′ iff: (i) s |= c for some c → e in Eff ia and f ∈ c; or (ii) s |= f and for all c → e in Eff ia such that s |= c, ¬f ̸∈ c. Sometimes we abuse notation and write Eff a = {cj → ej}j∈J ∪ oneof {Eff 1a , . . . , Eff na } to denote that each cj → ej is a conditional effect in all Eff ia , and we omit writing it in their explicit description. We also omit writing c in c → e when c = ∅. An execution finishing in state s satisfies a final-state goal G if s |= G.

3.3 Strong and Strong-Cyclic Solutions

In this paper, solutions to a FOND planning problem take the form of strategies. Following Camacho et al. [2019], a strategy for a FOND planning domain D = 〈F, A, δ, Poss〉 is a function σ : (2F )+ → A ∪ {end}. For a strategy to be well-defined, we require actions σ(s0 · · · sn) be applicable in sn. An execution of strategy σ in domain D from initial state s0 |= ϕI is a sequence π = (s0, a0)(s1, a1) · · · with the following properties: (i) an = σ(s0 · · · sn) for each n < |π|; (ii) for each n < |π| - 1, an ∈ A is an action applicable in sn and sn+1 ∈ δ(sn, an) is a result of applying action an in sn; (iii) if n = |π| - 1, then an = end. Intuitively, end is a special action symbol that indicates the termination of the execution. Non-terminating executions are infinite, and we write |π| = ∞. Strategies can be implemented compactly as finite-state controllers (FSCs) (cf. [Geffner and Bonet, 2013]). Goal formulae are evaluated with respect to execution traces, which are simply rewritings of executions π = (s0, a0)(s1, a1) · · · in the form of sequences of sets ρπ = (s0 ∪ {a0})(s1 ∪ {a1}) · · · .

1 If ϕI is only partially defined, the problem can be polynomially reduced to FOND planning with a (completely defined) dummy initial state sI and dummy action aI, only applicable at state sI, that non-deterministically maps sI to some state s (and henceforth ϕI ) that models the original ϕI .

Definition 2 (Strong Solutions). A strategy σ is a strong solution to FOND planning problem 〈D, ϕI , ϕG〉 with temporally extended goal formula ϕG if all execution traces of σ that commence in s0 |= ϕI satisfy ϕG.

Definition 3 (Strong-Cyclic Solutions). A strategy σ is a strong-cyclic solution to FOND planning problem 〈D, ϕI , ϕG〉 with temporally extended goal formula ϕG if all fair execution traces of σ that commence in s0 |= ϕI satisfy ϕG .

Our definitions for the classes of strong and strong-cyclic solutions to FOND planning with temporally extended goals extend those defined by Cimatti et al. [2003] for FOND planning with final-state goals. We highlight three differences worth noting. First, we define solutions to be strategies, whereas solutions as for Cimatti et al. [2003]'s paper take the more restricted form of policies, or memoryless strategies σ such that σ(s0 · · · sn) = σ(sn) for each s0 · · · sn. Second, execution of solutions to FOND planning with temporally extended goals may not terminate. In contrast, (fair) executions of solutions to FOND planning with final-state goals always terminate upon achievement of a goal state. Finally, strong policies that are solution to a FOND planning problem with final-state goal are acyclic. This property no longer holds, in general, for temporally extended goals.

3.4 FOND Planning with LTL and LTLf Goals

Throughout the paper, we use LTL and LTLf as goal specification languages and refer to the subsequent problems as LTL FOND and LTLf FOND, respectively. Nevertheless, our techniques can be extended to any formal language that can be transformed into automata (e.g. PSL, CTL, PLTL, and LDLf ). For simplicity, we limit the algorithms presented here to temporal formulas defined over the set of propositional variables AP = F. Note, our techniques can be naturally extended to handle propositional variables F ∪ A, allowing goal formulae to describe state-action execution traces by means of the addition of new fluents occ(a) that are made true after each action a is executed (cf. [Bienvenu et al., 2011]).

LTLf FOND Planning. The model of LTLf FOND planning is concerned with the synthesis of terminating strategies whose executions satisfy a prescribed temporally extended goal expressed with an LTLf formula over fluent variables.

LTL FOND Planning. The objective in LTL FOND planning is to synthesize non-terminating strategies whose executions satisfy a prescribed temporally extended goal expressed with an LTL formula over fluent variables.

3.5 RelatedWork

Existing tools to solve FOND planning with LTLf and LTL goals were limited to the computation of strong-cyclic solutions (cf. Table 1). In the context of planning with deterministic actions, a variety of planners exist for temporally extended goals expressed in LTLf (e.g. [Baier and McIlraith, 2006b; Baier and McIlraith, 2006a; Torres and Baier, 2015])), LTL (e.g. [Patrizi et al., 2011]), and with temporal operators in the syntax of PDDL3.0, a standard language for modeling planning problems [Gerevini et al., 2009]. The aforementioned approaches follow a similar schema that we also adopt.

1. Transform the goal formula ϕG into automata
2. Construct a new planning problem P ′ by augmenting P with the states and dynamics of the automata
3. Solve P ′ with an off-the-shelf planner
4. Extract a solution to P from a solution to P ′

LTLf FOND and LTL FOND planning have been well studied theoretically. Strong and strong-cyclic plan existence are EXP-complete in the size of the domain, and 2EXP-complete in the size of the goal formula [De Giacomo and Rubin, 2018; Camacho et al., 2019]. FOND planning with final-state goals is EXP-complete, and can be solved in polynomial time in the size of the search space [Rintanen, 2004]. Motivated by these recent results, we conducted an analysis of the sources of computational complexity of existing compilation-based approaches to LTLf FOND and LTL FOND planning. Table 2 reports the size of the search space in the compiled FOND planning problems in terms of the sizes of the original domain, the automaton transformation, and the goal formula. We determined that existing complete approaches can compute solutions in exponential time in the size of the original domain, and double exponential time in the size of the goal formula - matching the complexity of the decision problems.

4 Algorithms for LTLf FOND Planning

The approach taken by Camacho et al. [2017] to strongcyclic LTLf FOND planning takes an LTLf FOND planning problem P = 〈D, ϕI , ϕG〉 and constructs a final-state FOND problem, P ′ . Strong-cyclic solutions to P can be extracted from strong-cyclic solutions to P ′ . In essence, the compilation does a cross-product of the original domain and the automaton transformation of the formula. Figure 1 shows the details - we introduced minor changes that do not affect correctness. We convey that strong solutions to P can be also obtained from the same compilation, P ′ , by simply searching for strong solutions. We elaborate on the approach below.

Step 1: Transformation of ϕG into NFW or DFW. In the first step, a CNF representation of the LTLf goal formula ϕG = ϕ(1) G ∧ · · · ∧ ϕ(n) G is transformed into multiple NFW A(i) , one per each clause ϕ(i) G . The traces that satisfy ϕG are in correspondence with the traces that are accepted by all the A(i) , i = 1..n. Automata decompositions of ϕG are optional, and enable to scale to larger goal formulas. The compilation also works with DFW transformations of the LTLf formula, as DFW automata are a particular type of NFW automata.

Step 2: Construction of a new FOND problem. In the second step, a problem P ′ is constructed that integrates the dynamics of the NFW obtained in the first step. The details of the compilation are shown in Figure 1. In a nutshell, planning states in P ′ keep track of automaton runs on the partial plan being simulated. To this end, execution of the actions in P are followed by actions that synchronize the automaton states.

Step 3: Solving the compiled problem. An off-the-shelf strong or strong-cyclic planner is used to compute a solution to P ′ . Strong (resp. strong-cyclic) solutions to P can be extracted from strong (resp. strong-cyclic) solutions to P ′ .

Step 4: Extraction of a strategy. A strategy σ that is solution to P is constructed from the solution σ′ found in Step 3. Actions σ(s0 · · · sn) are obtained by unfolding σ′ in P ′ .

Correctness. Theorem 1 states the soundness and completeness of the approach. We omit the proof for space reasons, but it follows from the following properties: (i) State-action plans in P ′ simulate state-action plans in P; (ii) State-action plans in P ′ do bookkeeping of (some, or all) the runs of the automata; and (iii) An state-action plan in P satisfies ϕ iff the counterpart state-action plan in P ′ that simulates it and does bookkeeping of all the automata runs achieves the goal.

Theorem 1. An LTLf FOND problem P has a strong (resp. strong-cyclic) solution iff the compiled FOND problem P ′ described in Figure 1 has a strong (resp. strong-cyclic) solution.

Computational complexity. Our compilation-based ap- Components of the compilation:

Figure 1: Components of the compiled FOND problem P ′ = 〈F ′ , I ′ ,O′ ,G′ 〉 for an LTLf FOND problem P = 〈F, I,O, ϕG〉 with ϕG = ϕ(1) G ∧ · · · ∧ϕ(n) G and Ai = 〈Q(i) , 2F , q(i) 0 , T (i) , α(i) 〉. For convenience, we write Q := ⋃i Q(i) and T := ⋃i T (i) .

proach to strong and strong-cyclic LTLf FOND planning can compute solutions in worst-case time that matches the complexity of the decision problem (Theorem 2). The result follows by looking at the size of the search space in P ′ with respect of the size of the search space in P and the size of automata transformations of the goal formula. Interestingly, the worst-case computational complexity does not depend on whether NFW or DFW automata transformations are used (Corollary 1). 2 This is because the extra exponential cost incurred by DFW automata transformations is compensated with an exponentially reduced size of the search space in the compiled problem (w.r.t. compact domain representations).

Theorem 2. A strong (resp. strong-cyclic) solution to an LTLf FOND planning problem P = 〈D, ϕI , ϕG〉 can be computed in worst-case exponential time in the size of the D, and double-exponential time in the size of ϕG via the compilations to FOND planning described in Figure 1.

Proof. The size of the search space in the compiled problem, P ′ , is linear in the size of the search space of P and exponential in the size of NFW automata transformations of the goal formula. The desired result follows by observing that NFW automata transformations are worst-case exponential in the size of ϕG, and FOND planning can be solved in polynomial time in the size of the search space [Rintanen, 2004].

2 We thank Moshe Vardi for a question that inspired this result.

DFW automata transformations are worst-case doubleexponential. To obtain the desired result, we need to observe that with deterministic automata the size of the search space in P ′ augments only linearly (not exponentially) with the automata sizes - because in P ′ only one automaton state fluent per DFW automaton can be made true at a time.

Corollary 1. The worst-case domain and goal complexity of the compilation-based approach to strong and strong-cyclic LTLf FOND planning does not depend on whether the LTLf goal formula is transformed into NFW or DFW automata.

5 Bounded LTL FOND Planning

To date, no algorithms for computing strong solutions to LTL FOND planning had been studied. Unlike with LTLf FOND, we cannot simply take Camacho et al. [2017]'s approach to strong-cyclic LTL FOND planning and replace the strongcyclic planner by a strong planner. The reason is complex, and is related to the type of automaton that was used - Nondeterministic B¨uchi Word (NBW) automata. In essence, all approaches to LTL synthesis rely, in one way or another, to automata determinization. The problem with using NBW is that it cannot be determinized, in general. Because LTL synthesis can be reduced to strong LTL FOND planning [Camacho et al., 2019], we can expect similar determinization requirements in algorithms for strong LTL FOND planning

Noteworthy, we use a type of automaton that is particularly new to the planning community: UCW automata. In what follows, we say that the co-B¨uchi index of a word w (wrt a UCW automaton A = 〈Q, Σ, q0, δ, α〉) is the maximum k for which there exists a run of A on w that hits k states in α. Theorem 3 sets bounds on the co-B¨uchi index required to guarantee existence of solutions. In contrast to analogous results for bounded LTL synthesis, the bounds also depend on the domain size. In the next section, we will design algorithms for bounded plan synthesis in strong LTL FOND planning.

Lemma 1. Strategy executions traces of a strong solution to an LTL FOND planning problem yield accepting runs of UCW transformations of the goal formula.

Theorem 3 (Bounded plan synthesis). Let P = 〈D, ϕI , ϕG〉 be an LTL FOND planning problem, and let AG be a UCW transformation of ϕG. If P has a strong solution, then there exists a strategy σ that is a strong solution to P such that all executions traces of σ yield accepting runs of AG with coB¨uchi index bounded by some k < ∞ exponential in the size of AG, and exponential in the size of D.

Proof. From the reductions of LTL FOND into game structures, and further reductions into parity games, we know that a finite-state controller M that implements a strategy σ that is a strong solution to P can be synthesized in exponential time in the size of D, and exponential time in the size of AG (cf. [Camacho et al., 2019]). The size of such controller, |M|, is worst-case exponential in the size of D, and exponential in the size of AG. It must be the case that the runs of AG on executions traces of M have finite co-B¨uchi index - because M implements a solution (Lemma 1). Moreover, the co-B¨uchi index must be bounded by k = |M| · |AG|.

Algorithm 1 Strong solutions to LTL FOND planning

Input: P = 〈D, ϕI , ϕG〉

• 1: TransformϕG into UCWAϕ. Fix k = 1
• 2: Construct P ′k = XPRODUCT(P,Aϕ, k)
• 3: If P ′k has no solution, increment k by one and go to 2
• 4: return solution

Otherwise, a loopy behaviour could be generated that yields executions traces with infinite co-B¨uchi index. The bound k is exponential in the sizes of AG and D.

6 Algorithms for LTL FOND Planning

Our approach to compute a strong solution f to a LTL FOND planning problem P compiles the problem into a series of standard FOND planning problems P ′k with final-state goal. The compilations simulate the dynamics of P, and keep track of the runs of a UCW automata transformations of the goal formula. The parameter k in P ′k bounds the maximum coB¨uchi index allowed on the executions traces of f. Solutions to P can be directly extracted from solutions to P ′k .

Algorithm 1 summarizes the steps of our approach, that we detailed below. We combine ideas from strong-cyclic LTL FOND planning [Camacho et al., 2017] and LTL synthesis via strong-cyclic FOND planning [Camacho et al., 2018b].

Step 1: Transformation of ϕG into UCW. A CNF representation of the LTL formula ϕG = ϕ1G ∧ · · · ∧ ϕnG is transformed into multiple UCWAi, one for each clause ϕiG . The traces that satisfy ϕG are in correspondence with the traces that are accepted by every Ai, i = 1..n. As usual, automata decompositions serve to scale to larger goal formulas.

Step 2: Construction of a new FOND problem. In the second step, we construct a FOND problem P ′k that integrates the dynamics of the UCW within the original LTL FOND problem, P. Details are shown in Figure 2. The resulting problem is constructed in a way that enforces that strategy execution traces yield UCW runs with co-B¨uchi index no greater than input parameter k, starting with k = 1. The nondeterminism induced by action continue is a recourse used to generate non-terminating plans. It is important to note that the dynamics simulate all the runs of the UCW, and fluents newCnt(q, m) do bookkeeping of the maximum co-B¨uchi index among all the runs that finish in q ∈ Q. The dynamics of the FOND domain enforces that those runs never hit α more than k times. Certainly, a deadend is induced whenever one run hits α exactly k + 1 times. This is because actions syncF(q, m) can only synchronize automaton states with associated co-B¨uchi index not greater than k. Hence, automaton state fluents newF(q) with associated co-B¨uchi index oldCnt(q, k+1) cannot be made false, preventing the action continue from being applied.

Step 3: Solving the compiled problem. An off-the-shelf planner is used to compute a strong-cyclic solution to the compiled FOND problem. If no solution exists, parameter k is incremented by one and the algorithm goes to Step 2.

Step 4: Extraction of a strategy. Similar to the strategy extraction procedure for LTLf FOND, a strong solution to P

Figure 2: Components of the compiled FOND problem P ′k = 〈F ′ , I ′ , O′ , G′ 〉 for an LTL FOND problem P = 〈F, I, O, ϕG〉 with ϕG = ϕ(1) G ∧ · · · ∧ ϕ(n) G and Ai = 〈Q(i) , 2F , q(i) 0 , T (i) , α(i) 〉. For convenience, we write Q := ⋃i Q(i) and T := ⋃i T (i) .

can be obtained by unfolding a strong-cyclic solution to P ′ .

Correctness. Theorem 4 establishes the correctness of our compilation-based approach to computing strong solutions to LTL FOND planning. Note that a strong-cyclic planner is needed to obtain strong solutions.

Theorem 4. An LTL FOND problem P = 〈D, ϕI , ϕG〉 has a strong solution iff the compiled FOND problem P ′k described in Figure 2 has a strong-cyclic solution for some k < ∞ double exponential in the size of ϕG, and exponential in the size of D.

Proof sketch. We will exploit the following property: a strategy f is a strong-cyclic solution to a goal-oriented FOND planning problem iff the goal condition can be reached from any state that is reachable by f from the initial state.

Suppose P has a strong solution. By Theorem 3, there exists a strong solution f and k < ∞ worst-case double exponential in the size of ϕG and D so that execution traces of f generate automata runs with co-B¨uchi index not greater than k. Let f ′ be a strategy for P ′k that simulates f, i.e., that outputs the same actions as f in response to the plans being simulated. The goal of P ′k is reachable from all states that are reachable by f ′ from the initial state. I.e., f ′ is a strong-cyclic solution to P ′k (in the form of a strategy). Finally, if a FOND planning problem with final-state goal has a solution in the form of a strategy, then it also has one in the form of a policy.

In the other direction, we will see that a strong-cyclic solution π to P ′k yields a strong solution f to P. Certainly, consider f to be the strategy that results from unfolding π on the simulated plans, and choosing the non-deterministic effect of action continue that does not lead to the goal. It is easy to see that f yields infinite-length plans with co-B¨uchi index not greater than k, and therefore is a strong solution to P. The bounds follow from Theorem 3. □

Computational complexity. Our compilations can be used to compute strong solutions to an LTL FOND problem in worstcase time that matches the complexity of the decision problem (Theorem 5).

Theorem 5. A strong solution to an LTL FOND problem P = 〈D, ϕI , ϕG〉 can be computed in worst-case exponential time in the size of the size of D, and double exponential time in the size of ϕG via the compilations to strong-cyclic FOND planning described in Figure 2 and Algorithm 1.

Proof. The goal formula ϕG can be transformed into an UCW automaton AG in exponential time, with a number of states |Q| that is exponential in the size of ϕG and D (cf. Property 1). A strong solution to P can be extracted from a strong-cyclic solution to P ′k in linear time. The size of the search space in P ′k is exponential in the size of D, and polynomial in k|Q| (cf. Figure 2). The desired result follows by exploiting the bounds on the co-B¨uchi index stated in Theorem 3, and observing that FOND planning can be solved in polynomial time in the size of the search space, and the bounded number of iterations in Algorithm 1.

6.1 Proofs of Unsolvability

Whereas planning algorithms have been traditionally focused on the search for solutions, detecting when a planning instance is unsolvable is a topic of growing interest (e.g. [Eriksson et al., 2017]). The absence of strong solutions to an LTL FOND problem can be assessed when the compiled FOND problem Pk obtained with k exponential in Q has no strongcyclic solution (cf. Theorem 4). Unfortunately, the bounds on k are prohibitively large to assess unsolvability in practice.

We present an alternative method to obtain a proof that an LTL FOND problem has no strong solution. We follow on recent work by [Camacho et al., 2018a] to check unrealizability of specifications for LTL synthesis via reduction to reachability games, and adapt their techniques to LTL FOND planning LTL FOND can be interpreted as a two-player game between the agent - that decides on actions - and the environment - that decides on the outcome of the actions [Camacho et al., 2019]. The agent has the objective to satisfy ϕG. Observe that P is unsolvable iff the environment has a strategy to defeat the agent, that is, a strategy to satisfy ¬ϕG. With this in mind, we reason on the dualization of the problem. We transform ¬ϕG into UCW automata, and compute an agent strategy that forces a run with co-B¨uchi index greater than k, for some hyperparameter k. If no such strategy exists, we

Algorithm 2 Proof unsolvability in LTL FOND planning

Input: P = 〈D, ϕI , ϕG〉

• 1: Transform¬ϕG into UCWAϕ. Fix k = 1
• 2: Construct Pk = XPRODUCTUNSOL(P,Aϕ, k)
• 3: If Pk has strong solution, increment k by one and go to 2
• 4: return unsolvable

can conclude that the game is winning for the environment. In other words, P has no strong solution. Note, we do not obtain a environment counter-strategy, but a proof that one exists. The details of our approach follow below.

Step 1: Transformation of ¬ϕG into UCW. The negation of the goal formula is transformed into one or multiple UCW.

Step 2: Construction of a new FOND problem. The construction of a problem Pk = XPRODUCTUNSOL(P,Aϕ, k) follows that of Figure 2, with three exceptions: (i) the UCW automata used in the compilation are transformations of ¬ϕG; (ii) the goal of Pk is achieved when one of the fluents newCnt(q, m) with m = k is achieved; and (iii) the action to restablish the world dynamics of the problem is replaced by:

Step 3: Solving the compiled problem. A FOND planner is used to search for strong solutions to Pk. If no solution exists, the LTL FOND problem is deemed unsolvable. Otherwise, k is incremented by one and Step 2 is repeated.

Correctness. Theorem 6 states the correctness of our compilation-based approach to determining the existence of strong solutions to LTL FOND planning. Note that a strong planner is needed to search for solutions to P = 〈D, ϕI , ϕG〉. The proof follows the mechanics of the proofs of Theorems 3 and 4, and we omit it here for space reasons.

Theorem 6. An LTL FOND problem P = 〈D, ϕI , ϕG〉 has no strong solution iff for some k < ∞ double exponential in the size of ϕG, and exponential in the size of D, the compiled FOND problem Pk has no strong solution

Computational complexity. Our compilation-based approach to determine the existence of solutions to LTL FOND problem described in Algorithm 2 runs in worst-case time that matches the complexity of the decision problem (Theorem 7).

Theorem 7. Non-existence of strong solutions to an LTL FOND problem P = 〈D, ϕI , ϕG〉 can be proved in worstcase exponential time in the size of the size of D, and double exponential time in the size of ϕG via the compilations to strong FOND planning Pk and Algorithm 2.

Proof sketch. Analogous to the proof of Theorem 5. □

7 Experiments

To the best of our knowledge, ours are the first algorithmic approaches to compute strong solutions to LTLf FOND and LTL FOND planning. Our compilations are implemented in Python, and take (and produce) PDDL files. We used Spot [Duret-Lutz et al., 2016] to transform LTL to UCW, and Baier and McIlraith [2006b]'s code to transform LTLf to NFW.

We conducted a series of experiments to evaluate the efficiency of our methods in the Clerk, Lift, and Waldo domains from [Patrizi et al., 2013], detailed below. Goal formulas were interpreted as LTLf (resp. LTL) for LTLf FOND (resp. LTL FOND) planning. Strong policies to the compiled problems were computed with myND planner [Mattm¨uller et al., 2010], and PRP planner was used to compute strong-cyclic policies [Muise et al., 2012]. Because myND does not support conditional effects, we replaced action continue in Figure 1 with a cascade of actions without conditional effects. Our experiments ran in Ubuntu machines with an Intel(R) Xeon(R) 2.30GHz CPU. Runtime was limited to 30 minutes, and memory usage never exceeded 1GB.

Clerk. The agent has to process orders of different types of packages (n in problem pn). Each package can be served or stored in a designated location, with n locations in total. The agent can request orders, in which one of the n products is non-deterministically requested to be served, or put on hold for restock. The objective of the agent is to continuously complete orders. which we encoded with the following formula:

• □♦(active request)∧

Lift. The agent controls a lift in a building with a number of floors (n floors in problem pn). Each timestep, the elevator receives one or more requests from some of the floors (this is modeled in PDDL with a cascade of sequential actions). The objective is to compute a controller for the elevator that serves each request. This is modeled with the formula:

Waldo. The agent can inspect rooms, numbered in consecutive order, in a circular corridor. Problem p2n has 2n rooms. The n-th and 2n-th rooms have a special property: Waldo may non-deterministically appear when visiting one of those. The dynamics of the problem forces the agent to visit the 2nth room before revisting the n-th room (and vice versa). Each time both rooms are visited, a special fluent search again is made true for only one timestep and a new cycle starts. The objective is to find a strategy that searches for Waldo, i.e.,

In the search for strong solutions to LTLf FOND, strong planner myND detected unsolvability of the Clark problems relatively fast. The goals in the Lift problems resulted trivial. The Waldo problems show a more interesting scalability.

Strong solutions to LTL FOND in the Lift and Waldo domains are, conceptually, not very different than strong solutions to LTLf FOND, except that the agent has to cycle. Noteworthy, we observed that the performance of the planning step in LTL FOND suffered significantly (at least with PRP) in comparison with the planning step in LTLf FOND. Also in comparison, the search for strong-cyclic solutions to those LTL FOND problems (with Camacho et al. [2017]'s compilation) showed much better scalability. We conjecture three aspects that may challenge scalability in our approach to strong LTL FOND: (i) conditional effects affect performance of planners like PRP (ii) FOND planners based on plan aggregation, like PRP, may suffer from myopic behaviour because the compiled problem P ′ non-deterministically yields a goal state at each simulated timestep. (iii) it is challenging for the planner to generalize policies accross macrostates that vary on the co-B¨uchi idexes asociated to automaton state fluents.

The first two items identified above could be mitigated by new FOND planners. The third item is more delicate. If our conjecture (iii) is true, then bounded LTL FOND planning would suffer with final-state goals (e.g. ♦ϕ, for some propositional formula ϕ) and other temporally extended goals that require a large makespan, which translates into a large coB¨uchi index. Our experiments suggest the need for more effective methods in LTL FOND that handle large co-B¨uchi indexes without severely affect performance.

8 Discussion and FutureWork

Synthesizing programs for sequential decision-making in dynamical environments is a central problem in artificial intelligence. The problem can be cast as FOND planning with temporally extended goals expressed in LTL and its variant over finite traces, LTLf . While the problem is well understood theoretically, the number of existing tools is limited. We provided the first algorithmic approach to computing strong solutions to LTLf FOND and LTL FOND planning. Our techniques complement previous techniques for computing strong-cyclic solutions, collectively providing a complete battery of tools for strong and strong-cyclic FOND planning. We conducted an analysis of the sources of computational complexity, and determined that our techniques for plan synthesis are computationally effective in the sense that they match the domain and goal complexity of the plan existence decision problems. We evaluated the performance of our approaches and identified potential sources of complexity that make it challenging to compute strong solutions to LTL FOND, relative to computing strong-cyclic ones.

Acknowledgements

We gratefully acknowledge funding from the Natural Sciences and Engineering Research Council of Canada.