Automata-Theoretic Foundations of FOND Planning for LTLf and LDLf Goals

1 Introduction

We study planning in fully observable nondeterministic domains (FOND) [Ghallab et al., 2004; Geffner and Bonet, 2013] for temporally extended goals expressed in LTLf and its extension LDLf . We consider two variants of planning: in FONDunr, plans are guaranteed to produce traces that satisfy the goal; in FONDfair, this is guaranteed only in fair environments [Daniele et al., 1999; Pistore and Traverso, 2001; Cimatti et al., 2003; Sardi˜na and D'Ippolito, 2015].

Linear temporal logic on finite traces (LTLf ) has been used extensively in AI [Bacchus and Kabanza, 2000; Baier and McIlraith, 2006; De Giacomo and Vardi, 2013], as well as in other areas of computer science such as in business process modeling [van der Aalst et al., 2009]. In Planning, notably, LTLf can be used for expressing trajectory constraints in PDDL 3.0 [Gerevini et al., 2009].

Linear dynamic logic on finite traces (LDLf ) [De Giacomo and Vardi, 2013] is a proper extension of LTLf by regular expressions. It can capture procedural constraints on executions, as in [Fritz and McIlraith, 2007; Baier et al., 2008], which are typically expressed as regular expressions that must be fulfilled by traces. The logics LTLf /LDLf are also used to express non-Markovian rewards/goals in extensions of MDPs [Camacho et al., 2017a; Brafman et al., 2018].

In this paper we make a careful study of the complexity of solving FONDunr and FONDfair. We observe that from results in literature, reviewed below, it is easy to see that both of these are in 2EXPTIME. However, such results blur the

Sasha Rubin

Univ. Napoli "Federico II", Italy

sasha.rubin@unina.it

distinction between the domain specification (typically large) and the goal (typically small). In our analysis we want to distinguish these two source of complexity, i.e., the domain complexity and the goal complexity.

FOND Planning. One way to see that FONDunr planning is solvable in 2EXPTIME is to reduce it to reactive synthesis. Reactive Synthesis is a problem that is deeply related to planning in fully observable nondeterministic domains. It can be seen as a generalization of planning in non-deterministic domains, where both the goal and the domain are represented as formulas. Reactive synthesis for LTLf /LDLf formulas is 2EXPTIME-complete [De Giacomo and Vardi, 2015].

For the upper bound, observe that FONDunr with LTLf /LDLf goals is polynomially reducible to reactive synthesis for LTLf /LDLf goals. Indeed, we can polynomially represent the domain specification in terms of LTLf formulas expressing preconditions and effects. This gives the 2EXPTIME upper bound. However, this reduction does not allow one to study the domain/goal complexities since it compiles both the domain and the goal into a single formula.

For the lower bound, observe that LTLf /LDLf reactive synthesis is polynomially reducible to FONDunr planning in a very simple domain that allows all actions and has all possible nondeterministic effects. This establishes that FONDunr with LTLf /LDLf goals is also 2EXPTIME-hard.

FOND planning in fair environments. Turning to the 2EXPTIME upper bound for FONDfair, we note that fairness is a property that requires the analysis of traces that are infinite. Hence we cannot reduce FONDfair directly to LTLf /LDLf synthesis. That said, we can indeed reduce it to LTL/LDL synthesis, i.e., synthesis on infinite traces, which is 2EXPTIMEcomplete [Pnueli and Rosner, 1989]. 1 However, synthesis still appears to be prohibitive in the infinite-trace setting, not so much for the 2EXPTIME-completeness, but for the difficulties of finding good algorithms for automata determinization, a crucial step in the solution, see, e.g., [Fogarty et al., 2013]. Fortunately, efficient techniques for solving FONDfair for LTLf /LDLf goals have been proposed in [Camacho et al., 2017b], where a sound and complete translation into an exponentially larger FONDfair problem for the standard reachability goal has been presented, implemented and experimented in practice. This compilation not only gives the 2EXPTIME upper bound, but better algorithms. However, it still blurs the complexity coming from the domain and that coming from the LTLf /LDLf goal since it compiles both the domain and the LTLf /LDLf goal into the domain. The existence of matching lower bounds has been open until now. 2

1 We remark that LDL on infinite traces [Vardi, 2011] can be seen as a clean version of standard formalisms used in verification such as Intel ForSpec [Armoni et al., 2002] and the standard PSL [Eisner and Fisman, 2006]. The synthesis techniques developed in [Pnueli and Rosner, 1989] immediately extends to LDL on infinite traces.

Our contribution. We study the complexity of planning for LTLf /LDLf goals separating the analysis wrt the domain and the goal. For the upper bounds, we develop simple, direct and elegant automata-based techniques to deal both with FONDunr and FONDfair for LTLf /LDLf goals. Using these techniques we separate the domain and goals as sources of complexity, and characterize both problems as EXPTIME in the size of domain specification (expressed compactly, e.g., as in PDDL) and as 2EXPTIME in the size of the LTLf /LDLf goal. For the lower bounds, we observe that EXPTIMEhardness in the size of the domain already holds for reachability goals [Rintanen, 2004]. For FONDunr, 2EXPTIMEhardness in the size of the goal comes from the mentioned reduction from LTLf synthesis, and here we extend this reduction to show 2EXPTIME-hardness also for FONDfair. We actually strengthen this characterization by showing that the smallest plan/strategy fulfilling an LTLf goal may indeed need memory that is doubly-exponential in the size of the goal. This result applies to FONDfair as well as to FONDunr. Finally, we develop a tight correspondence between solving FONDfair with LTLf /LDLf goals and solving probabilistic planning problems with LTLf /LDLf goals, analogous to the well-known one for reachability goals [Rintanen, 2004].

2 Automata, LTLf and LDLf

Linear-time Temporal Logic over finite traces (LTLf ) has the same syntax as standard LTL, but is interpreted over finite traces (instead of infinite traces). For instance, the formula ✸G where G is a Boolean formula expresses that eventually G holds. Linear Dynamic Logic (LDLf ) is a proper extension of LTLf that is able to capture full regular expressions over traces. We refer to [De Giacomo and Vardi, 2013] for more details. Here, we focus on the property that: for every LTLf /LDLf formula ϕ there is a nondeterministic finite word automata (NFA) that accepts the traces τ that satisfy ϕ, and the size of the NFA is at most exponential in the size of the formula [De Giacomo and Vardi, 2013]. Such an NFA, as any NFA, can be transformed, e.g., by the well-known subset construction [Rabin and Scott, 1959], into a deterministic finite state automaton (DFA), which is in general exponential in the NFA, though in many cases the resulting DFA is comparable to, if not smaller (after minimization) than the original NFA [Tabakov and Vardi, 2005].

2 An alternative way of studying the complexities separately is to reduce to model checking variants of ATL∗ [Alur et al., 2002]. However, we would get into the same difficulties as for LTL synthesis mentioned above. Hence, here we follow a different path.

3 FOND Planning with LTLf /LDLf Goals

Following [Geffner and Bonet, 2013], a nondeterministic domain is a tuple D = (2F ,A, s0, δ, α) where: F is a set of fluents (atomic propositions); A is a set of actions (atomic symbols); 2F is the set of states; s0 is the initial state (initial assignment to fluents); α(s) ⊆ A represents action preconditions; (s, a, s′ ) ∈ δ with a ∈ α(s) represents action effects (including frame assumptions). Such a domain is assumed to be represented compactly (e.g. in PDDL), hence we consider the size of the domain as the cardinality of F, i.e., logarithmic in the number of states.

Intuitively, a nondeterministic domain evolves as follows: from a given state s, the agent chooses an action a ∈ α(s), after which the environment chooses a successor state s′ with (s, a, s′ ) ∈ δ. The agent can choose its action based on the history of states so far (i.e., the agent has full observation).

We now define what it means to solve a planning problem on D. A trace of D is a finite or infinite sequence s0, a0, s1, a1, · · · where s0 is the initial state, and ai ∈ α(si) and si+1 = δ(si, ai) for each si, ai in the trace. A strategy (or plan) is a partial function f : (2F )+ →A such that for every u ∈ (2F )+, if f(u) is defined then f(u) ∈ α(last(u)), i.e., it selects applicable actions. If f(u) is undefined, we write f(u) = ⊥. A trace τ is generated by f, or simply an f-trace, if (i) if s0, a0, · · · si, ai is a prefix of τ then f(s0s1 · · · si) = ai, and (ii) if τ is finite, say τ = s0, a0, . . . , an-1, sn, then f(s0s1 · · · sn) = ⊥.

Given a domain D and a LTLf /LDLf goal formula ϕ over atoms F ∪ A, a strategy f is a strong solution to D for goal ϕ if every f-trace of D is finite and satisfies ϕ. The FONDunr problem takes as input D and ϕ, and decides if there exists a strong solution to D for goal ϕ. In case such a strategy exists, we are also interested in computing one.

Relationship with reachability goals. In the classical setting the goal has the form ✸G, where G is a propositional formula over atoms F (i.e., the objective is to reach a domain state satisfying G). This form of planning has been thoroughly studied in literature under the name conditional planning with full observability, e.g., [Rintanen, 2004]. Typically such plans are represented as conditional trees. Alternatively we can compute a universal plan [Schoppers, 1987], i.e., a memoryless policy that given the current state returns the action to do. The two kind solutions have the same computational cost, although algorithms for universal plans are typically less efficient. Note that for reachability goals ✸G it is guaranteed that if a strong solution exists there is one which is memoryless (i.e., a memoryless policy). This is not true for general LTLf /LDLf goals, which is why we consider plans to be (memoryfull) strategies. Solving FONDunr for goals of the form ✸G is known to be EXPTIME-complete in the size of the domain [Rintanen, 2004].

Automata-theoretic solution. Next, we use automatatheoretic techniques to solve FONDunr planning for LTLf /LDLf goals, Algorithm 1 (for simplicity, complexities in parenthesis are wrt explicit representation of domain D, i.e., in the number of states).

Algorithm 1: FONDunr for LDLf /LTLf goals

Given LTLf /LDLf domain D and goal ϕ

• 1: Compute DFA corresponding to D (poly)
• 2: Compute NFA for ϕ (exp)
• 3: Determinize NFA to DFA (exp)
• 4: Compute product with DFA of D (poly)
• 5: Solve DFA game (poly)
• 6: Return winning strategy if it exists

The various steps are described in detail below.

Nondeterministic domains as automata. In Step 1 we transform the nondeterministic domain D = (2F , A, s0, δ, α) into an automaton AD recognizing all its traces, defined as AD = (2F∪A, (2F ∪ {sinit}), sinit, ϱ, F) with: alphabet 2F∪A (actions A include dummy start action); states 2F ∪ {sinit}; initial dummy state sinit; final states F = 2F (all states of the domain are final); transitions ϱ(s, [a, s′ ]) = s′ with a ∈ α(s) and (s, a, s′ ) ∈ δ, and ϱ(sinit, [start, s0]) = s0. For convenience we use the notation [a, s′ ] to stand for {a} ∪ s′ . Note that in the automaton AD we consider actions as further fluents in the alphabet.

A critical observation is that AD is a DFA. This is because in order to progress, the automaton reads both the action and its effect. In particular, the nondeterminism in the environment (which is devilish) is not translated into a nondeterminism in the automaton (which is angelic).

Example 1 Consider the following simplified version of the classical Yale shooting domain [Hanks and McDermott, 1986], where we have that the turkey is either alive or not and the actions are either shoot and wait with the obvious effects, though with a gun that may be faulty. In particular, shooting with a (supposedly) working gun may either result in killing the turkey or in the turkey remaining alive and the discovery that the gun is not working properly. However shooting (with care) with a gun that does not work properly makes it work and kills the turkey. The domain D is as follows:

Its corresponding DFA AD is:

DFA Game on the product automaton Step 4 of the algorithm forms the DFA AD ×Aϕ for the product of AD and Aϕ (the final states are the product of the final states). Traces in the product come from D, while the final states are determined by Aϕ. To solve the FONDunr we solve a certain game (Step 5) on the DFA AD × Aϕ where the objective of the player is to reach a final state of AD × Aϕ, i.e., a state that deems the trace fromD as satisfying the LTLf /LDLf formula ϕ. Such a game is called a DFA game. Solving such games amounts to finding an agent strategy that is winning, i.e., ensures the reachability objective no matter how the environment behaves. Before looking at DFA games, we consider a couple of examples.

Example 2 Continuing our example, consider a standard reachability goal ✸¬a. A corresponding DFA A✸¬a is as follows (actually any reachability goal ✸G with G propositional has an analogous structure):

The product DFA is: AD ×A✸¬a is:

A winning strategy (a plan) is:

Notice that as this example shows AD and AD ×A✸G are identical except for the final states, which for AD × A✸G are only those where G holds. In other words the states are functionally dependent on those of D and we do not need additional memory to store them explicitly. This is not the case for general LTLf /LDLf goals.

Example 3 For the goal ✸✷¬a a corresponding DFA is:

while the product AD ×A✸✷¬a is

One question arises: do we need to determinize the automaton for the formula in the above construction? 3 In fact we cannot use NFA's directly, because of a basic mismatch:

• NFA (being based on angelic nondeterminism) have perfect foresight, or clairvoyance, while
• strategies must be runnable: depend only on the past, not the future, and hence can handle only devilish nondeterminism.

To see the problem, let's look again at our example.

Example 4 Let us consider again ✸✷¬a. An NFA for A✸✷¬a is:

The product AD ×A✸✷¬a is:

The transition (shoot, not alive, working) may change or not the NFA A✸✷¬a state to final. If we give this choice to the environment we give it too much power since it may force looping in a non-final state forever without realizing that we have fulfilled our goal. If we give the choice to the agent then we are giving it clairvoyance, which is unrealistic.

So, before applying the product we need to determinize the NFA for the LTLf /LDLf formula. Unfortunately the resulting DFA can be exponential in the NFA, though is not in many cases (we briefly return to this point in the conclusion).

DFA Games. DFA games have been used for LTLf /LDLf synthesis [De Giacomo and Vardi, 2015], and seamlessly apply to our case. For disjoint sets F and A, a DFA game G = (2F∪A, S, sinit, ϱ, F) has: alphabet 2F∪A; states S; initial state sinit; partial transition function ϱ : S ×2F∪A → S; and final states F. The game evolves as follows: from a current state s, the agent chooses an action a ∈ A (for which ϱ(s, [a, E]) is defined for some E), then the environment sets the fluent values E, and then the game moves to the state ϱ(s, [a,E]). The evolution ends, and is won by the agent, if a state of F is reached. A strategy in G is a partial function f : (2F )∗ →A. We recast the notions of trace and f-trace to DFA games. A strategy is winning if each f -trace in G starting in the initial state is finite and terminates in F.

To compute winning strategies in DFA games we define the universal preimage for a ∈ A, X ⊆ S: PreA(a, X) = {s ∈ S | ∀E ∈ 2F , if s′ = ϱ(s, [a,E]) then s′ ∈ X}. A state s is in PreA(a,X) if from s and action a, all possible effects E chosen by the environment result in a state of X. Let PreC(X) = {s ∈ S : ∃a ∈ A, s ∈ PreA(a,X)}. The winning regionWin of a DFA game G, i.e., states fromwhich the agent has a winning strategy, is characterized by leastfixpoint, Win = µX.F ∪ PreC (X), which can be computed by the following algorithm:

• Win1 = F (the final states of G);
• Wini+1 =Wini ∪PreC(Wini);
• Win = ⋃i≤|S| Wini.

Note: computingWin is linear in the number of states of G. If the initial state sinit is inWin, we can extract a winning strategy as follows: define ω : Win \ F → 2A as mapping s ∈ Wini+1 \ Wini to the set of all a ∈ A such that s ∈ PreA(a,Wini). Every way of restricting ω(s) to return only one action (chosen arbitrarily) gives a winning strategy for G.

Correctness. To see that Algorithm 1 is correct, note that there is a tight correspondence between strategies in D and strategies in AD × Aϕ. It is straightforward to see that a strong solution to D corresponds to a winning strategy in the DFA Game AD × Aϕ, and vice versa.

Notice that the algorithm for solving DFA games generates memoryless strategies for the DFA game, which include in the state the status of the formula. These strategies correspond to memoryfull strategies in the original domain D (the memory being the states of the DFA for the goal).

Complexity analysis. For the upper bounds, generate the states of D explicitly and apply Alg. 1, and for the lower bounds consider hardness of standard FONDunr [Rintanen, 2004] and LTLf synthesis [De Giacomo and Vardi, 2015]:

Theorem 1 Solving FONDunr for LTLf /LDLf goals is:

• EXPTIME-complete in the size of the domain;
• 2EXPTIME-complete in the size of the goal.

It is interesting to observe that if the goal is a reachability goal of the form ✸G then the cost wrt the goal becomes polynomial (since it amounts to propositional evaluation). Moreover if for a given LTLf /LDLf goals the determinization step does not cause a state explosion (which, as mentioned, is often the case) the complexity wrt the goal is EXPTIME.

4 FOND Planning in Fair Environments

Consider nondeterministic domains D = (2F , A, s0, δ, α) (as before) although now assume a fair environment [Cimatti et al., 2003; Daniele et al., 1999; Pistore and Traverso, 2001; Geffner and Bonet, 2013; Sardi˜na and D'Ippolito, 2015]. Such a system evolves as before except the environment is assumed to satisfy a fairness assumption, which says (roughly speaking) that if an action a is applied in a state s again and again, then every possible effect will eventually happen.

Formally, a (finite or infinite) trace τ = s0, a0, s1, a1, . . . of D is fair if for every (s, a) that occurs infinitely often in τ , if (s, a, s′ ) ∈ δ then also (s, a, s′ ) occurs infinitely often in τ . Note, in particular, that every finite trace is fair.

Given a nondeterministic domainD and an LTLf /LDLf formula ϕ, a strategy f is a fair solution in D for goal ϕ if every fair f-trace of D starting in the initial state is finite and satisfies ϕ. Note that strategy f does not impose any constraints on infinite traces that are unfair.

Relationship with FONDfair for reachability goals. When the goal is ✸G we get the standard form for FONDfair, which is known to be EXPTIME-complete in the size of the set of fluents F [Rintanen, 2004]. There is an equivalent definition of solving FONDfair for reachability goals that can be expressed in the temporal logic CTL [Daniele et al., 1999; Pistore and Traverso, 2001; Cimatti et al., 2003]. It captures the intuition that the agent can ensure that, if the goal has not yet been reached, then should the environment ever choose to co-operate, the goal could be reached. Informally, a strategy f is a strong-cyclic solution for G if every state reachable using f can be extended, again using f , to a terminal state satisfying G. Equivalence between strong-cyclic solutions and fair solutions is discussed in [Sardi˜na and D'Ippolito, 2015].

Relationship with Probabilistic Planning. We now show how to give a probabilistic interpretation to fair solutions. This connection has been noted for reachability goals [Rintanen, 2004]. A probabilistic domain (including initial state)

is a tuple Dp = (2F ,A, s0, p, α) where: F is a set of fluents (atomic propositions); A is a set of actions; 2F is the set of domain states; s0 is the initial state (initial assignment to fluents); ∅ ̸= α(s) ⊆ A represents action preconditions (we assume no dead-ends); and p : 2F ×A → Dbn(2F ) maps pairs (s, a) with a ∈ α(s) to a probability distribution on domain states. Such a system evolves (forever) as follows: from a given state s, the agent chooses an action a ∈ α(s), after which the environment chooses a successor state s′ according to the distribution p(s, a).

A strategy for a probabilistic domain is a total function f : (2F )+ → A such that for every u ∈ (2F )+ we have that f(u) ∈ α(last(u)). A strategy f induces a probability distribution Prf,Dp over the set of all infinite traces of Dp [Puterman, 2005]. Thus, for a measurable set X of infinite traces, we write Prf,Dp (X) for the probability of the set of f-traces in Dp that are in X (all our sets are seen to be measurable). An infinite trace of Dp is fair if for every (s, a) that occurs infinitely often in τ, if p(s, a)(s′ ) > 0 then also (s, a, s′ ) occurs infinitely often in τ . A strategy is finite-state if it is induced by a finite-stateMoore machine. If f is finitestate, writing R for the set of fair f-traces of Dp, we have Prf,Dp (R) = 1 [Kemeny and Snell, 1976].

We now describe how to translate fair domains to probabilistic domains. Given a FONDfair D define a probabilistic domain Dp as follows: add a fluent done, and an action win! that has no preconditions, and its effects are to make the fluent done true; add ¬done to the precondition of every other action; replace δ with any probability distribution p : 2F × A → Dbn(2F ) such that p(s, a)(s′ ) > 0 iff (s, a, s′ ) ∈ δ. Given a finite trace τ of D that ends in a state s, define the infinite trace ext(τ) = τ · (win! · s)ω of Dp. Observe that ext(τ) is fair in Dp. For a set X of finite traces of D, define the set ext(X) = {ext(τ) : τ ∈ X} of infinite traces of Dp.

We say that an infinite trace τ of Dp satisfies an LTLf /LDLf formula ϕ if τ = ext(τ ′ ) for some finite trace τ ′ of D, and τ ′ satisfies ϕ. Let [ϕ] denote the set of infinite traces of Dp satisfying ϕ. There is a tight correspondence between strategies in D and in Dp.

Theorem 2 Let D be a nondeterministic domain, ϕ an LTLf /LDLf formula, and consider finite-state strategies f in D and g in Dp that correspond. Then, f is a fair solution to D for goal ϕ iff Prg,Dp ([ϕ]) = 1.

Proof. Left to Right: Suppose f is a fair solution. Let R be the set of all fair f-traces in D starting in the initial state. By assumption, all traces in R are finite and satisfy ϕ, thus ext(R) ⊆ [ϕ]. Let R′ be the set of fair g-traces. By remark above, Prg,Dp (R′ ) = 1. Since Prg,Dp (·) is monotone, it is sufficient to prove that R′ ⊆ ext(R). So, aiming for a contradiction, let τ ∈ R′ \ ext(R). But τ is an infinite trace that doesn't mention win!, and thus (by definition of g, Dp) is also an f-trace. Moreover, since τ is fair in Dp it is also fair in D. This contradicts that every fair f-trace in D is finite.

Right to Left: Suppose Prg,Dp ([ϕ]) = 1 and τ is an f-trace of D starting in the initial state that does not satisfy ϕ. If τ is finite then Prg,Dp ({ext(τ)}) > 0 contradicting the assumption that Prg,Dp ([ϕ]) = 1. If τ is infinite then τ is also a fair g-trace in Dp. Thus, it reaches a bottom strongly-connected component C of the finite-state Markov chain induced by Dp and g. In no state of C is done true. Thus, every infinite trace of Dp that reaches C does not satisfy ϕ. But the probability of reaching C is non-zero, contradicting Prg,Dp ([ϕ]) = 1.

Along the lines of [Brafman et al., 2018] we can use this theorem to reduce solving FONDfair with LTLf /LDLf goals to solving MDPs, i.e., take the product of the DFA Aϕ with Dp to get an equivalent MDP Aϕ × Dp with reachability goal G, and use standard MDP planners to decide "almost sure reachability", i.e., if there is a policy π ensuring the probability of reaching G is equal to 1. On the other hand, almost sure reachability can be solved by a nested fixpoint construction [de Alfaro et al., 2007], which we use in our automatatheoretic technique.

Automata-theoretic solution. We give a direct automatatheoretic technique for solving FONDfair for LTLf /LDLf (again, complexities are wrt explicit representation of D).

Algorithm 2: FONDfair for LDLf /LTLf goals

Given LTLf /LDLf domain D and goal ϕ

• 1: Compute DFA corresponding to D (poly)
• 2: Compute NFA for ϕ (exp)
• 3: Determinize NFA to DFA (exp)
• 4: Compute product with DFA of D (poly)
• 5: Solve fair DFA game (poly)
• 6: Return winning strategy if one exists

The steps are the same as for FONDunr, except that the resulting game is a fair DFA game instead of a DFA game.

Fair DFA Games. A fair DFA game G consists of the same components as a DFA game (2F∪A, S, sinit, ϱ, F). However, the notion of winning is different: a strategy f is winning for the fair DFA game G if every fair f-trace starting in the initial state terminates in a state of F. The idea for winning such games is that the agent should remain in a "safe area" from which it is possible to cooperatively reach the final state.

We already defined the universal preimage, we now define the existential preimage PreE(a, Y ) for a ∈ A and Y ⊆ S as: {s ∈ S | ∃E ∈ 2F , ∀s′ , if s′ = ϱ(s, [a,E]) then s′ ∈ Y }. Let PreAE(X, Y ) = {s ∈ S : ∃a ∈ A. s ∈ PreA(a, X) ∩ PreE(a, Y )} and define two nested fixpoints, a greatest (for safety) and least (for reachability):

This gives rise to a nested fixpoint computation: X0 = S (all states of G); Xi+1 = µY.F ∪ PreAE(Xi, Y ); Safe = ⋂i≤|S| Xi; where µY.F ∪ PreAE(Xi, Y ) is computed as Yi,1 = F; Yi,j+1 = Yi,j ∪ PreAE(Xi, Yi,j); Yi = ⋃j≤|S| Yi,j. Note. Computing Safe is quadratic in the number of states of G.

We can stratify Safe according to when a state enters the least fixpoint: Reach1 = F, Reachj+1 = Reachj ∪ PreAE(Safe,Reachj). Note that Safe = ∪j≤|S|Reachj. Define ω : Safe \ F → 2A as mapping s ∈ Reachj+1 \ Reachj to the set of all a ∈ A such that ∃E.ϱ(s, [a, E])∈Reachj .

Theorem 3 For a state s ∈ S, we have s ∈ Safe iff there is a winning strategy for the fair DFA game G starting in state s.

Proof (sketch). Left to Right: Let f : Safe \ F → A be a function, restricting ω(s), i.e., such that f(s) ∈ ω(s). Let Gf be the DFA formed from G by keeping transitions of the form (s, [f(s), E], s′ ), i.e., Gf is the game in which the player commits to playing f. We use the following properties of s ∈ Safe: (i) every path from s in Gf is in Safe until it reaches F, (ii) there is a path from s in Gf that reaches F.

So, let τ be a fair f-trace in G. Then τ is a trace in Gf with the following property (⋆): if s, s′ are in the same strongly connected component of Gf and τ visits s infinitely often then τ visits s′ infinitely often (indeed, induct on the length n of the shortest path from s to s′ : if n = 0 we are done; if n > 0 then there is an edge (s, [f(s),E], t) in Gf such that the length from t to s is < n, but by fairness t is visited infinitely often). Thus, τ eventually reaches a bottom strongly connected component C of Gf (since Gf is finite). By (i) and (⋆) C ⊆ Safe, and by (ii) and (⋆) C ∩ F ̸= ∅. Thus, by (⋆) the trace τ reaches F, as required.

Right to Left: We can stratify the complement of Safe according to when a state is thrown out of the greatest fixpoint. E.g., if s ∈ X0 \ X1 then there s cannot reach F, and if s ∈ X1 \ X0 then s cannot reach F without the environment moving to a state that cannot reach F, etc. In other words, from s ̸∈ Safe, no matter what the strategy f is, after finitely many steps a trace will visit a state from which there is no path to F. Thus there are fair f-traces that never visit F.

Correctness and complexity analysis. As before, correctness follows from the tight correspondence between strategies in D and strategies in AD × Aϕ. Regarding complexity, our automata-theoretic technique gives us that solving FONDfair for LTLf /LDLf goals is in EXPTIME wrt the domain and 2EXPTIME wrt the goal. These bounds are tight:

Theorem 4 Solving FONDfair for LTLf /LDLf goals is:

• EXPTIME-complete in the size of the domain;
• 2EXPTIME-complete in the size of the goal.

Proof (sketch). It remains to argue the lower bounds. EXPTIME-hardness wrt the domain comes EXPTIMEhardness of FONDfair for standard reachability goals. Also, 2EXPTIME-hardness wrt the goal follows from 2EXPTIMEhardness wrt the goal of FONDunr. Indeed, let D be a nondeterministic domain and ϕ an LTLf goal. Build a planning domain D′ which simulates D but has an additional counter that increases with every action until it reaches 2|F| + 1, at which point no action is available. Let f be a strong solution to D. Note that every f-trace visits each state of D at most once (for otherwise there would be an infinite f-trace). Thus, f is also a fair solution to D′ for ϕ. Conversely, let g be a fair solution to D′ for g. Then every fair g-trace is finite and satisfies ϕ. But all traces of D′ are fair and finite. Thus g is a strong solution to D.

Actually, we can strengthen this and give lower bounds on the solution memory:

Theorem 5 Memory for strategies solving FONDunr and FONDfair for LTLf (and hence LDLf ) goals may be required to be doubly-exponential in the size of the goal.

Proof (sketch). We present the proof for fair solutions (it can be adapted to strong solutions). Following [Kupferman and Vardi, 2005; Schewe, 2006], we consider the language Ln: {{0, 1, #}∗ ·#·w·#·{0, 1, #}∗ ·$·w·#·#∗ | w ∈ {0, 1}n } A word is in Ln iff the suffix of length n that comes after the $ appears somewhere before the $. The smallest DFA that accepts Ln has at least 22n states [Chandra et al., 1981]. This is because reaching the marker $, the DFA should remember the possible set of words in {0, 1}n that have appeared before. We can specify Ln with an LTLf formula ΦLn of length quadratic in n. The formula ΦLn makes sure that there is only one $ in the word and that eventually there exists a position in which # is true and the i-th letter from this position, for 1 ≤ i ≤ n, agrees with the i-th letter after the $, namely:

[¬$ U($ ∧ ◦(0 ∨ 1) ∧ ◦2 (0 ∨ 1) ∧ · · · ◦n ((0 ∨ 1) ∧ ◦✷#)] ∧✸[# ∧ ∧1≤i≤n (◦i 0 ∧ ✷($ ⊃ ◦i 0) ∨ ◦i 1 ∧ ✷($ ⊃ ◦i 1))]

Define a planning domain with actions step, accept, reject, and fluents Stop, 0, 1,#, $. Initially ¬Stop, ¬Accepted, ¬Rejected hold. The precondition of step is ¬Stop, and its nondeterministic effects make one of 0, 1, # $ true (and the rest false) and, simultaneously, either Stop or ¬Stop. The precondition of accept (resp. reject) is Stop, and its effect is Accepted (resp. Rejected). The goal is: (ΦLn ⊃ ✸Accepted) ∧ (¬ΦLn ⊃ ✸Rejected).

While ¬Stop holds (as it does initially), the only possible action is step. By fairness, eventually Stop holds and the actions accept and reject can be used to set either Accepted or Rejected to be true. The goal requires that if the produced trace is in Ln (resp. not in Ln) then the agent played accept (resp. reject). Intuitively, to win, the strategy needs to memorize all possible words of length 2n , hence it cannot be smaller than 22n . In particular, a winning strategy executed in the domain becomes a DFA for recognizing Ln but this cannot be smaller than 22n .

5 Conclusions

We conclude by observing that DFA games with or without fairness can be seen as variants of FONDfair and FONDunr problems for reachability goals. Hence, heuristics, knowledge and solvers developed by the planning community for the latter can immediately be applied. This is a crucial point for effectiveness and scalability of the techniques.

We remark that although the 2EXPTIME bound is high, in many cases the actual complexity is much smaller, e.g., it is polynomial for ✸G, i.e., for reachability of a propositional goal G. Moreover, often the determinization step in the technique, which is in general exponential, is not needed if the automaton corresponding to the formula is already deterministic. This is, e.g., the case for the LTLf formulas used in declarative business process modeling [van der Aalst et al., 2009], which are Boolean combinations of patterns that correspond to very small deterministic automata. Also, even when determinization cannot be avoided, it is often the case that it does not produce an exponential blow-up as shown in [Tabakov and Vardi, 2005]. Finally, the experiments in [Camacho et al., 2017b] confirm experimentally actual feasibility in spite of 2EXPTIME-completeness.