Planning for LTLf /LDLf Goals in Non-Markovian Fully Observable Nondeterministic Domains

1 Introduction

Most formalisms for planning and reasoning about actions make the Markov assumption: the executability of an action and its effects are entirely determined by the current state [Reiter, 2001; Geffner and Bonet, 2013]. The same assumption plays a central role in Markov Decision Processes (MDPs) [Puterman, 2005]. Here, we want to consider systems with non-Markovian dynamics, as was done in work on reasoning about actions where executability conditions and effects of an action depend not only on what holds when the action is to occur, but also on whether certain conditions were satisfied in the past [Giunchiglia and Lifschitz, 1995; Mendez et al., 1996; Gonzalez et al., 2005; Gabaldon, 2011].

To get an intuition of non-Markovian dynamics, consider the following example taken from [Gabaldon, 2011]: Imagine a robot that works in a biological research facility with different safety-level areas. The dynamics is such that a material will be considered contaminated after the robot touches it if the robot has been to a low safety area or has directly been in contact with a hazardous material, and has not been to the disinfection station since then. So the effect of touching the material depends on the history of robot activities.

Situations in which the dynamics of the domain depend on the history are common. In simple cases, it is not difficult to avoid explicit reference to the whole history by extending the state with suitable auxiliary state variables that preserve the necessary information from the history. But in general it may not be obvious how to do so, and the resulting Markovian representation of the domain may be substantially more complex, with a larger number of state variables and corresponding description of their dynamics. In fact, as we show in this paper, this may require, in the worst case, a doubly exponential blowup in the number of states w.r.t. a non-Markovian representation expressed using temporal logic (this answers an informal conjecture in [Gabaldon, 2011]). This potential blowup makes it implausible that a human designer can come up with the suitable control variables to describe the dynamic as a Markovian system in the general case. Moreover, making intuitive sense of these auxiliary state variables may be difficult or even impossible.

In this paper we consider non-Markovian specification in the context of planning in Fully Observable Nondeterministic Domains (FOND), see e.g., [Geffner and Bonet, 2013], and investigate strong planning for temporally extended goals expressed in linear-time-logics over finite traces, namely LTLf , and its extension LDLf [De Giacomo and Vardi, 2013; Camacho et al., 2017; De Giacomo and Rubin, 2018].

For concreteness, we introduce Temporal FONDs (or TFONDs) as a means to succinctly and declaratively define non-Markovian dynamics in planning domain, based on the use of LTLf /LDLf . We provide the following results:

• We devise a technique for planning in LTLf /LDLf TFONDs for LTLf /LDLf temporally extended goals. This technique is based on a reduction to a (larger) standard FOND planning problem, and hence can exploit the highly optimized FOND planners (such as NDP [Alford et al., 2014], FIP [Fu et al., 2016], MyND [Mattm¨uller et al., 2010], Gamer [Kissmann and Edelkamp, 2011], PRP [Muise et al., 2012], and FOND-SAT [Geffner and Geffner, 2018]).
• We caracterize the computational complexity of planning for LTLf /LDLf goals in TFOND as 2EXPTIME-complete both in the domain and in the goal.
• We also show that TFONDs are able to capture all NonMarkovian Nondeterministic Fully Observable Planning

Domains (NMFONDs) in which the dependency on the history is "finite state" in a precise formal sense.

Finally we look at partially observable nondeterministic planning domains (PONDs) and we show that these are equivalent in a strong sense to LDLf TFONDs defined over the observable variables only. This result is quite interesting since it removes completely the unobservable variables, whose nature is ambiguously being postulated by the modeller, but may be intangible in reality. The ability to remove the dependence on unobservable variables is likely to help learn such models from data, which typically consists of observable entities only.

2 Preliminaries

We breifly recall the main notions regarding LTLf /LDLf and FOND planning. LTLf is the Linear-time Temporal Logic LTL interpreted over finite traces [De Giacomo and Vardi, 2013], instead of infinite ones [Pnueli, 1977]. Given a set P of propositional symbols, LTLf formulas ϕ are:

where φ is a propositional formula over P, ○ is the next operator and U is the until operator. We use the usual abbreviations such as ϕ1∨ϕ2 ≐ ¬(¬ϕ1∧¬ϕ2); eventually as ◇ϕ ≐ true U ϕ; always as ◻ϕ ≐ ¬◇¬ϕ; and ●ϕ ≐ ¬○¬ϕ. (Note that on finite traces ¬○ϕ /≡ ○¬ϕ.) LTLf is as expressive as FO (first order logic) over finite traces and star-free regular expressions (RE), thus strictly less expressive than RE, which in turn are as expressive as monadic second order logic over finite traces. RE themselves are not convenient for expressing temporal specifications, since they miss direct constructs for negation and conjunction, and adding them makes reasoning non-elementary, see e.g., [Lodaya, 2012].

For this reason, [De Giacomo and Vardi, 2013] introduced LDLf , linear dynamic logic on finite traces, which merges LTLf with RE, through the syntax of the well-known logic of programs PDL, propositional dynamic logic [Fischer and Ladner, 1979; Harel et al., 2000; Vardi, 2011], but interpreted over finite traces. Here, following, [Brafman et al., 2018], we consider a variant of LDLf that works also on empty traces:

where tt stands for logical truth; φ is a propositional formula over P (including the propositional formula true, not to be confused with tt ); ϱ denotes path expressions, which are RE over propositional formulas φ, and the test construct ϕ? typical of PDL. We abbreviate [ϱ]ϕ ≐ ¬⟨ϱ⟩¬ϕ as in PDL, ff ≐ ¬tt for false, and φ ≐ ⟨φ⟩tt to denote an occurence of propositional formula φ. Intuitively, ⟨ϱ⟩ϕ states that, from the current step in the trace, there exists an execution satisfying the RE ϱ such that its last step satisfies ϕ, while [ϱ]ϕ states that, from the current step, all executions satisfying the RE ϱ are such that their last step satisfies ϕ. Tests are used to insert into the execution path checks for satisfaction of additional LDLf formulas. As mentioned LDLf is as expressive as MSO over finite words. It captures LTLf , by seeing next and until as the abbreviations ○ϕ ≐ ⟨true⟩(ϕ ∧ ¬end) and ϕ1 U ϕ2 ≐ ⟨(ϕ1?; true)∗ ⟩(ϕ2 ∧ ¬end), and any RE r, with the formula

⟨r⟩end, where end ≐ [true]ff expresses that the trace has ended. Note that in addition to end we can also denote the last element of the trace as last ≐ ⟨true⟩end.

An NFA is a tuple A = ⟨Σ,Q, q0, δ, F⟩, where: (i) Σ is the input alphabet of the automaton; (ii) Q is the finite set of states; (iii) q0 ∈ Q is the initial state; (iv) δ ⊆ Q×Σ×Q is the transition relation; (v) F ⊆ Q is the set of final states. A DFA is an NFA where δ is a function δ ∶ Q × Σ → Q. By L(A) we mean the set of all traces over Σ accepted by A.

We can associate each LTLf /LDLf formula ϕ with an (exponentially large) NFA Aϕ = ⟨2P ,Q, q0, δ,F⟩ that accepts exactly the traces satisfying ϕ. The construction relies on the fact that (i) every LDLf formula ϕ can be associated with a polynomial alternating automaton on words (AFW) accepting exactly the traces that satisfy ϕ [De Giacomo and Vardi, 2013], and (ii) every AFW can be transformed into an NFA, see, e.g., [De Giacomo and Vardi, 2013].

The NFA Aϕ can be transformed into a DFA, in exponential time, and then possibly put in (the unique) minimal form, in polynomial time [Rabin and Scott, 1959]. Thus, we can transform any LTLf /LDLf formula into a DFA of double exponential size. While this is a worst-case complexity, in most cases the size of the DFA is actually manageable [Tabakov and Vardi, 2005]. Moreover, determinization can be performed on-the-fly, without the need to explicitly construct the DFA by progressing all possible states the NFA can be in after consuming the next trace symbol. We accept the trace iff, once it has been completely read, the set of possible states contains a final state. This on-the-fly construction allows for a compact (i.e., logarithmically factorized) representation of the DFA, and it is, e.g., exploited in [Camacho et al., 2018a; Brafman et al., 2018].

Fully Observable Nondeterministic Domains (FOND) are commonly studied in Planning see e.g., [Geffner and Bonet, 2013]. Here we consider the domains to be rooted, i.e., they include the initial state and formally define FOND as a tuple D = (P,A, 2P , s0, tr) where: 1. P is a finite set of atomic propositions also called fluents; 2. A is a finite set of actions; 3. 2P is the set of domain states; 4. s0 is the initial state (initial assignment to fluents); 5. (s, a, s′ ) ∈ tr represents action effects (including frame assumptions), and implicitly also actions preconditions: action a is possible in state s if (s, a, s′ ) ∈ tr, for any s′ . 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 P, i.e., logarithmic in the number of states. Intuitively, a nondeterministic domain evolves as follows: from a given state s, the agent chooses a possible action a (i.e., such that there exists an s′ such that (s, a, s′ ) ∈ tr), after which the environment chooses a successor state s′ with (s, a, s′ ) ∈ tr. The agent can choose its action based on the history of states so far (i.e., the agent has full observation).

Given a domain D and a LTLf /LDLf goal formula ϕ over fluents P, a strategy f is a strong solution to D for goal ϕ, if every f-trace of D is finite and satisfies ϕ. A solution this problem is given in [De Giacomo and Rubin, 2018] (see also [Camacho et al., 2018a; 2018b]):

Solving FOND for LTLf /LDLf goals

Given FOND D and goal ϕG

• 1: Compute DFA AϕG for ϕG (2exp in ϕG)
• 2: Compute product FOND Dp of D and AϕG (poly)
• 3: Solve FOND Dp for goal g = {(s, q) ∣ q ∈ FG}

(poly in the number of states of Dp)

Here the product FOND Dp = (Pp,A,Sp, sp,0, trp) of a FOND D = (P,A, 2P , s0, tr) and a goal DFA AϕG = (2P ,QG, qG,0, δG,FG) is defined as follows: (i) Pp = P ∪ PQG , where PQG is a set of additional fluents for the logarithmic representation of QG, (ii) Sp = 2P ×QG, (iii) ((s, q), a, (s′ , q′ )) ∈ trp iff (s, a, s′ ) ∈ tr and δG(q, s′ ) = q′ (where, we project s′ on the propositions in P only). We have following complexity characterization (note that the complexity in the domain is the same as in classical FOND [Rintanen, 2004]):

Theorem 1. [De Giacomo and Rubin, 2018] Planning for LTLf /LDLf goals in FONDs is: EXPTIME-complete in the domain (compactly represented) and 2EXPTIME-complete in the goal.

3 NMFONDs

We now introduce the basic semantic model of a NonMarkovian Nondeterministic Fully Observable Planning Domain (NMFOND). An NMFOND is very much like a standard FOND, except that the effect of an action depends on the entire history of states (trace) of the system. A Non-Markovian Nondeterministic Fully Observable Planning Domain (NMFOND) is a tuple D = (P,A,S, s0, tr), where 1. P is finite set of primitive propositions (the fluents); 2. A is a finite set of actions; 3. S = 2P is the set of possible truth assignments to P , which we still call domain states; 4. s0 ∈ S denotes the initial state (with an initial dummy action a0); 5. tr ∶ S+ ×A×S is a transition relation, such that ((s0, . . . , sk), a, s′ ) ∈ tr if given the sequence of states s0, ..., sk starting from the initial state s0 and an action a, the state s′ is a possible outcome resulting from executing the action a after traversing s0, ..., sk. (We use the standard notation S+ for denoting S ∪ S×S ∪ S×S×S ⋯.) Note that if tr ∶ S+ ×A×S has in fact the form tr ∶ S ×A×S, i.e., instead of the sequence s0, . . . , sk we consider only one state s, then the NMFOND is actually a standard FOND.

A goal for an NMFOND is a subset G of S+ , denoting the desired traces. A plan is a partial function p ∶ S+ → A such that for every w ∈ S+ , if p(w) is defined then ∃s′ .(w, p(w), s′ ) ∈ tr (the action chosen by p(w) is executable). If p(w) is undefined, we write p(w) = bot. A trace τ is generated by p, or simply a p-trace, if (i) for any prefix s0, . . . , sk, sk+1 of τ we have that p(s0, . . . , sk) = a for some action a and ((s0, . . . , sk), a, sk+1) ∈ tr; and (ii) if τ is finite, say τ = s0, . . . , sn, then p(s0, . . . , sn) = bot.

Given an NMFOND D and a goal G, a plan p realizes G in D if every p-trace of D satisfies G.

4 TFONDs

A declarative way to specify NMFONDs is by using a logical language to describe properties of finite traces, and a natural choice for such a logical formalism is LTLf and its extension LDLf . Hence, we introduce Temporal FONDs (TFONDs). Formally a TFOND DL is a tuple DL = (P,A,S, s0, trL), where P , A, S and s0 are as NMFONDs, while the transition function is defined implicitly by trL as follows: trL is given in terms of a set T of triples of the form:

where ϕ is a temporal LTLf /LDLf formula over P, a ∈ A, and φ is a propositional formula over P. Each of the triples (ϕ, a, φ) states that if the trace s0, . . . , sk from the initial state s0 to the current state sk satisfies ϕ then performing action a may bring about any state s′ where φ is true. We call LTLf (resp. LDLf ) TFONDs those TFONDs that use LTLf (resp. LDLf ) for ϕ. Given a trace s0, . . . , sk and an action a, the possible next states are those satisfying the propositional formula:

In other words: ((s0, . . . , sk), a, s′ ) ∈ tr iff s′ ⊧ ⋀(ϕ,a,φ)∈T,s0,...,sk⊧ϕ φ. Note that if ⋀(ϕ,a,φ)∈T,s0,...,sk⊧ϕ φi ≡ false then there is no s′ ⊧ ⋀(ϕ,a,φ)∈T,s0,...,sk⊧ϕ φi, i.e., there are no transitions at all (we can say that the precondition of the actions are violated). Otherwise there is one transition for each s′ satisfying the condition. Note also that if for no ϕ we have s0, ..., sk ⊧ ϕ then there are no restrictions on s′ , i.e., the transition nondeterministically goes to every possible state.

Observe that if one restricts ϕ to be propositional then triples (ϕ, a, φ) get a quite standard (Markovian) meaning, similar, say, to PDDL conditional effects: if the current state s satisfies condition ϕ then by doing action a one brings about effect φ. Note that, differently from PDDL, we need to specify persistence explicitly using further triples. This is easy to do when capturing PDDL, but having such specification derived automatically in the general case, e.g., by exploiting the semantic principle of "explanation closure" used for deriving Successor State Axioms in [Reiter, 2001], requires further studies. PDDL also allows for "axioms" that define derived predicates and can substantially simplify the representation of planning problems [Thi´ebaux et al., 2005]. These can be introduced in TFONDs as well, and are related to state constraints [Reiter, 2001]. We leave both issues to future work. Finally, observe that, if in a TFOND we do not constrain the effects of an action a through some triple then the next state can be arbitrary. But notice that if we want to constrain the effects to be always within, say, φ1 . . . φn, similarly to a "one-of" clause in PDDL, we can simply add the triple (true, a, φ1 ∨ . . . ∨ φn).

Consider the example in the introduction [Gabaldon, 2011], and suppose we have the following fluents among other: Material-is-Contaminated (mci, for each material i); Robot-inLow-Safety-Area (rlsa); Robot-in-Contact-with-HazardousMaterial (rchm); Robot-in-Disinfection-Station (rds), and action robot-touched-material i (touchi, for each material i) Then the (non-Markovian) effect "a material i will be considered contaminated after the robot touches it if the robot has been to a low safety area or has directly been in contact with a hazardous material, and has not been to the disinfection station since then" can be specified in LDLf as:

which says that, if trace s0, ..., sk from the initial instant 0 to the current instant k satisfies the formula ⟨true∗ ; (rlsa ∨ rchm); (¬rds)∗ ⟩end, i.e., s0, ..., sk belongs to the regular language true∗ ; (rlsa∨rchm); (¬rds)∗ , then by doing action touchi we get to a state sk+1 where mci holds i.e., where the material i is contaminated.

5 Planning in TFONDs for LTLf /LDLf Goals

Next we look into solving planning in TFONDs for LTLf /LDLf goals. We start by observing that planning in TFONDs even for reachability goals is at least as difficult as LTLf /LDLf synthesis, which is 2EXPTIME-complete [De Giacomo and Vardi, 2015]. Consider a very simple TFOND DL = (P,A, 2P , s0, trL) with a single triple (ϕ, stop,Done), where stop is an action in A and Done a fluent in P, and consider as the goal reaching a state where Done is true. Then there exists a (strong) plan for reaching Done if and only if the agent controlling actions A has a winning strategy against the environment controlling P. So in general, planning in TFONDs can be difficult. But how can we solve it at all?

We now show that TFONDs can be translated into FONDs with additional fluents. To do so we first introduce what we call finite NMFONDs, and show that TFONDs can be translated into them. A finite NMFOND D = (P,A,S, s0, tr) is an NMFOND whose transition relation tr is generated by a finite state transition transducer Tr = (Q, q0, δ, ϱ): (i) Q is the finite set of the transducer states; (ii) q0 is the initial state of the transducer; (iii) δ ∶ Q×S →Q is the transducer (deterministic) transition function; (iv) ϱ ∶ Q×A× S is the output function of the transducer. As usual, we extend the transition function δ ∶ Q × S → Q to sequences, i.e., δ ∶ Q × S+ → Q, in the standard way [Hopcroft and Ullman, 1979].

Tr defines the NMFOND transition relation tr ∶ S+×A×S as:

Thus, the information about the current trace s1, . . . , sk relevant to the future behavior of the NMFOND is summarized by δ(q0, (s1, . . . , sk)), and the transition relation tr is represented by making use of δ together with ϱ.

Now we show that given a TFOND DL, we can construct an equivalent finite NMFONDD. Let us consider the set T of formulas of the form (ϕ, a, φ) defining trL. For convenience let's enumerate the triples in T as (ϕ1, a1,φ1), . . . , (ϕnan,φn). For each formula ϕi, we build the corresponding DFA Ai = (2P ,Qi, qi,0, δi,Fi), i.e., an automaton that accepts exactly those traces satisfying this formula. We define a corresponding finite NMFOND D = (P, A, S, s0, tr) with tr generated by the transducer T r = (Q, q0, δ, ϱ) with: 1. Q = Q0×⋯×Qn; 2. q0 = q1,0, . . . , qn,0; 3. δ ∶ Q × S → Q where δ((q1, . . . , qn), s) = (q′1 , . . . , q′n )) iff q′i = δi(qi, s); 4. ϱ ∶ Q × A × S where ((q′1 , . . . , q′n ), a, s′ ) ∈ ϱ iff s′ ⊧ ⋀i∶(ϕi,a,φi),q′i ∈Fi φi. The construction is based on computing the automata for the LTLf /LDLf formulas in the triples, and then run all of them in parallel. The resulting NMFOND D is equivalent to the TFONDDL in the sense that they produce sets of traces that are isomorphic (i.e., in bijection).

Next we show that given a finite NMFOND D = (P,A,S, s0, tr) with tr generated by any finite transducer Tr = (Q, q0, δ, ϱ), we can construct an equivalent FOND Df = (Pf ,A,Sf , sf,0, trf) as follows: 1. Pf = P ∪ Paut where P is the finite set of primitive propositions and Paut are propositions for the separate binary encoding of states Q of the transducer Tr; 2. A is the finite set of actions of D; 3. Sf is the set of possible truth assignments to Pf , which we call (domain) states; 4. sf,0 = s0 ∪ q0, where s0 is a truth assignment over P denoting the initial state, and q0 is the (encoding of) the initial state of Tr; 5. tr ∶ Sf ×A×Sf , such that:

Essentially, since the aspects of the history that are relevant to future transitions in an NMFOND can be summarized by some state q ∈ Q, if we maintain both the current element of Q and of S, we have all the information that we need.

Again, the finite NMFOND D and the resulting finite FOND Df are equivalent in the sense that they produce sets of traces that are isomorphic (i.e., in bijection). Hence, by combining above constructions we get a way of solving LTLf /LDLf TFOND planning.

Solving TFOND planning for LTLf /LDLf goals

Given a TFOND DL and a goal ϕG

• 1: Compute the finite NMFOND D (2exp in DL)
• 2: Compute FONDDf equivalent to D (poly)
• 3: Compute DFA AϕG for ϕG (2exp in ϕG)
• 4: Compute product FOND Dp of Df and AϕG (poly)
• 5: Solve FOND Dp for goal g = {(s, q) ∣ q ∈ FG}

(poly in the number of states of Dp)

Now we are ready to give the complexity characterization.

Theorem 2. Planning for finite trace temporal goals in LTLf /LDLf TFONDs is 2EXPTIME-complete in the domain and 2EXPTIME-complete in the LTLf /LDLf goals.

Proof (sketch). Membership comes from the construction above. Note that we easily devise a logarithmic representation in terms of fluents for Dp, however, solving FOND with a compact representation requires exponential time. The 2EXPTIME-hardness in the domain comes for the reduction of LTLf synthesis to TFONDs discussed above, which is for a fixed goal. The 2EXPTIME-hardness in the goal comes from planning for LTLf goals in FONDs [De Giacomo and Rubin, 2018], which are a special case of TFONDs.

The increase of complexity in the domain with respect to standard FOND is due to the succinctness of the representation that LTLf /LDLf formulas provide: the corresponding FOND requires exponentially many additional auxiliary fluents to logarithmically represent the DFAs for the formulas in the triples. This blowup is inevitable, and it makes it virtually impossible even for a human to come up directly with a FOND that captures dependencies on history that are conveniently expressed in LTLf /LDLf . This answers positively an informal conjecture in [Gabaldon, 2011].

Observe that, in practice, the 2EXPTIME worst-case complexity often does not manifest itself, since DFAs for LTLf /LDLf formulas are often small. Moreover, while, in general, deteminization of NFA can produce an exponential blowup, often the size of the DFA obtained (possibly after minimization) from a NFA, is comparable to that of the NFA itself [Tabakov and Vardi, 2005].

The reduction from TFOND to FOND can be seen as a way to synthesize automatically and conveniently "control fluents". To see this, consider the following example: an action "rest" has the effect of "putting the robot on maintenance" only when performed in an history satisfying ⟨(s; (a; b∗ ; c)∗ ; e)∗ ⟩end, i.e., a finite repetition of starting condition, followed by finite repetitions of three phases a ("preparing an item"), b ("cleaning the item"), c ("finalizing the item"), in which b can be repeated an arbitrary number of times (multiple cleaning phases may be needed), then followed by an end condition. The minimal DFA for this formula has 7 states (see, e.g., LDLf translator at https://flloat.herokuapp.com). Hence, if we factor these states into a binary representation we get 3 new control fluents. Note that it is not easy to come with these 3 fluents in the first place since it is not obvious how to assign intuitive meaning to them (after all they simply capture the dynamics of the DFA). As the number of these formulas grows, it becomes more and more unmanageable to come up with such control fluents directly. For example, if we replace the previous formula with ⟨(s; (a; b∗ ; c)∗ ; e)∗ ⟩end ∧ [true∗ ; (a; c; a; c)]ff , intuitively, disallowing two consecutive repetition of phase a and c in which cleaning does not occur, the number of states in the minimal DFA grows to 32 and hence we need 5 control fluents whose dynamics is rather obscure. Note also that if we consider the two formulas ⟨(s; (a; b∗ ; c)∗ ; e)∗ ⟩end and [true∗ ; (a; c; a; cx)]ff (whose minimal DFA has 6 states) separately, then we get 6 control fluents in total, which is more than what is actually needed.

6 TFONDs and finite NMFONDs

We can consider finite NMFONDs as the class of NMFONDs in which the dependency of transitions on the history is finitestate (i.e., can be expressed by using a finite state function). Above, we have seen that TFONDs can be translated into finite NMFONDs. We now show every finite NMFOND can be translated into LDLf TFONDs. Hence, LDLf TFONDs can be considered a sort of declarative counterpart of finite NMFONDs. Note that it is not true for LTLf TFONDs, since LTLf does not have the full power of RE needed for the translation.

Let D = (P,A,S, s0, tr) be a finite NMFOND with tr generated by a finite state transition transducer Tr = (Q, q0, δ, ϱ). We define the corresponding LDLf TFOND DL = (P,A,S, s0, trL), where the transition relation trL is generated by a set T of triples (ϕ, a, φ) defined as follows: For every transducer state q we consider the DFA AqTr defined as AqTr = (Q, q0, δ, {q}). That is, we consider the DFA obtained from the transducer by removing the output function ϱ and making final the state q. Notice that we have one AqTr for each q but all of them are identical except for the accepting state. From basic automata theory, we know that there is a regular expression rq that accepts the paths, i.e., the traces in S+ leading from the initial state q0 to q. Hence we can express reaching q by the LDLf formula ϕq = ⟨rq⟩end.

Using these formulas, for every transducer state q and every action a, we can define the triple (ϕq, a,φ) where φ = ⋁(q,a,s′ )∈ϱ s′ . As observed above, all DFA AqTr (for q ∈ Q) are identical except for the accepting state, hence each formula ϕq can be represented by the exact same DFA, except for the final states, which depend on the specific q. This means that when we transform such an LDLf TFOND DL = (P, A, S, s0, trL) into the corresponding finite TFOND using the construction above, we get exactly D = (P, A, S, s0, tr).

Theorem 3. Every finite NMFOND can be expressed as a LDLf TFOND, and vice-versa.

7 PONDs and TFONDs

In this section we consider Partially Observable Nondeterministic Planning Domains (POND). Our main result here is to show the equivalence between POND and (fully observable) TFONDs. While it is not surprising that a POND can be translated into a FOND - this is the well known belief state construction [Bonet and Geffner, 2000; Goldman and Boddy, 1996; Reif, 1984] - the significant aspect of this representability result is that the TFONDmakes no mention of the unobservable fluents, not even in the form of belief states. This is particularly significant in the case of learning, where we may have no a-priori knowledge of the nature of the hidden variables. Indeed, if we think of an agent situated in a domain, this agent has access only to its observations, and knowledge of hidden variables presupposes some prior knowledge pertaining to the understanding of the underlying structure of the domain.

We formally define POND as follows: A Partially Observable Nondeteministic Planning Domain (POND) is a tuple PO = ⟨O, U, A, S, S0, tr⟩, where 1. P = O ∪ U is a finite set of atomic propositions or fluents, partitioned ( O ∩ U = ∅) into observable ones O and unobservable ones U; 2. A is a finite set of actions; 3. S = 2O × 2U is the set of states of PO which are truth assignments to P partitioned into the one for O and the one for U. We denote states by (o,u) ∈ S 4. S0 = {(o0, u1), . . . , (o0, un)} is the set of possible initial states in S, all sharing the same observation o0; 5. tr ∶ S×A×S is the transition relation. POND is a Markovian model where both observable and unobservable fluents are nondeterministic. The dynamics of the state is Markovian and depends on the current value of all the fluents - both observable and unobservable, and the current action. Initially, the acting agent knows the value of all the observable fluents, and following each action, it gets to observe their new value. Note that the fact that P is divided into fully observable and unobservable fluents does not lead to loss of generality, as it easily captures a model with separate transition and observation functions, often adopted in POMDPs [Kaelbling et al., 1998].

A goal for a POND PO is a subset G of (2O )+ , denoting the desired sequences of observations. A plan is a partial function p ∶ (2O )+ →A such that for every w ∈ S+ , if p(w∣O) is defined (where w∣O is the projection of w onto O) then ∃s′ .(w, p(w∣O), s′ ) ∈ tr (the action chosen by p(w∣O) is executable). If p(w∣O) is undefined, we write p(w∣O) = bot. A trace τ is generated by p, or simply a p-trace, if (i) if s0, . . . sk is a prefix of τ then s0, . . . sk, p((s0, . . . , sk)∣O), sk+1 is also a prefix of τ, and (ii) if τ is finite, say τ = s0, . . . , sn, then p((s0, . . . , sn)∣O) = bot. Given a POND PO and a goal G, a plan p realizes G in PO if every p-trace of PO satisfies G. Notice that this definition is essentially the same as for NMFOND, with the only exception that the plan p takes as input only the sequence of observations, instead of the states themselves. As a result, the choice of action at each point of time depends only on what was observed so far.

We can reduce POND to FOND by the so called belief state construction [Goldman and Boddy, 1996; Reif, 1984]. Given a POND PO = ⟨O, U, A, S, S0, tr⟩ we can construct a FOND Dpo = ⟨O × 2U , A, Spo, b0, trpo⟩ defined as follows: 1. O × 2U are the available propositions (in fact, the propositions 2U are expressed in terms of knowledge, typically); 2. A is the original set of actions; 3. Spo = 2O × 22U is the set of states, of the form b = (o, u), where o is a truth assignments to the observable fluents, and u is a set of possible truth assignments for the unobservable fluents. Each state b is a belief-state; 4. b0 = (o0,u0) where u0 = {u ∣ (o0,u) ∈ S0} is the initial belief state corresponding to the set of (o0,u) considered initially possible, which forms the initial state of PO; 5. Spo × A × Spo is the transition function defined as follows: ((o,u), a, (o′ ,u′ )) ∈ trpo iff (i) for all u ∈ u there exists a u′ such that ((o,u), a, (o′ ,u′ )) ∈ tr; and (ii) u′ = {u′ ∣ u ∈ u and ((o,u), a, (o′ ,u′ )) ∈ tr}; notice that given o, u, a and o′ there exists a single u′ such that ((o, u), a, (o′ , u′ )) ∈ trpo.

Theorem 4 ([Goldman and Boddy, 1996; Reif, 1984]). A plan realizes G in PO iff it realizes G in Dpo.

We formalize the correspondence between POND and TFONDs whose fluents are restricted to the observable ones only. For convenience, we work with finite NMFONDs instead of TFONDs. We start by formalizing when a POND and a finite NMFOND produce the same observable behavior. A POND PO = ⟨O,U,A,S,S0, tr⟩ with observable fluents O and an NMFOND D = ⟨O,A, 2O , o0, tro⟩ with fluents O are O-indistinguishable iff (i) for every sequence of observations and actions: o0, a1, o1, . . . , ak, ok in D with ((o0, o1, . . . , oi-1), ai, oi) ∈ tro for i = 1, . . . , k, there exists a sequence of states and actions s0, a1, . . . , ak, sk in PO such that s0 ∈ S0, and (si-1, ai, si) ∈ tr for i = 1, . . . , k, and si∣O = oi for i = 0, . . . , k; (ii) for every s0, a1, s1, . . . , ak, sk in PO with s0 ∈ S0 and (si-1, ai, si) ∈ tr for i = 0, . . . , k, let si∣O = oi, then o0, a1, o1, . . . , ak, ok is such that o0 is the initial state of D and ((o0, o1, . . . , oi-1), ai, oi) ∈ tro for i = 1, . . . , k. Next we show that for every POND, there exists a finite NMFOND over its observables that is O-indistinguishable.

Theorem 5. For every POND PO = ⟨O, U, A, S, S0, tr⟩ there exists a finite NMFOND Dt = ⟨O,A, 2O , o0, trt⟩ such that PO and Dt are O-indistinguishable.

Proof. Given PO we start with the belief set construction, defining a standard FOND Dpo = ⟨O × 2U ,A,Spo, b0, trpo⟩. From Dpo we define the finite NMFOND Dt = ⟨O, A, 2O , o0, trt⟩, where O are the observable fluents and A the original set of actions; Spo = 2O is the set of states and o0 the initial observation; trt is generated by a finite state transition transducer Tr = ⟨Q, q0, δ, ϱ⟩ where: 1. Q = {q0} ∪ Spo is the set of the transducer states; 2. q0 is the initial state of the transducer; 3. δ ∶ Q × S → Q is the deterministic transition function of the transducer, defined as follows: (i) δ(qo, o0) = (o0,u0); (ii) δ((o,u), o′ ) = (o′ ,u′ ) where ((o, u), a, (o′ , u′ )) ∈ trpo with o′ ⊧ a; 4. ϱ ∶ Q×A× S is the output function of the transducer, defined as follows: (i) (qo, a0, o0) ∈ ϱ where a0 is the (dummy) action in o0; (ii) ((o, u), a, o′ ) ∈ ϱ where again ((o, u), a, (o′ , u′ )) ∈ trpo with o′ ⊧ a. It is easy to see that Dt = ⟨O,A, 2O , o0, trt⟩ and Dpo = ⟨O × 2U , A, Spo, b0, trpo⟩ are indeed O-indistinguishable.

Also the reverse result holds.

Theorem 6. For every finite NMFOND D with fluents O there exists a POND PO with observables O such that D and PO are O-indistinguishable.

Proof. Take the finite NMFOND, and using the construction in the previous section, transform it into a FOND. Let O be the set of fluents that define the state of the finite NMFOND. Let U be fluents that correspond to (a boolean encoding of) the state of the finite transducer. We can easily re-express transitions of the FOND in terms of such fluents. Considering U as unobservable fluents we get the desired POND.

Considering the relationship between finite NMFOND and TFONDs, we finally get:

Theorem 7. For every POND PO there exists a LDLf TFOND DL such that PO and DL are O-indistinguishable. Moreover, for every LDLf /LTLf TFOND DL there exists a POND PO such that DL and PO are O-indistinguishable.

Hence, LDLf TFONDs (but not LTLf TFOND, in general) provide an alternative to POND with one major benefit - in TFONDs there is no mention of, nor no need to know, nor hypothesize, a set U of unobservables.

Finally we observe that the construction that reduces POND to a finite NMFOND generates a transducer T rt, which can be minimized by reducing its number of states, without changing the traces generated by the NMFOND, and hence the observable traces of the original POND. If we transform back the resulting finite NMFOND into a POND with new unobservable fluents which are a factorization of the minimized states of Trt, we get a POND that is equivalent to the original one but with a minimal number of unobservable fluents. The practical ramification of such an observation deserves further study.

8 Conclusion

In many natural cases, the dynamics of the domain of interest is non-Markovian. In this paper we introduced and studied NMFONDs and, in particular, TFONDs, which provide a succinct and elegant formalism for specifying non-Markovian dynamics and rewards. We showed that this model can be solved using one's favorite FOND algorithm after an initial automated preprocessing phase. With these tools, we believe handling non-Markovian models becomes quite realistic and undaunting.

Acknowledgements

This work is partially supported by the Israel Ministry of Science and Technology grant 877017, the Lynn and William Frankel Center for Computer Science, and Sapienza project "Immersive Cognitive Environments".