Temporally extended goals are critical to the specification of a diversity of real-world planning problems. Here we examine the problem of planning with temporally extended goals over both finite and infinite traces where actions can be nondeterministic, and where temporally extended goals are specified in linear temporal logic (LTL). Unlike existing LTL planners, we place no restrictions on our LTL formulae beyond those necessary to distinguish finite from infinite trace interpretations. We realize our planner by compiling temporally extended goals, represented in LTL, into Planning Domain Definition Language problem instances, and exploiting a state-of-the-art fully observable nondeterministic planner to compute solutions. The resulting planner is sound and complete. Our approach exploits the correspondence between LTL and automata. We propose several different compilations based on translations of LTL to (Bu¨chi) alternating or non-deterministic finite state automata, and evaluate various properties of the competing approaches. We address a diverse spectrum of LTL planning problems that, to this point, had not been solvable using AI planning techniques. We do so while demonstrating competitive performance relative to the state of the art in LTL planning.
Most real-world planning problems involve complex goals that are temporally extended, require adherence to safety constraints and directives, necessitate the optimization of preferences or other quality measures, and/or require or may benefit from following a prescribed high-level script that specifies how the task is to be realized. In this paper we focus on the problem of planning for temporally extended goals, constraints, directives or scripts that are expressed in Linear Temporal Logic (LTL) for planning domains in which actions can have non-deterministic effects, and where LTL is interpreted over either finite or infinite traces.
Planning with deterministic actions and LTL goals has been
well studied, commencing with the works of Bacchus and
Kabanza [2000] and Doherty and Kvarnstro¨m [2001].
Significant attention has been given to compilation-based
approaches
In this paper, we propose a number of compilation-based approaches for LTL planning with non-deterministic actions. Specifically, we present two approaches for LTL planning with non-deterministic actions over infinite traces and two approaches for LTL planning with non-deterministic actions over finite traces1. In each case, we exploit translations from LTL to (Bu¨chi) alternating or non-deterministic finite state automata. All of our compilations are sound and complete and result in Planning Domain Definition Language (PDDL) encodings suitable for input to standard fully observable nondeterministic (FOND) planners. Our compilations based on alternating automata are linear in time and space with respect to the size of the LTL formula, while those based on nondeterministic finite state automata are worst-case exponential in time and space (although optimizations in the implementation avoid this in our experimental analysis).
Our approaches build on methods for finite LTL planning 1Subtleties relating to the interpretation of LTL over finite traces are discussed in [De Giacomo and Vardi, 2013]. with deterministic actions by Baier and McIlraith [2006] and Torres and Baier [2015], and for the infinite non-deterministic case, on the work of Patrizi, Lipovetzky, and Geffner [2013]. While in the finite case the adaptation of these methods was reasonably straightforward, the infinite case required non-trivial insights and modifications to Torres and Baier’s approach. We evaluate the relative performance of our compilation-based approaches using state-of-the-art FOND planner PRP [Muise, McIlraith, and Beck, 2012], demonstrating that they are competitive with state-of-the-art LTL planning techniques.
Our work presents the first realization of a
compilationbased approach to planning with non-deterministic actions
where the LTL is interpreted over finite traces. Furthermore,
unlike previous approaches to LTL planning, our
compilations make it possible, for the first time, to solve the
complete spectrum of FOND planning with LTL goals interpreted
over infinite traces. Indeed, all of our translations capture the
full expressivity of the LTL language. Table 1 summarizes
existing compilation-based approaches and the contributions
of this work. Our compilations enable a diversity of
realworld planning problems as well as supporting a number of
applications outside planning proper ranging from business
process analysis, and web service composition to narrative
generation, automated diagnosis, and automated verification.
Finally and importantly, our compilations can be seen as a
practical step towards the efficient realization of a class of
LTL synthesis tasks using planning technology
Following Ghallab, Nau, and Traverso [2004], a Fully Observable Non-Deterministic (FOND) planning problem consists of a tuple hF , I, G, Ai, where F is a set of propositions that we call fluents, I ✓ F characterizes what holds in the initial state; G ✓ F characterizes what must hold for the goal to be achieved. Finally A is the set of actions. The set of literals of F is Lits (F ) = F [ {¬ f | f 2 F } . Each action a 2 A is associated with hP rea, E↵ ai, where P rea ✓ Lits (F ) is the precondition and E↵ a is a set of outcomes of a. Each outcome e 2 E↵ a is a set of conditional effects, each of the form (C ! `), where C ✓ Lits (F ) and ` 2 Lits (F ). Given a planning state s ✓ F and a fluent f 2 F , we say that s satisfies f , denoted s |= f iff f 2 s. In addition s |= ¬f if f 62 s, and s |= L for a set of literals L, if s |= ` for every ` 2 L. Action a is applicable in state s if s |= P rea. We say s0 is a result of applying a in s iff, for one outcome e in E↵ a, s0 is equal to s \ {p | (C ! ¬ p) 2 e, s |= C} [ { p | (C ! p) 2 e, s |= C}. The determinization of a FOND problem hF , I, G, Ai is the planning problem hF , I, G, A0i, where each non-deterministic action a 2 A is replaced by a set of deterministic actions, ai, one action corresponding to each of the distinct non-deterministic effects of a. Together these deterministic actions comprise the set A0.
Solutions to a FOND planning problem P are policies. A policy p is a partial function from states to actions such that if p(s) = a, then a is applicable in s. The execution of a policy p in state s is an infinite sequence s0, a0, s1, a1, . . . or a finite sequence s0, a0, . . . , sn 1, an 1, sn, where s0 = s, and all of its state-action-state substrings s, a, s0 are such that p(s) = a and s0 is a result of applying a in s. Finite executions ending in a state s are such that p(s) is undefined. An execution yields the state trace ⇡ that results from removing all the action symbols from .
Alternatively, solutions to P can be represented by means
of finite-state controllers (FSCs). Formally, a FSC is a
tuple ⇧ = hC, c0, , ⇤ , ⇢, ⌦ i, where C is the set of controller
states, c0 2 C is the initial controller state, = S is the
input alphabet of ⇧ , ⇤ = A is the output alphabet of ⇧ ,
⇢ : C ⇥ ! C is the transition function, and ⌦ : C ! ⇤ is
the controller output function
Following Geffner and Bonet [2013], an infinite execution is fair iff whenever s, a occurs infinitely often within , then so does s, a, s0, for every s0 that is a result of applying a in s. A solution is a strong cyclic plan for hF , I, G, Ai iff each of its executions in I is either finite and ends in a state that satisfies G or is (infinite and) unfair. 2.2
Linear Temporal Logic (LTL) was first proposed for verification [Pnueli, 1977]. An LTL formula is interpreted over an infinite sequence, or trace, of states. Because the execution of a sequence of actions induces a trace of planning states, LTL can be naturally used to specify temporally extended planning goals when the execution of the plan naturally yields an infinite state trace, as may be the case in non-deterministic planning.
In classical planning –i.e. planning with deterministic
actions and final-state goals–, plans are finite sequences of
actions which yield finite execution traces. As such, approaches
to planning with deterministic actions and LTL goals
LTL and LTLf allow the use of modal operators next (⌦), and until ( U ), from which it is possible to define the wellknown operators always ( ) and eventually ( ). LTLf , in Deterministic Actions [Albarghouthi et al., 2009] (EXP) [Patrizi et al., 2011] (EXP)
Infinite LTL
Non-Deterministic Actions [Patrizi et al., 2013] (limited LTL) (2EXP) [this paper (BAA)] (LIN) [this paper (NBA)] (EXP)
Finite LTL Deterministic Actions Non-Deterministic Actions [Edelkamp, 2006] (EXP) [this paper (NFA)] (EXP) [Cresswell & Coddington, 2006] (EXP) [this paper (AA)] (LIN) [Baier & McIlraith, 2006] (EXP) [Torres & Baier, 2015] (LIN) addition, allows a weak next (✏) operator. An LTLf formula over a set of propositions P is defined inductively: a proposition in P is a formula, and if and are formulae, then so are ¬ , ( ^ ), ( U ), ⌦ , and ✏ . LTL is defined analogously.
The semantics of LTL and LTLf is defined as follows. Formally, a state trace ⇡ is a sequence of states, where each state is an element in 2P . We assume that the first state in ⇡ is s1, that the i-th state of ⇡ is si and that |⇡ | is the length of ⇡ (which is 1 if ⇡ is infinite). We say that ⇡ satisfies ' (⇡ |= ', for short) iff ⇡, 1 |= ', where for every natural number i 1: • ⇡, i |= p, for a propositional variable p 2 P , iff p 2 si, • ⇡, i |= ¬ • ⇡, i |= ( ^ iff it is not the case that ⇡, i |= , ) iff ⇡, i |= and ⇡, i |= , • ⇡, i |= ⌦' iff i < |⇡ | and ⇡, i + 1 |= ', ( R ) d=ef ¬(¬
U ¬ ). • ⇡, i |= ('1 U '2) iff for some j in {i, . . . , |⇡ |}, it holds that ⇡, j |= '2 and for all k 2 { i, . . . , j 1}, ⇡, k |= '1, • ⇡, i |= ✏' iff i = |⇡ | or ⇡, i + 1 |= '.
Observe operator ✏ is equivalent to ⌦ iff ⇡ is infinite. Therefore, henceforth we allow ✏ in LTL formulae, we do not use the acronym LTLf , but we are explicit regarding which interpretation we use (either finite or infinite) when not obvious from the context. As usual, ' is defined as (true U '), and ' as ¬ ¬'. We use the release operator, defined by 2.3
Regardless of whether the interpretation is over an infinite or finite trace, given an LTL formula ' there exists an automata A' that accepts a trace ⇡ iff ⇡ |= '. For infinite interpretations of ', a trace ⇡ is accepting when the run of (a Bu¨chi non-deterministic automata) A' on ⇡ visits accepting states infinitely often. For finite interpretations, ⇡ is accepting when the final automata state is accepting. For the infinite case such automata may be either Bu¨chi non-deterministic or Bu¨chi alternating [Vardi and Wolper, 1994], whereas for the finite case such automata may be either non deterministic [Baier and McIlraith, 2006] or alternating [De Giacomo, Masellis, and Montali, 2014; Torres and Baier, 2015]. Alternation allows the generation of compact automata; specifically, A' is linear in the size of ' (both in the infinite and finite case), whereas the size of nondeterministic (Bu¨chi) automata is worst-case exponential.
These automata constructions have been exploited in deterministic and non-deterministic planning with LTL via compilation approaches that allow us to use existing planning technology for non-temporal goals. The different state of the art automata-based approaches for deterministic and FOND LTL planning are summarized in Table 1. Patrizi, Lipovetzky, and Geffner [2013] present a Bu¨chi automata-based compilation for that subset of LTL which relies on the construction of a Bu¨chi deterministic automata. It is a well-known fact that Bu¨chi deterministic automata are not equivalent to Bu¨chi non-deterministic automata, and thus this last approach is applicable to a limited subset of LTL formulae. 3
An LTL-FOND planning problem is a tuple hF , I, ', Ai, where F , I, and A are defined as in FOND problems, and ' is an LTL formula. Solutions to an LTL-FOND problem are FSCs, as described below.
Definition 1 (Finite LTL-FOND). An FSC ⇧ is a solution for hF , I, ', Ai under the finite semantics iff every execution of ⇧ over I is such that either (1) it is finite and yields a state trace ⇡ such that ⇡ |= ' or (2) it is (infinite and) unfair. Definition 2 (Infinite LTL-FOND). An FSC ⇧ is a solution for hF , I, ', Ai under the infinite semantics iff (1) every execution of ⇧ over I is infinite and (2) every fair (infinite) execution yields a state trace ⇡ such that ⇡ |= '.
Below we present two general approaches to solving LTLFOND planning problems by compiling them into standard FOND problems. Each exploits correspondences between LTL and either alternating or non-deterministic automata, and each is specialized, as necessary, to deal with LTL interpreted over either infinite (Section 3.1) or finite (Section 3.2) traces. We show that FSC representations of strong-cyclic solutions to the resultant FOND problem are solutions to the original LTL-FOND problem. Our approaches are the first to address the full spectrum of FOND planning with LTL interpreted over finite and inifinte traces. In particular our work is the first to solve full LTL-FOND with respect to infinite trace interpretations, and represents the first realization of a compilation approach for LTL-FOND with respect to finite trace interpretations.
We present two different approaches to infinite LTL-FOND planning. The first approach exploits Bu¨chi alternating automata (BAA) and is linear in time and space with respect to the size of the LTL formula. The second approach exploits Bu¨chi non-deterministic automata (NBA), and is worst-case exponential in time and space with respect to the size of the LTL formula. Nevertheless, as we see in Section 4, the second compilation does not exhibit this worst-case complexity in practice, generating high quality solutions with reduced compilation run times and competitive search performance.
Our BAA-based compilation builds on ideas by Torres and Baier [2015] for alternating automata (AA) based compilation of finite LTL planning with deterministic actions (henceforth, TB15), and from Patrizi, Lipovetzky, and Geffner’s compilation [2013] (henceforth, PLG13) of LTL-FOND to FOND. Combining these two approaches is not straightforward. Among other reasons, TB15 does not yield a sound translation for the infinite case, and thus we needed to modify it significantly. This is because the accepting condition for BAAs is more involved than that of regular AAs.
The first step in the compilation is to build a BAA for our LTL goal formula ' over propositions F , which we henceforth assume to be in negation normal form (NNF). Transforming an LTL formula ' to NNF can be done in linear time in the size of '. The BAA we use below is an adaptation of the BAA by Vardi [1995]. Formally, it is represented by a tuple A' = (Q, ⌃ , , q ' , QF in), where the set of states, Q, is the set of subformulae of ', sub(') (including '), ⌃ contains all sets of propositions in P, QF in = {↵ R 2 sub(')}, and the transition function, is given by: (`, s) = ⇢> if s |= ` (`, literal)
? otherwise (↵ ^ , s ) = (↵, s ) ^ (, s )
(⌦↵, s ) = ↵ (↵ _ , s ) = (↵, s ) _ (, s ) (↵ U , s ) = (, s ) _ ( (↵, s ) ^ ↵ U ) (↵ R , s ) = (, s ) ^ ( (↵, s ) _ ↵ R ) As a note for the reader unfamiliar with BAAs, the transition function for these automata takes a state and a symbol and returns a positive Boolean formula over the set of states Q. Furthermore, a run of a BAA over an infinite string ⇡ = s1s2 . . . is characterized by a tree with labeled nodes, in which (informally): (1) the root node is labeled with the initial state, (2) level i corresponds to the processing of symbol si, and (3) the children of a node labeled by q at level i are the states appearing in a minimal model of (q, si). As such, multiple runs for a certain infinite string are produced when selecting different models of (q, si). A special case is when (q, si) reduces to > or ? , where there is one child labeled by > or ? , respectively. A run of a BAA is accepting iff all of its finite branches end on > and in each of its infinite branches there is an accepting state that repeats infinitely often. Figure 1 shows a run of the BAA for p ^ ¬p—a formula whose semantics forces an infinite alternation, which is not necessarily immediate, between states that satisfy p and states that do not satisfy p.
In our BAA translation for LTL-FOND we follow a similar approach to that developed in the TB15 translation: given an input problem P, we generate an equivalent problem P0 in which we represent the configuration of the BAA with fluents (one fluent q per each state q of the BAA). P0 contains the actions in P plus additional synchronization actions whose objective is to update the configuration of the BAA. In P0, there are special fluents to alternate between so-called world mode, in which only one action of P is allowed, and synp p p
p > . . . . . .
p > {{q¬↵SSq,`Sq,Sq,`T¬!q↵ S,^q¬↵Tq_,`q↵}T^ ! {q↵T , qT , ¬q↵T^ }}
T {{qq↵S,, ¬¬qqS↵↵SS__ , qT↵T_ !! {{Tqq↵TT ,, ¬¬Tqq↵↵TT__ }}}} {q↵S, ¬q⌦↵ , q⌦↵ ! {q↵ , ¬q⌦↵ }} {{qq↵SS,, q¬↵ qU↵S U, ¬, qq↵↵TS UU , !q↵T U{qT !,¬qq↵↵TT }U }} q , q↵S, ¬q↵S R , q↵T R T {{{qq↵SS,, q¬↵ qRS ↵ ,, ¬qTq↵S↵ R!, {q↵Tq↵TR!,¬!¬qTq↵¬↵}Rq}↵T }R }
S {{qq↵S ,↵ q, ¬↵ q, ¬↵ q}S↵ , qT↵ ! ¬qT↵ } is {sync, qS }, plus ` when chronization mode, in which the configuration of the BAA is updated.
Before providing details of the translation we overview the main differences between our translation and that of TB15. TB15 recognizes an accepting run (i.e., a satisfied goal) by observing that all automaton states at the last level of the (finite) run are accepting states. In the infinite case, such a check does not work. As can be seen in the example of Figure 1, there is no single level of the (infinite) run that only contains final BAA states. Thus, when building a plan with our translation, the planner is given the ability to “decide” at any moment that an accepting run can be found and then the objective is to “prove” this is the case by showing the existence of a loop or lasso in the plan in which any non-accepting state may turn into an accepting state. To keep track of those non-accepting states that we require to eventually “turn into” accepting states we use special fluents that we call tokens.
For an LTL-FOND problem P = hF , I, ', Ai, where ' is an NNF LTL formula with BAA A' = (Q, ⌃ , , q ' , QF in), the translated FOND problem is P0 = hF 0, I0, G0, A0i, where each component is described below.
Fluents P0 has the same fluents as P plus fluents for the representation of the states of the automaton FQ = {q | 2 Q}, and flags copy, sync, world for controlling the different modes. Finally, it includes the set FQS = {qS | 2 Q} which are copies of the automata fluents, and tokens FQT = {qT | 2 Q}. We describe both sets below. Formally, F 0 = F [ FQ [ FQS [ FQT [ { copy, sync, world, goal}.
The set of actions A0 is the union of the sets Aw and As plus the continue action.
World Mode Aw contains the actions in A with preconditions modified to allow execution only in world mode. Effects are modified to allow the execution of the copy action, which initiates the synchronization phase, described below. Formally, Aw = {a0 | a 2 A} , and for all a0 in Aw: P rea0 = P rea [ { world},
E↵ a0 = E↵ a [ { copy, ¬world}.
Synchronization Mode This mode has three phases. In the first phase, the copy action is executed, adding a copy qS for each fluent q that is currently true, deleting q. Intuitively, qS defines the state of the automaton prior to synchronization. The precondition of copy is {copy}, while its effect is: E↵ copy = {q ! { qS , ¬q} | q 2 FQ} [ { sync, ¬copy} As soon as the sync fluent becomes true, the second phase of synchronization begins. Here the only executable actions are those that update the state of the automaton, which are defined in Table 2. These actions update the state of the automaton following the definition of the transition function, . In addition, each synchronization action for a formula that has an associated token qT , propagates such a token to its subformulae, unless corresponds to either an accepting state (i.e., is of the form ↵ R ) or to a literal ` whose truth can be verified with respect to the current state via action tr(q`S ).
When no more synchronization actions are possible, we enter the third phase of synchronization. Here only two actions are executable: world and continue. The objective of world action is to reestablish world mode. Its precondition is {sync} [ FQS , and its effect is {world, ¬sync}.
The continue action also reestablishes world mode, but in addition “decides” that an accepting BAA can be reached in the future. This is reflected by the non-deterministic effect that makes the fluent goal true. As such, it “tokenizes” all states that are not final states in FQ, by adding qT for each BAA state q that is non-final and currently true. Formally, P recontinue = {sync} [ {¬ q'T | ' 62 QF in} E↵ continue = {{goal},
{q' ! q'T | ' 62 QF in} [ { world, ¬sync}}
The set As is defined as the one containing actions copy, world, and all actions defined in Table 2.
Initial and Goal States The resulting problem P0 has initial state I0 = I [ { q' , copy} , and goal G0 = {goal}.
In summary, our BAA-based approach builds on TB15 while integrating ideas from PLG13. Like PLG13 our approach uses a continue action to find plans with lassos, but unlike PLG13, our translation does not directly use the accepting configuration of the automaton. Rather, the planner “guesses” that such a configuration can be reached. The token fluents FQT , which did not exist in TB15, are created for each non-accepting state and can only be eliminated when a non-accepting BAA state becomes accepting.
Now we show how, given a strong cyclic policy for P0, we can generate an FSC for P. Observe that every state ⇠ , which is a set of fluents in F 0, can be written as the disjoint union of sets sw = ⇠ \ F and sq = ⇠ \ (F 0 \ F ). Abusing notation, we use sw 2 2F to represent a state in P. For a planning state ⇠ = sw [ sq green in which p(⇠ ) is defined, we define ⌦( ⇠ ) to be the action in A whose translation is p(⇠ ). Recall now that executions of a strong-cyclic policy p for P0 in state ⇠ generate plans of the form a1↵ 1a2↵ 2 . . . where each ai is a world action in Aw and ↵ i are sequences of actions in A0 \ Aw. Thus ⌦( ⇠ ) can be generated by taking out the fluents world and copy from the precondition and effects of p(⇠ ). If state s0w is a result of applying ⌦( ⇠ ) in sw, we define ⇢ (⇠, s 0w) to be the state ⇠ 0 that results from the composition of consecutive non-world actions ↵ 1 mandated by an execution of p in s0w [ sq. Despite non-determinism in the executions, the state ⇠ 0 = ⇢ (⇠, s 0w) is well-defined.
The BAA translation for LTL-FOND is sound and complete. Throughout the paper, the soundness property guarantees that FSCs obtained from solutions to the compiled problem P0 are solutions to the LTL-FOND problem P, whereas the completeness property guarantees that a solution to P0 exists if one exists for P.
Theorem 1. The BAA translation for Infinite LTL-FOND planning is sound, complete, and linear in the size of the goal formula.
A complete proof is not included but we present some of the intuitions our proof builds on. Consider a policy p0 for P0. p0 yields three types of executions: (1) finite executions that end in a state where goal is true, (2) infinite executions in which the continue action is executed infinitely often and (3) infinite, unfair executions. We do not need to consider (3) because of Definition 2. Because the precondition of continue does not admit token fluents, if continue executes infinitely often we can guarantee that any state that was not a BAA accepting state turns into an accepting state. This in turn means that every branch of the run contains an infinite repetition of final states. The plan for P, p, is obtained by removing all synchronization actions from p0, and the FSC that is solution to P is obtained as described above. In the other direction, a plan p0 for P0 can be built from a plan p for P by adding synchronization actions. Theorem 1 follows from the argument given above and reuses most of the argument that TB15 uses to show their translation is correct.
This compilation relies on the construction of a nondeterminisitic Bu¨chi automaton (NBA) for the goal formula, and builds on translation techniques for finite LTL planning with deterministic actions developed by Baier and McIlraith [2006] (henceforth, BM06). Given a deterministic planning problem P with LTL goal ', the BM06 translation runs in two phases: first, ' is transformed into a non-deterministic finite-state automata (NFA), A' , such that it accepts a finite sequence of states if and only if |= '. In the second phase, it builds an output problem P0 that contains the same fluents as in P plus additional fluents of the form Fq, for each state q of A' . Problem P0 contains the same actions as in P but each action may contain additional effects which model the dynamics of the Fq fluents. The goal of P 0 is defined as the disjunction of all fluents of the form Ff , where f is an accepting state of A' . The initial state of P 0 contains Fq iff q is a state that A' would reach after processing the initial state of P . The most important property of BM06 is the following: let = s0s1 . . . sn+1 be a state trace induced by some sequence of actions a0a1 . . . an in P 0, then Fq is satisfied by sn+1 iff there exists a run of A' over that ends in q. This means that a single sequence of planning states encodes all runs of the NFA A' . The important consequence of this property is that the angelic semantics of A' is immediately reflected in the planning states and does not need to be handled by the planner (unlike TB15).
For LTL-FOND problem P = hF , I, ', Ai, our NBAbased compilation constructs a FOND problem P 0 = hF 0, I0, G0, A0i via the following three phases: (i) construct an NBA, A' for the NNF LTL goal formula ', (ii) apply the modified BM06 translation to the determinization of P (see Section 2.1) , and (iii) construct the final FOND problem P 0 by undoing the determinization, i.e., reconstruct the original non-deterministic actions from their determinized counterparts. More precisely, the translation of a non-deterministic action a in P is a non-deterministic action a0 in P 0 that is constructed by first determinizing a into a set of actions, ai that correspond to each of the non-deterministic outcomes of a, applying the BM06-based translation to each ai to produce a0 , and then reassembling the a0 s back into a noni i deterministic action, a0. In so doing, E↵ a0 is the set of outcomes in each of the deterministic actions a0i, and P rea0 is similarly the precondition of any of these a0 . i
The modification of the BM06 translation used in the second phase leverages ideas present in PLG13 and our BAAbased compilations to capture infinite runs via induced nondeterminism. In particular, it includes a continue action whose precondition is the accepting configuration of the NBA (a disjunction of the fluents representing accepting states). Unlike our BAA-based compilation, the tokenization is not required because accepting runs are those that achieve accepting states infinitely often, no matter which ones. As before, one non-deterministic effect of continue is to achieve goal, while the other is to force the planner to perform at least one action. This is ensured by adding an extra precondition to continue , can continue, which is true in the initial state, it is made true by every action but continue , and is deleted by continue .
In order to construct a solution ⇧ to P from a strong-cyclic solution p to P 0 = hF 0, I0, G0, A0i, it is useful to represent states ⇠ in P 0 as the disjoint union of s = ⇠ \ F and q = ⇠ \ (F 0 \ F ). Intuitively, s represents the planning state in P , and q represents the automaton state. The controller ⇧ = hC, c0, , ⇤ , ⇢, ⌦ i is defined as follows. c0 = I 0 is the initial controller state; = 2 F ; ⇤ = A; ⇢ (⇠, s 0) = s0 [ q0, where q0 is the automaton state that results from applying action p(⇠ ) in ⇠ ; ⌦( ⇠ ) = p(⇠ ); and C ✓ 2F0 is the domain of p. Actions in P 0 are non-deterministic and have conditional effects, but the automaton state q0 that results from applying action p(⇠ ) in state ⇠ = s [ q is deterministic, and thus ⇢ is well-defined. Theorem 2. The NBA translation for Infinite LTL-FOND planning is sound, complete, and worst-case exponential in the size of the LTL formula.
Theorem 2 follows from soundness, completeness, and the complexity of the BM06 translation, this time using a NBA automaton, and an argument similar to that of Theorem 1. This time, if continue executes infinitely often we can guarantee accepting NBA states are reached infinitely often. 3.2
Our approach to finite LTL-FOND extends the BM06 and TB15 translations, originally intended for finite LTL planning with deterministic actions, to the non-deterministic action setting. Both the original BM06 and TB15 translations share two general steps. In step one, the LTL goal formula is translated to an automaton/automata – in the case of BM06 an NFA, in the case of TB15, an AA. In step two, a planning problem P 0 is constructed by augmenting P with additional fluents and action effects to account for the integration of the automaton. In the case of BM06 these capture the state of the automaton and how domain actions cause the state of the automaton to be updated. In the case of the TB15 translation, P must also be augmented with synchronization actions. Finally, in both cases the original problem goals must be modified to capture the accepting states of automata.
When BM06 and TB15 are exploited for LTL-FOND, the non-deterministic nature of the actions must be taken into account. This is done in much the same as with the NBA- and BAA-based compilations described in the previous section. In particular, non-deterministic actions in the LTL-FOND problem are determinized, the BM06 (resp. TB15) translation is applied to these determinized actions, and then the non-deterministic actions reconstructed from their translated determinized counterparts (as done in the NBA-based compilation) to produce FOND problem, P 0. A FSC solution, ⇧ , to the LTL-FOND problem P , can be obtained from a solution to P 0. When the NFA-based translations are used, the FSC, ⇧ , is obtained from policy p following the approach described for NBA-based translations. When the AA-based translations are used, the FSC, ⇧ , is obtained from p following the approach described for BAA-based translations.
Theorem 3. The NFA (resp. AA) translation for Finite LTLFOND is sound, complete, and exponential (resp. linear) in the size of the LTL formula.
Soundness and completeness in Theorem 3 follows from soundness and completeness of the BM06 and TB15 translations. Fair executions of ⇧ yield finite plans for P 0, and therefore state traces (excluding intermediate synchronization states) satisfy '. Conversely, our approach is complete as for every plan in P , one can construct a plan in P 0. Finally, the run-time complexity and size of the translations is that of the original BM06 and TB15 translations – worst case exponential in time and space for the NFA-based approach and linear in time and space for the AA approach. 4
We evaluate our framework on a selection of benchmark domains with LTL goals from [Baier and McIlraith, 2006; (a) Translation run times.
(b) Number of new fluents. (a) Run-time in Waldo problems. (b) Run-time in Lift problems. (c) PRP run times.
(d) PRP Policy Size. (e) Preferred world Plan Length. Patrizi, Lipovetzky, and Geffner, 2013; Torres and Baier, 2015], modified to include non-deterministic actions. Experiments were conducted on an Intel Xeon E5-2430 CPU @2.2GHz Linux server, using a 4GB memory and a 30minute time limit.
LTL-FOND Planning over Finite Traces: We evaluated the performance of our BM06 (NFA) and TB15 (AA) translators, with respect to a collection of problems with deterministic and non-determinisitic actions and LTL goals, interpreted on finite traces. We used the state-of-the-art FOND planner, PRP [Muise, McIlraith, and Beck, 2012], to solve the translated problems. NFA-based translation times increased when the LTL formula had a large number of conjunctions and nested modal operators, whereas AA-based translation times remain negligible. However, the AA translation included a number of new fluents that were, in some cases, up to one order of magnitude larger than with the NFA (Figures 2a and 2b). This seems to translate into more complex problems, as PRP run times become almost consistently greater in problems translated with AA (Figure 2c). The size of the policies obtained from the AA compilations were considerably greater than those obtained with NFA compilations (Figure 3d). This is expected, as AA translations introduce a number of synchronization actions, whereas the number of actions in NFA translations remains unchanged. To assess the quality (c) Run-time in Clerk problems. (d) Policy Size (world actions). of the plans obtained from each translation, we compared the number of world actions (i.e., excluding automaton-state synchronization actions) in the shortest plans of the policies obtained (Figure 2e). This is a crude estimator of the quality of plans, since these plans are not necessarily the ones that minimize the number of world actions, as they also contain synchronization actions. The number of world actions that we obtained in both compilations was very similar.
Interestingly, whereas the size of the AA translations is linear in the size of the original LTL formula and NFA translations are worst-case exponential, in practice we observed the size of the NFA-based translated problems is smaller. Furthermore, PRP performs better when problems are compiled using NFAs, generating similar quality policies in lower search run-times.
We didn’t experience any untoward decrease in performance in deterministic problems that were extended with non-deterministic actions, suggesting that AA- and NFAbased translations remain competitive in LTL-FOND. LTL-FOND Planning over Infinite Traces: The relative performance observed between NBA- and BAA-based translations for LTL-FOND planning, interpreted over infinite traces, is reflective of the finite case. NBA translation run times are greater, but result in lower planner run times and smaller policy sizes. For reference, we compared BAA translations with the so-called sequential and parallel translations developed by Patrizi, Lipovetzky, and Geffner [2013], subsequently referrd to as PLG13seq and PLG13par, respectively. The former alternates between world and sync actions (that update the automaton state), whereas the latter parallelizes this process in a single action. The current implementation of PLG13 translations forced us to perform such comparisons only in the three domains that appear in [Patrizi, Lipovetzky, and Geffner, 2013]. Namely, the Waldo, Lift, and Clerk domains. All problems have LTL goals that can be compiled into deterministic Bu¨chi automata. Unfortunately, we could not include a fair comparison with NBA translations in the Lift and Clerk domains, due to a specific encoding that forced transitions to synchronization phases (existing in PLG13 and BAA translations, but not in NBA). In the Waldo problems, however, NBA translations generated smaller solutions (by a half) with roughly half the run time required by BAA. On the other hand, NBA translation times timed out after the 12th instance (possibly due to lack of optimization of the translator).
The Waldo problems require construction of a controller for a robot that moves around n rooms and finds Waldo infinitely often. Waldo may or may not appear in the nth and n/2-th rooms when these are visited. The dynamics of the problem preclude visiting a room twice before visiting the remaining ones, in which case the predicate search again becomes true. The LTL goal of the problem is search again _ Waldo. The Lift problems requires construction of a controller for an n-floor building that serves all requests. The dynamics of the problem require alternation between move and push fi actions, i = 1, . . . , n. Fluents ati and reqi model, respectively, whether the lift is at the ith floor, and whether a request from the i-th floor has been issued and not served. The lift can only move up if some request is issued. The push fi actions non-deterministically request the lift to service the i-th floor. Initially, the lift is at floor 1, and no request is issued. The LTL goal of the problem is ' = Vin=1 (reqi ! ati ). Finally, the Clerk problems require construction of a controller that serves all clients in a store. Clients can order one of n packages pi . If the package is not available, the clerk has to buy it from a supplier, pick it up, and store it in its correct location. In order to serve the client, the clerk has to find the package, pick it up, and sell it. The LTL goal of the problem is (active request ! (item served _ item stored )).
The results of experiments are summarized in Figure 3. In Waldo problems, the planner run times using BAAbased translations are situated between the run times with PLG13seq and PLG13par. In Lift problems, the BAA translations demonstrate significantly greater scalability. The Lift problems contain a (increasing) large number of conjunctive LTL goals. We conjecture that the poor scalability with PLG13seq (runs out of time) and PLG13par (runs out of memory) translations is due to the bad handling of conjunctive goals, that results in a exponentially large number of different state transitions. On the other hand, the PRP handles conjunctive goals much better in the BAA translations thanks to the AA progression of the LTL formula. In the Clerk problems, PRP scales slightly worse with the BAA translation than with the PLG13seq and PLG13par translations, which can solve 1 and 2 more problems respectively. The run times with all translations seem to show the same exponential trend, and differ in a small offset that corresponds to the increase in problem complexity.
Figure 3d compares the size of the policies found by PRP to problems compiled with BAA and PLG13par translations. PLG13seq translations resulted in slightly larger policies, due to separate world and sync action phases. We account only for world actions, excluding synchronization actions from the count. Policy sizes with BAA-based translations are similar, but consistently smaller than those from PLG13par translations, except in the Lift problems where the former results in considerably smaller policies. Finally, we evaluated the validity of our system with LTL goals that could not be handled by PLG13. In particular, we solved Waldo problems with goals of the form ↵ .
Overall, our system proves very competitive with (as good as or better than) the previous state-of-the-art LTL-FOND planning methods, while supporting a much broader spectrum (the full spectrum) of LTL formulae. 5
We have proposed four compilation-based approaches to fully observable non-deterministic planning with LTL goals that are interpreted over either finite or infinite traces. These compilations support the full expressivity of LTL, in contrast to much existing work. In doing so, we address a number of open problems in planning with LTL with non-deterministic actions, as noted in Table 1. Our LTL planning techniques are directly applicable to a number of real-world planning problems as well as capturing a diversity of applications beyond standard planning, including but not limited to genomic rearrangement [Uras and Erdem, 2010], program test generation [Razavi, Farzan, and McIlraith, 2014], story generation [Haslum, 2012], automated diagnosis [Grastien et al., 2007; Sohrabi, Baier, and McIlraith, 2010], business process management [De Giacomo et al., 2014], verification [Albarghouthi, Baier, and McIlraith, 2009; Patrizi et al., 2011], and robot motion planning [Plaku, 2012].
Our work has focused on the specification of temporally
extended goals as rich LTL path constraints, which is in
keeping with the planning community’s integration of a
subset of LTL into the Planning Domain Definition Language
(PDDL). Nevertheless, some goals are best described
procedurally, using regular expressions. The EAGLE goal
language [Lago, Pistore, and Traverso, 2002] and variants of
the Golog language
We evaluated the effectiveness of our FOND compilations using the state-of-the-art FOND planner, PRP. An interesting observation is that our worst-case exponential NFA-based translations run faster and return smaller policies than the AA-based linear translations. This seems to be due to the larger number of fluents (and actions) required in the AAbased translations. Compared to the existing approach of [Patrizi, Lipovetzky, and Geffner, 2013], experiments indicate that our approaches scale up better.
Finally, we observe that LTL-FOND is related to the problem of LTL synthesis [Pnueli and Rosner, 1989]. Informally, it is the problem of computing a policy that satisfies an LTL formula, assuming that an adversary (which we can associate to the non-deterministic environment) may change some fluents after the execution of each action. Recently De Giacomo and Vardi [2015] showed how to map a finite LTL-FOND problem into a synthesis problem. Sardin˜a and D’Ippolito [2015] go further, showing how FOND plans can be synthesized using LTL synthesis algorithms. An open question is whether any existing planning technology can be used for LTL synthesis as well. LTL synthesis is not an instance of strong cyclic FOND planning since synthesis adversaries are not fair.
Acknowledgements: We gratefully acknowledge funding from the Natural Sciences and Engineering Research Council of Canada and from Fondecyt grant number 1150328.