Fair LTL Synthesis for Non-Deterministic Systems using Strong Cyclic Planners

1 Introduction

Classical planning is concerned with reachability problems over compact propositional representations where a goal state is to be achieved from a given initial state by applying actions with deterministic effects. While the problem is computationally intractable [Bylander, 1994], significant progress has been achieved, enabling classical planners to solve problems with hundreds of actions and propositions [Richter and Westphal, 2010]. In the last few years temporally extended goals, expressed in temporal logics such as LTL [Pnueli, 1977] have been increasingly used to capture a richer class of plans, where restrictions over the whole sequence of states must be satisfied as well [Gerevini and Long, 2005]. A (temporally) extended goal may state, for example, that any borrowed tool should be kept clean until returning it; a constraint that does not apply to states but, rather, to state sequences. While most of this work has been focused on LTL goals that can be achieved by finite plans [Bacchus and Kabanza, 1998; Edelkamp, 2003; Cresswell and Coddington, 2004;

Hector Geffner

ICREA & Univ. Pompeu Fabra Barcelona, Spain hector.geffner@upf.edu

Edelkamp, 2006; Baier and McIlraith, 2006; Baier et al., 2009], more recent work has addressed the more general task of planning for LTL goals that require infinite plans [Kabanza and Thi´ebaux, 2005; Albarghouthi et al., 2009; Patrizi et al., 2011]. For instance, in order to monitor a set of rooms, an extended LTL goal may require the agent to always return to each of the rooms, a goal that cannot be achieved by a finite plan. It is known that the required plans in such a setting can be finitely characterized as "lassos": a sequence of actions mapping the initial state of a composite system into some state s, followed by a second action sequence that maps s into itself that is repeated infinitely often [Vardi, 1996]. In [Patrizi et al., 2011], it is shown that such plans can efficiently be constructed by calling a classical planner once, over a classical planning problem obtained from the composite system represented by the product of the planning domain and the B¨uchi automaton corresponding to the LTL goal [De Giacomo and Vardi, 1999].

The aim of this work is to push the envelope further by showing how to use current planning techniques for dealing with the more general problem of planning for LTL goals that require infinite executions, in environments where actions have non-deterministic effects and states are fully observable. From a planning point of view, this is the standard fully-observable non-deterministic planning problem (FOND) but with reachability goals replaced by temporally extended goals. From a formal verification point of view, this is the standard control synthesis problem for LTL formulas [Pnueli and Rosner, 1989]. Since the general synthesis problem is known to be 2EXPTIME-complete [Pnueli and Rosner, 1989], however, it is common to impose restrictions on the class of LTL formulas for scaling up. A common restriction is to focus on Generalized Reactive or GR(1) formulas for which a synthesis algorithm has been developed that is O(|S|3 ), where S is the problem state space [Bloem et al., 2012]. Other approaches are based on restricting to LTL formulas that can be mapped efficiently into deterministic automata [Alur and La Torre, 2004; Morgenstern and Schneider, 2008; 2011].

In this work we adopt the latter assumption by considering LTL formulas that can be mapped into deterministic B¨uchi automata, and show that by assuming further that action non-determinism is fair, namely that infinite executions of a non-deterministic action in the same state yield each possible successor state an infinite number of times, the (fair) synthesis problem can be reduced to a standard strong cyclic planning task over a domain that is the product of the (non-deterministic) planning domain and the (deterministic) B¨uchi automaton. A strong cyclic plan over a non-deterministic planning domain is a policy π such that if s is a non-goal state that is potentially reachable from the initial state by following π, then a goal state must be potentially reachable from s by following π [Daniele et al., 1999; Cimatti et al., 2003]. Since strong cyclic planners are built on top of efficient classical planners [Kuter et al., 2008; Fu et al., 2011; Muise et al., 2012] the transformation reduces the non-deterministic, fully observable, extended planning task into the solution of classical planning tasks. Finally, we report on a number of experiments showing the potential benefits of this planning approach to synthesis in comparison with state-of-the-art symbolic synthesis methods.

The paper is organized as follows. First, we review nondeterministic planning domains, LTL, and B¨uchi automata. Then we consider the target problem and the reduction to strong cyclic planning, present the empirical results, and finish with a summary and discussion.

2 Preliminaries

We review the models and results associated with nondeterministic planning, LTL, and B¨uchi automata.

2.1 Nondeterministic Planning Domains

A (nondeterministic) planning domain is a tuple D = 〈Act, P rop, S, S0, f 〉 where:

• Act is the finite set of domain actions;
• Prop is the set of domain propositions;
• S ⊆ 2Prop is the set of domain states;
• s0 ∈ S is the (single) initial state; and
• f : S ×Act ↦→ 2S is the state-transition function.

A D-path is a possibly infinite sequence µ = s0 a0 -→ s1 a1 -→ · · · such that si+1 ∈ f(si, ai). Astate s ∈ S is reachable if there exists a D-path where s occurs. Moreover, we say that a path µ reaches a state s, if s occurs in µ. In the rest of the paper we assume, without loss of generality, that every reachable state admits an executable action a, i.e., f(s, a) ̸= ∅. Consequently, every finite path can be extended into an infinite path. This allows us to consider the case of domains with infinite runs only. Obviously, when the assumption is not fulfilled, an additional action, say nop can be introduced.

A D-path µ is said to be fair if for every state s and action a such that s a-→ occurs infinitely many times in µ, it is the case that for every s′ ∈ f(s, a), s a-→ s′ occurs infinitely many times in µ. A D-trace is a possibly infinite sequence τ = s0s1 . . . such that there exists some D-path µ = s0 a0 -→ s1 a1 -→ · · · . A D-trace τ is said to be fair if there exists a D-path µ′ = s0 a′0 -→ s1 a′1 -→ · · · that is so.

As it turns out, fairness captures the intuition that whenever an action is executed infinitely often, all of its effects take place infinitely often. This accounts for a form of nondeterminism that is typical when modeling natural events, as opposed to adversarial ones.

Planning languages such as STRIPS or ADL, all accommodated in the PDDL standard, are commonly used to specify the states and transitions in compact form. A goal in this language is a specification of the desired traces on D. In particular, classical reachability goals, which require reaching a state s where a certain propositional formula ϕ over Prop holds, are expressed as selecting all those finite traces t = s0s1 · · · sn, such that sn |= ϕ. Using infinite traces allows us to consider a richer set of goals, suitably expressed through LTL formulas.

2.2 Linear Temporal Logic (LTL)

LTL was originally proposed as a specification language for concurrent programs [Pnueli, 1977]. Formulas of LTL are built from a set Prop of propositional symbols and are closed under the boolean operators, the unary temporal operators ©, ✸, and ✷, and the binary temporal operator U. 1 Intuitively, ©ϕ says that ϕ holds at the next instant, ✸ϕ says that ϕ will eventually hold at some future instant, ✷ϕ says that from the current instant on, ϕ will always hold, and ϕU ψ says that at some future instant ψ will hold and until that point ϕ holds. We also use the standard boolean connectives ∨, ∧, and →.

The semantics of LTL is given in terms of interpretations over a linear structure. For simplicity, we use IN as the linear structure: for an instant i ∈ IN, the successive instant is i+1. An interpretation is a function ι : IN → 2Prop assigning to each element of Prop a truth value at each instant i ∈ IN. For an interpretation ι, we inductively define when an LTL formula ϕ is true at an instant i ∈ IN (written ι, i |= ϕ):

• ι, i |= p, for p ∈ Prop iff p ∈ ι(i).
• ι, i |= ¬ϕ iff not ι, i |= ϕ.
• ι, i |= ϕ∧ϕ′ iff ι, i |= ϕ and ι, i |= ϕ′ .
• ι, i |=©ϕ iff ι, i+1 |= ϕ.
• ι, i |= ϕU ϕ′ iff for some j ≥ i, we have that ι, j |= ϕ′ and for all k, i ≤ k < j, we have that ι, k |= ϕ.

A formula ϕ is true in ι (written ι |= ϕ) if ι, 0 |= ϕ. Given a planning domain, every trace τ = s0s1s2 . . . can be seen as an LTL interpretation ι such that ι, i |= p iff si |= p.

2.3 LTL and B¨uchi Automata

There is a tight relation between LTL and B¨uchi automata on infinite words [Vardi, 1996]. A B¨uchi automaton [Thomas, 1990] is a tuple A = 〈Σ, Q, Q0, ρ, F 〉, where:

• Σ is the finite input alphabet of the automaton;
• Q is the finite set of automaton states;
• Q0 ⊆ Q is the set of initial states of the automaton;
• ρ : Q×Σ→ 2Q is the automaton transition function;
• F ⊆ Q is the set of accepting states.

When Q0 is a singleton, and |ρ(q, σ)| ≤ 1, for every q ∈ Q and σ ∈ Σ, A is said to be deterministic. When this is the case, we use q0 instead of Q0, and assume ρ : Q × Σ → Q.

1 In fact, all operators can be defined in terms of © and U.

The input words of A are the infinite words w = σ0σ1 · · · ∈ Σω . A run of A on an infinite word w is an infinite sequence of states r = q0q1 · · · ∈ Qω such that q0 ∈ Q0 and qi+1 ∈ ρ(qi, σi). A run r is accepting iff lim(r) ∩ F ̸= ∅, where lim(r) is the set of states that occur in r infinitely often. In other words, a run is accepting if it gets into F infinitely many times, which means, being F finite, that there is at least one state qf ∈ F visited infinitely often. The language accepted by A, denoted by L(A), is the set of (infinite) words for which there is an accepting run.

The nonemptiness problem for an automaton A is to decide whether L(A) ̸= ∅, i.e., whether the automaton accepts at least one word. The relevance of such problem for LTL follows from the correspondence obtained by setting the automaton alphabet to propositional interpretations, i.e., Σ = 2Prop . Then, an infinite word over the alphabet 2Prop represents an interpretation of an LTL formula over Prop. Formally, if the set of all models of an LTL formula ϕ is denoted as M(ϕ), the result is that:

Theorem 1 [Vardi andWolper, 1994] For every LTL formula ϕ one can effectively construct a B¨uchi automaton Aϕ whose number of states is at most exponential in the length of ϕ and such that L(Aϕ) = M(ϕ).

In general, the automaton Aϕ of Theorem 1 is nondeterministic. In fact, formulas exist for which no deterministic B¨uchi automaton accepts exactly its models, e.g., ϕ = ✸✷p. Thus, nondeterministic B¨uchi automata are strictly more powerful than deterministic ones. In the following, we only consider LTL goal formulae ϕ such that Aϕ is a deterministic B¨uchi automaton such that L(Aϕ) = M(ϕ). We call such formulas deterministic. Deterministic LTL formulas are general enough to capture many of the extended temporal goals and requirements that arise in practice.

3 The Problem

Given a (nondeterministic) planning domain D = 〈Act, Prop, S, S0, f〉, a finite-state controller (FSC) for D is a tuple Π = 〈C, c0, Γ, Λ, δ, Ω〉, where:

• C is the finite set of controller states;
• c0 ∈ C is the initial controller state;
• Γ = S is the controller input alphabet;
• Λ = Act is the controller output alphabet;
• δ : C ×Γ ↦→C is the controller transition function;
• Ω : C ↦→ Λ is the controller output function.

Formally, Π is a Moore machine whose input and output alphabets are the states and the actions of D, respectively. The machine is intended to "drive" D so as to make it show a desired behavior. Note that, besides being able to observe the domain state, Π owns an internal state, allowing it to track past events, although in a limited way, as typical of finitestate machines.

A Π-execution is a possibly infinite sequence η = c0 s0 -→ c1 s1 -→ · · · , such that ci+1 = δ(ci, si). A D-path µ = s0 a0 -→ s1 a1 -→ · · · is said to be induced by Π if there exists a Πexecution η = c0 s0 -→ c1 s1 -→ · · · such that ai = Ω(ci). If so,

Π is said to induce the D-trace τ = s0s1 . . .. A state c of Π is Π-reachable if there exists a Π-execution where c occurs.

We are interested in those FSCs that, when executed on D, yield only evolutions that satisfy a requirement expressed in the LTL goal. The following definitions capture this intuition. We say that a FSC Π realizes an LTL goal ϕ (on D) if for all the D-traces µ that Π induces on D, it is the case that µ |= ϕ. We say that Π fairly realizes an LTL goal ϕ (on D) if for all the fair D-traces µ induced by Π, µ |= ϕ.

Thus, the notion of goal realization requires all evolutions of D, obtained by executing Π, to satisfy ϕ. Observe that since the domain is nondeterministic, thus partially controllable, whenever Π prescribes the execution of an action in some state, it must also take care of all the possible outcomes, i.e., prescribing an action for each possible successor state.

An empty FSC inducing no D-trace, realizes any LTL goal. To prevent such degenerate cases, we introduce the following notion. A FSC Π for a domain D is said to be closed, if: 1. Ω(c0) and δ(c0, s0) are defined; 2. whenever a = Ω(c) and c′ = δ(c, s) are defined, for some c and s, it is the case that f(s, a) ̸= ∅, and, for every s′ ∈ f(s, a), Ω(c′ ) and δ(c′ , s′ ) are defined. In words, this definition requires Π to prescribe an executable action on both the initial state and on all the D-states reachable by executing actions prescribed by Π. In the rest of the paper we consider only closed controllers. The problem of interest can thus be expressed as follows:

Given a non-deterministic planning domain D and a deterministic LTL goal ϕ, build a closed finitestate controller Π that fairly realizes ϕ on D.

We refer to this the problem as the LTL fair realization problem (for deterministic LTL goals over nondeterministic planning domains). This is a generalization of fully observable, non-deterministic planning problem (FOND), with reachability goals replaced by LTL goals, as well as an instance of the general formal synthesis problem for deterministic LTL formulas, where non-determinism is assumed to be fair. While we implicitly assume fairness, in synthesis it is typically stated in the input.

The standard approaches to controller synthesis are based on symbolic methods that compute the states over which certain types of "games" can be won. For example, the problem of realizing ϕ = ✸p (eventually p), is mapped into that of finding the largest set S of states such that: S contains all the states satisfying p, and from any state in S, the system can be forced to reach a state satisfying p. If the initial state is in S, a strategy realizing ϕ can be obtained from the construction of S [Bloem et al., 2012]. Similarly, to realize ✷✸p (always eventually p), one computes the set of states from which the system can be forced to make p true infinitely often. Such sets S, called winning sets, are characterized by fixpoint formulas in the µ-calculus (over game structures), and are typically computed by symbolic methods. By taking advantage of the symbolic representation, these methods can deal with very large collections of states (see, e.g., [Burch et al., 1992]). Planning methods, on the other hand, are aimed at exploiting the structure of the planning domains by means of heuristics that operate on the compact representation of the domains.

We show below how to map the LTL fair realization problem into a planning problem. As a first step towards this goal, we show that we can restrict the search to controllers Π = 〈C, c0, S,Act, δ,Ω〉 of a specific class, for which all components are fixed except for the action selection function Ω. Thus, the search for FSCs that achieve a goal ϕ with (deterministic) automaton Aϕ will be reduced to the search for a policy Ωϕ mapping state-pairs 〈q, s〉 into actions where q is a B¨uchi automaton state and s is a domain state:

Theorem 2 Consider a planning domain D = 〈Act, Prop, S, s0, f〉 and an LTL formula ϕ such that there exists a deterministic B¨uchi automaton Aϕ = 〈S, Q, q0, ρ, F 〉 such that L(Aϕ) = M(ϕ). Then, there exists a FSC Π = 〈C, c0, S, Act, δ, Ω〉 that fairly realizes ϕ on D iff there exists a FSC Πϕ = 〈Q × S, 〈q0, s0〉, S,Act, δϕ,Ωϕ〉 that fairly realizes ϕ on D, such that: δϕ(q, s) = 〈q′ , s′ 〉 iff q′ = ρ(q, s) and s′ ∈ f(s, Ωϕ(q, s)).

Theorem 2 says that a FSC for realizing an LTL goal ϕ can be obtained from a policy π = Ωϕ over the domain D′ that is the product of the non-deterministic domain D and the deterministic B¨uchi automaton Aϕ. In the next section we show a theorem that characterizes the goal achieved by this policy over D′ , and the form in which such goal is achieved.

4 Reduction to Strong Cyclic Planning

A (nondeterministic) planning problem is a pair P = 〈D, G〉, where D is a planning domain and G ⊆ S a set of goal states. A policy π for a planning domain D is a function π : S → Act, mapping states into actions. A D-path µ is said to be induced by a policy π if µ = s0 π(s0) ---→ s1 π(s1) ---→ · · · . A D-state s′ is said to be π-reachable from a D-state s if there exists a finite path µ = s0 π(s0) ---→ · · · π(sk-1) -----→ sk induced by π, such that sj = s, for 0 ≤ j ≤ k, and sk = s′ , for k ≥ 1. A policy π is said to be a non-terminating strong cyclic solution to P if π(s0) is defined and for every state s π-reachable from s0, there exists a state s′ ∈ G π-reachable from s.

The following result tells us that the output function ΩA of the FSC ΠA of Theorem 2 can be easily extracted from a nonterminating strong cyclic solution π of a particular planning problem defined over the cross-product domain of D and Aϕ.

Theorem 3 Consider a planning domain D = 〈Act, Prop, S, s0, f〉 and an LTL formula ϕ such that there exists a deterministic B¨uchi automaton Aϕ = 〈S, Q, q0, ρ, F 〉 with L(Aϕ) = M(ϕ). Let D′ = 〈Act, Prop′ , S′ , s′0 , f ′ 〉 be the planning domain such that:

• Prop′ = Prop ∪ {pq | q ∈ Q};
• s′0 = s0 ∪ {pq0 };
• f ′ (s, a) = s′D ∪pq′ iff s′D ∈ f(sD, a) and q′ = ρ(q, sD), for sD = s ∩ Prop and pq ∈ s.

Further, let G = {s ∈ S′ | pq ∈ s, for q ∈ F}. Then, π : S → Act is a non-terminating strong cyclic solution to 〈D′ , G〉 iff the FSC Π = 〈Q× S, 〈q0, s0〉, S, Act, δ, Ω〉, with:

• Ω(q, sD) = π(s) for s = sD ∪ pq;
• δ(q, s) = 〈q′ , s′ 〉 for q′ = ρ(q, s), s′ ∈ f(s, Ω(q, s));

fairly realizes ϕ on D.

The theorem says that we can transform the problem of building a finite-state controller for an LTL goal into that of building a non-terminating strong-cyclic policy for a planning problem. We show next how to map the problem of computing a non-terminating strong cyclic policy for a nondeterministic problem P = 〈D, G〉 into the problem of computing a standard strong cyclic policy for a non-deterministic problem P ′ = 〈D′ ,G′ 〉, which can be computed with any existing, off-the-shelf, strong cyclic planner. A (standard) strong cyclic policy is a policy π such that if s is a non-goal state π-reachable from s0, then a goal state s′ is π-reachable from s [Cimatti et al., 2003]. The difference between standard (terminating) and non-terminating strong cyclic policies π is that the former can be undefined over the goal states, while the latter have to be defined over all π-reachable states, including goal states, as they must give rise to infinite executions.

Theorem 4 A policy π is a non-terminating strong cyclic solution π to P = 〈D,G〉 iff π is a strong cyclic solution to P ′ = 〈D′ ,G′ 〉, with D′ = 〈Act, Prop′ , S′ , s0, f ′ 〉 and G′ = {sg ∪ {ok} | sg ∈ G}, where:

• Prop′ = Prop ⊎ {ok}; 2
• S′ = S ∪G′ ;
• f ′ (s, a) = f(s, a) ∪ {sg ∪ {ok} | sg ∈ f(s, a) ∩G}, if f (s, a) ∩ G ̸= ∅, else f ′ (s, a) = f (s, a).

The transformation maps each goal state sg in P into a nongoal state sg of P ′ . In addition, a goal state sg ∪ {ok} that is added as a possible successor state of the state-action pairs (s, a) that can transition into sg. The transformation allows us to compute non-terminating strong cyclic solutions by resorting to planners for (standard) strong cyclic solutions. Notice that all the steps in such transformation involve only syntactic manipulations of the domain D and the B¨uchi automaton. Theorems 2-4 together result in the following theorem:

Theorem 5 If there exists a solution to the fair realization problem defined by a non-deterministic planning domain D and a deterministic LTL formula ϕ, then a non-deterministic planning problem P ′ = 〈D′ ,G′ 〉 can be constructed such that the strong cyclic solutions to P ′ yield a FSC that fairly realizes ϕ on D.

5 Implementation

In line with Theorem 5, we have implemented a compiler that maps the compact description of a non-deterministic domain P and an LTL goal ϕ, into a standard strong cyclic planning problem Pϕ in PDDL that can be solved with off-the-shelf planners. The first ingredient of the compilation is SPOT 3 , an available tool able to map a large class of LTL goals ϕ into deterministic B¨uchi automata Aϕ. We then take advantage of Theorems 3 and 4, for obtaining the strong cyclic planning problem Pϕ by means of syntactic transformations of P and Aϕ. Pϕ is the cross-product of P and the propositional representation of the automaton Aϕ, where an atom pq is introduced to represent each state q of Aϕ. The goal of Pϕ is the dummy atom ok, inserted as an additional possible outcome of the actions that can add an atom pq, for accepting state q of the automaton Aϕ. The cross-product is encoded into two different ways, which give rise to two different but logically equivalent encodings of the strong cyclic planning problem Pϕ. In the sequential encoding, domain actions are followed by actions that progress the state of the automaton Aϕ, according to its transition function. In the parallel encoding, a new action is created for representing each possible sequence of a domain action followed by an automaton transition. In order to solve the resulting strong cyclic planning problem we use the recent PRP planner [Muise et al., 2012], that like other recent solvers [Kuter et al., 2008; Fu et al., 2011], maps the strong cyclic planning problem into a sequence of classical planner calls.

2⊎ stands for disjoint union.

3 http://spot.lip6.fr/ltl2tgba.html

6 Experiments

We have tested the proposed approach by running the PRP planner over the problems Pϕ and comparing the method with the standard symbolic synthesis tool called TLV [Pnueli and Shahar, 1996], which provides an implementation of the algorithm for GR(1) synthesis described in [Bloem et al., 2012]. 4 TLV accepts the LTL goal ϕ directly along with a compact description of the non-deterministic domain obtained from P. In addition, we encode in LTL the assumptions about fairness so that the space of solutions of the two approaches coincide.

6.1 Lift

The Lift controller problem [Bloem et al., 2012] requires to build a lift controller for an n-floor building, that guarantees every request from a floor to be eventually served. The main fluents we use to model the domain are ati and reqi, one per floor (i = 1, . . . , n), which represent, respectively, the lift being at floor i, and a request having been issued from floor i. As to actions, we use push fi 1, push fi 2, move up from fi (i = 1, . . . , n - 1), and move down from fi (i = 2, . . . , n), with the following semantics: push fi 1 is executable only if ¬ati, and nondeterministically either sets the value of reqi to true or does nothing; push fi 2 is executable only when ati holds, and sets the value of reqi to false; move up from fi unsets fi and sets fi+1; move down from fi unsets fi and sets fi-1. The lift is initially at floor 1, and no request is issued. We require move-up actions to be executable only if some request is issued. To this end we use a fluent called in their precondition. To describe the domain evolution, we introduce auxiliary fluents that we use in combination with preconditions to force the alternate execution of a move and n push fi actions, i = 1, . . . , n. In this way, we capture all the possible situations the controller faces when the lift is at some floor. Notice that the nondeterminism of push fi 1 captures the fact that the lift may or may not be called from some floor. The LTL formula capturing the goal has the GR(1) form

4 Also certain non-GR(1) problems, such as Clerk (see below), can easily be rewritten as GR(1).

ϕ = ∧ni=1 ✷✸(reqi → ati). We generated 10 instances incrementing the number n of floors from 1 to 10.

6.2 Waldo

The problem involves a robot that must move between locations until Waldo is found [Kress-Gazit et al., 2007]. The robot moves in a circle of n rooms, and Waldo can appear non-deterministically (from nowhere) when the robot is in room i or i/2. When Waldo appears, the robot must remain in the same room. The robot must thus "patrol" rooms i and i/2 until Waldo appears. The LTL formula of this requirement is ✷✸(ri ∨ W) ∧ (ri/2 ∨ W), where W represents the appearance of Waldo. In our account, the behavior of Waldo is fair, meaning that when the robot visits rooms i or i/2 infinitely often, Waldo will eventually show up (in fact, infinitely often). This is captured as non-deterministic effects in the actions that take the robot into rooms i and i/2. The result of the fairness assumption in this problem is that the best valid policy is to go either to i or i/2, move one step away and return to the same location. As in the original problem formulation the robot has to bounce between locations i and i/2 until Waldo appears, we considered a formulation with an extra predicate visitedi to enforce that once the robot visits one target location, it has to visit the remaining ones before searching in the same location again. When every target location has been visited and Waldo didn't appear, the extra predicate search again becomes true and all visitedi false. The LTL goal is set to ✷✸(search again ∨ W). We generated 40 instances, incrementing the number n of rooms by 100, from 100 up to 4000.

6.3 Clerk

This domain models the actions of a clerk in a store. The problem requires to build a controller which guarantees that every client request is served. New customers show up requesting one of the n items or packages pi, which can be available or not. If the item is not available, the clerk buys the product from a supplier first. The available items pi are described by the fluents instore pi and the package the customer requests by fluent want pi. If no customer is requesting an item, the action request will nondeterministically make true one of the want pi fluents and the fluent item requested. If instore pi is true, the action sell pi renders instore pi and want pi to be false while making true item served. Otherwise, buy supply pi adds instore pi when want pi is true and instore pi false. The goal is ✷(item requested → ✸item served).

We tested also an extended version of the same domain where package pi must be stored and retrieved in a cell loci of a 1 × (n + 1) grid. The desk of the clerk is at locn+1. If a package is requested, the clerk has to find the package in the grid, pick it up and sell it to the customer at the desk. If a supplier brings a package, the clerk has to pick the package and store it in its correct location. The goal then is encoded with the formula ✷(active request → ✸(item served ∨ item stored)), where active request is made true every time the action request is applied, and made false once the request has been satisfied, either stored or served. Instances were generated for the two versions of the domain with number n of packages ranging from 1 to 20.

6.4 Results

All experiments were run on an Intel Core i7-3770 3.4GHz processor, with a timeout of 30 minutes and a memory limit of 4GB. The results are shown in Figure 1. In Lift, TLV is unable to solve 6 floors, while PRP solves up to 7 floors. The sequential encoding scales up better than the parallel one, which runs out of memory while parsing the problem with 5 floors. In Waldo: TLV solves 35 instances, taking 1788.6s to solve the instance with 3500 rooms, while PRP solves all 40 instances, taking 6.8s and 66.72s in the largest instance with 4000 rooms in the sequential and parallel encodings respectively. Finally, in Clerk, PRP solves the complete suite of benchamarks up to 20 packages with the parallel encoding, each instance in less than 0.25s. With the sequential encoding, PRP solves up to 16 floors in 26.54s, running out of memory in the larger instances. TLV fails even with 4 packages, and for 3 it takes 265s (against 0.04 of PRP). In the extended version of the domain, PRP based on parallel encoding solves all instances in the suite in less than 1.4s, while all instances up to 14 packages in 52.01s, when using the sequential encoding. TLV solves a few instances only, and is not shown.

The results of the experiments show that the planning approach scales up better than TLV, in particular, as the problems become more planning-like with many actions and propositions. The encoding of the cross-product between the planning domain and B¨uchi automaton, that has been implemented in two ways, sequential and parallel, makes a large difference in some cases, with the parallel encoding performing better as the size of the B¨uchi automaton decreases. Last, the LTL goal can often be encoded in many different ways too. In many of these domains there is an enumerative approach with goals like 'if requesti comes alive, then perform servei' and a generic approach like 'if there is request, then serve it', which can be rendered equivalent by tinkering with the planning domain. When this is possible, smaller automata are obtained, which benefits the planning approach further.

Finally, we performed tests on deterministic problems to compare with the approach reported recently in [Patrizi et al., 2011], where deterministic planning with general LTL goals is mapped into a classical planning problem that is solved once, and whose solution encodes a lasso-plan that achieves the LTL goal. For this, we considered their Gripper instances. In terms of time, both approaches performed similarly, with PRP being slightly faster on average (0.38s vs. 0.4s), and finding more compact policies. In terms of coverage, out of 500 instances, PRP solved 470, 70 more problems than the other approach, that time out in compilation. It is worth noting that our strong-cyclic-planning approach does not reduce to the classical approach in [Patrizi et al., 2011] over deterministic problems. This is because the proposed mapping makes the resulting problem Pϕ non-deterministic even if the original domain P is deterministic (this is the result of the transformation in Theorem 4 for mapping non-terminating strong cyclic policies into standard ones). Yet the approach appears to be competitive with the deterministic approach when this is used for computing lasso-plans.

7 Conclusions

We have considered the problem of planning in environments where the state is fully observable, actions have (fair) nondeterministic effects, and plans must generate infinite state trajectories for complying with LTL goals. The problem is a generalization of the fully-observable non-deterministic planning problem (FOND) where reachability goals are replaced by temporally extended LTL goals, and a special case of the more general formal synthesis problem where nondeterminism is assumed fair and LTL formulas encode deterministic B¨uchi automata. We have shown that the problem can be compiled into a strong cyclic planning problem that can be solved by off-the-shelf planners. The experiments show that the approach is computationally meaningful and has potential benefits in relation to standard symbolic synthesis methods. The proposed formulation extends the scope of current planning methods, which can thus be used effectively to generate controllers for systems that must operate continuously, under exogenous interventions that cannot be predicted or controlled.

Acknowledgments

This work was partly supported by the EU projects FP7ICT 257593 (ACSI) and EC-7PM-SpaceBook, and the ARC project LP110100115.