Towards Fully Observable Non-Deterministic Planning as Assumption-based Automatic Synthesis

1 Introduction

In this paper, we relate advanced forms of planning to the general long-standing Computer Science problem of automatic synthesis [Manna and Waldinger, 1987; Abadi et al., 1989; Pnueli and Rosner, 1989]: the problem of automatically building an executable piece of code from (high-level) user intent. Despite planning and synthesis not being areas too far from each other, the connection between the two worlds have not been much explored. We are not in fact the first in noticing that such a relation exists, in the planning community others have pointed it out; see [Pistore and Traverso, 2001]. Still, as no (complete) formalization has been presented, the relation is only informally analyzed. We concentrate in this work on fully observable non-deterministic (FOND) planning, a type of planning that has recently attracted much attention and which aims to accommodate events outside the control of the agent [Daniele et al., 2000]. In FOND planning, actions are non-deterministic, in that their execution yields one of a set of possible effects, and this is Nature's choice. Once the effect has ensued, however, the agent is able to observe it.

Strong cyclic plans-those that re-try until success is obtained-have arguably become the de-facto solution concept for FOND planning. Daniele et al. [2000] provided its first characterization in CTL, as those plans for which "in any of its executions, it is always the case that the goal is always reachable." This was later refined in [Pistore and Traverso, 2001; Cimatti et al., 2003] to disregard what happens after goal achievement. Then, with the advancement of planning

Nicolas D'Ippolito

Departamento de Computaci ´on, FCEN Universidad de Buenos Aires Buenos Aires, Argentina ndippolito@dc.uba.ar

and model checking technologies, several promising techniques and systems have emerged for solving FOND planning problems, such as PRP [Muise et al., 2012], NDP [Kuter et al., 2008], and FIP [Fu et al., 2011], MBP [Cimatti et al., 2003], and GRENDEL [Ramirez and Sardina, 2014]. The first three are built on top of classical planners, whereas the last two perform fix-point reasoning via model-checking type techniques. Nonetheless, the point is that they all amount to specialized-clever though often involved-algorithms for constructing "loopy" but "closed" plans.

In this work, we revisit what planning under nondeterministic actions is with the aim of framing it as a special case of controller synthesis [Pnueli and Rosner, 1989]. The study of both novel controller synthesis and planning techniques could lead to interesting developments in the planning community by taking advantages of the expressiveness and guarantees provided by the controller synthesis approaches. Moreover, whereas control synthesis was deemed computationally impossible in the past, recent approaches (e.g., [Bloem et al., 2012; D'Ippolito et al., 2011]) have shown that for some quite expressive specifications, the task is amenable for computation. In turn, planning problem specifications can inform meaningful specifications-for goals and assumptions-to the reactive synthesis field.

It turns out that to make such link evident, one needs to formalize the assumptions on the environments in which strong cyclic plans are guaranteed to eventually achieve their goals. Surprisingly, this aspect has merely been discussed at an informal level, by calling for "fair" environments, that is, those in which "all actions' outcomes will ensue infinitely often, if tried infinitely often." To settle that formally, we provide a logical characterization of the environment which complements that of "good" plans found in [Pistore and Traverso, 2001]. We show, with an example, that a naive interpretation of the fairness assumption does not yield the expected results, and provide a characterization that accounts for "failure independence." We prove that strong cyclic plans are indeed sound and complete solution concepts under such characterization. Finally, we argue that, by using the characterization developed, reactive synthesis [Pnueli and Rosner, 1989] can be directly used to solve FOND planning tasks, and show that, for the special case in which actions have "intended effects," existing effective synthesis techniques can be exploited.

2 Preliminaries

2.1 Fully Observable Non-Deterministic Planning

We mostly follow the characterisation of non-deterministic planning given in [Rintanen, 2008], as it provides a more formal framework than others to work on. However, such account is indeed equivalent to the usual "oneof" clauses in PDDL based characterisations [Gerevini et al., 2006].

A fully observable non-deterministic (FOND) planning problem is a tuple P = 〈P,O, sI, φgoal〉 consisting of a set of Boolean state propositions P (atoms), an initial state sI , a goal φgoal as a conjunction of literals (i.e., atoms or negated atoms), and an operator set O (see below). We use l to denote the complement of literal l.

A state s is a consistent set (or conjunction) of literals such that |s| = |P|-every atom is either true or false. We use S to denote the set of all states of task P.

An operator is a pair o = 〈Preo, Eff o 〉, where Preo is a condition describing the preconditions of operator o, and Eff o = e1 | · · · | en the (non-deterministic) effects of o, where each ei is a (deterministic effect) condition and n ≥ 1. The intended meaning is that one of the ei events ensue nondeterministically, by the environment's choice. Operator o is executable on a state s if s |= Preo. The successor states resulting from executing operator o in state s is defined as next(o, s) = JEff o Ks, where:

In general, JEff o Ks yields a set of states (one per effect of o); if o is deterministic (i.e., Eff o = e), then |JEff o Ks| = 1. A policy (or conditional plan) is a function π : S ↦→ 2O mapping states s ∈ S onto the set of executable operators π(s) such that if o ∈ π(s), then s |= Preo. The universal policy for a FOND problem P is ˆπ(s) = {o | o ∈ O, s |= Preo}. A policy π executed from state s defines a set of possible executions Λπ(s) made up of executions λ = s0o0s1 · · · sioisi+1 · · · , where s0 = s, oi ∈ π(si), si |= Preoi , and si+1 ∈ next(oi, si), for all i ≥ 0. The set of states relevant to a policy π from state s is defined as Sπ(s) = ⋃λ∈Λπ(s) {si | si ∈ λ} (we abuse notation and write s ∈ λ to say that execution λ mentions state s). A policy π is closed iff ⋃o∈π(si) next(o, si) ⊆ Sπ(sI) for all states si ∈ Sπ(sI), that is, π always returns an action for every nongoal state it reaches. In turn, a state s is reachable by a policy π from state s′ if there is a chance that following π leads the agent to s; formally, there exists λ ∈ Sπ(s′ ) such that s ∈ λ.

When it comes to FOND planning, the usual solution concept in the literature is that of strong cyclic plans.

Definition 1 (Strong Cyclic Plan [Cimatti et al., 2003]). A strong cyclic plan is a closed policy such that a goal state is reachable from every reachable state using the policy. ■

Strong policies are a special case of strong cyclic policies, for which all executions are finite and acyclic: they solve the planning problem in a bounded number of steps. We close by noting that non-deterministic planning with full observability is EXPTIME-complete [Rintanen, 2004].

2.2 Labelled Transition Systems

Labelled Transition Systems (LTS) [Keller, 1976] are operational models that describe behaviour in terms of the occurrence of actions and their effect on the system's state. LTSs are widely used in many domains, particularly, as description language for event-based controllers and controller synthesis.

Definition 2 (Labelled Transition Systems). A labelled transition system (LTS) is a tuple E = (S,A,∆, s0), where S is a finite set of states, A is its communicating alphabet, ∆ ⊆ (S ×A× S) is a transition relation, and s0 ∈ S is the initial state. We use ∆(s) = {ℓ | (s, ℓ, s′ ) ∈ ∆} to denote the set of enabled actions in state s. A sequence t = ℓ0ℓ1 · · · is a trace in E if there exists a sequence s0ℓ0s1ℓ1 · · · such that (si, ℓi, si+1) ∈ ∆ for all i ≥ 0. ■

The parallel composition of two LTS Ei=(Si, Ai, ∆i, ei0), with i ∈ {1, 2}, is defined as the LTS E1‖E2 = (S1 × S2,A1 ∪ A2,∆, (e10, e20)) obtained from the synchronous product of E1 and E2, and encodes the concurrent execution of E1 and E2 by interleaving non-shared actions but forcing synchronisation on shared actions [Hoare, 1978].

2.3 Temporal Logics

Temporal logics are logic formalisms tailored for statements and reasoning which involve the notion of order in time. They allow the formal specification of behavioral properties of systems [Pnueli, 1977] and are the basis for model checking and synthesis. Some widely known and used such logics are CTL* and its fragments CTL and LTL [Emerson and Halpern, 1986; Clarke and Emerson, 1982]. In particular, CTL has been proved to be a convenient framework for describing the notion of strong cyclic plans in a precise and concise manner. The syntax of CTL* is defined with the following grammar:

where p ranges over the set of propositions. Formulas of the form Ψ are called state formulas, whereas those of the form ϕ are said to be path formulas. Formula AΨ (EΨ) states that all executions (some execution) from the current state satisfy property Ψ. Then, path formulas Xϕ, Fϕ, and Gϕ state that ϕ is true in the next state of the path, eventually in the path, or always along the path, resp. Finally, ϕ1Uϕ2 says that ϕ1 holds along the path until ϕ2 becomes true and ϕ2 is eventually true; ϕ1Wϕ2 is its weak version where ϕ2 is not required to eventually come true in the path. Common combinations of path and state quantifiers allow us to say things like all or some next states satisfy ϕ (AXϕ and EXϕ), and ϕ holds in all or some executions (AGϕ or EGϕ).

The meaning of such CTL* formulas is given over the states and paths of a transition system, with a branching-time interpretation of time. Concretely, a CTL* transition system over a set of propositions P, also called Kripke structure, is a tuple K = 〈W, R, P 〉, where:

• W ⊆ 2P is the set of states of K; and
• R ⊆ W ×W is the transition relation of K such that for every w ∈ W, there exists w′ ∈ W such that R(w, w′ ). When R(w1,w2) holds, it means that state w2 is a possible successor of state w1.

A run in K from state w0 is an infinite sequence π = w0w1w2 · · · such that R(wi,wi+1), for all i ≥ 0. Given a state formula Ψ and a state w ∈ W, we can define whether Ψ holds true in structure K at state w, denoted K,w |= Ψ. Finally, LTL is the fragment obtained from CTL* by withholding the A and E quantifiers and assuming universal path quantification. CTL, in turn, is the CTL* fragment obtained by requiring that each temporal path quantifiers (e.g., X, F, etc.) be under the immediate scope of an A or E quantifier.

A variant of LTL used in the Software Engineering context (from where we will import certain results) is FLTL (fluentLTL) [Giannakopoulou and Magee, 2003], which is more tailored towards reasoning about fluents via automata-like structures with emphasis on transitions' labels rather than states' labels. A fluent f = 〈If, Tf, initf〉 is defined by sets of disjoint initiating and terminating actions If and Tf from a universal set of actions Act, resp., and an initial value initf.

Given a set of fluents, the truth of an FLTL temporal formula is defined relative to an infinite trace t = a0a1 · · · over the universal set of actions Act. If t is an infinite trace, the satisfaction of an FLTL formula ϕ at position i, denoted t, i |= ϕ, is standard and omitted. However, we just point out that since FLTL traces focus on action/events (i.e., transitions labels in an LTS), the truth of a fluent f at a certain prefix ti of trace t = a0a1 · · · is defined as: t, i |= f if and only if one of the following conditions holds: (i) initf ∧ (∀j.0 ≤ j ≤ i → aj /∈ Tf); and (ii) ∃j.(j ≤ i∧aj ∈ If )∧(∀k ∈ N.j < k ≤ i → ak /∈ Tf). We say that ϕ holds in t, denoted t |= ϕ, if t, 0 |= ϕ. Finally, a FLTL formula ϕ holds in an LTS E (denoted E |= ϕ) iff t, 0 |= ϕ, for all infinite traces t of E.

3 Strong-cyclic Plans and Fair Environments

In this section, we revisit the semantics of FOND planning, with special focus on the "environment" where plans are to be executed. In particular, whereas the notion of strong cyclic plans have been vastly studied and formally defined, the type of environments in which such plans will succeed are often discussed at an informal level.

The first precise analysis of what a solution is for FOND planning was given by Daniele et al. [1999; 2000]. There, the authors formally defined strong cyclic plans through a CTL formula on their executions. To capture all executions of a policy, they defined what is basically the projection of the underlying state model for a planning task onto the policy.

Definition 3 ((P, π)-structure). Let P = 〈P, O, sI , φg〉 be a FOND planning problem over the set of propositions P and π a policy over P. The induced structure of (P, π) is a Kripke structure KπP = 〈W, R, P 〉, where:

• W = {〈s, o〉 | s ∈ 2P , o ∈ O, s |= Preo}. Intuitively, 〈s, o〉 represents the execution of operator o in state s;

Structure KπP represents all evolutions of policy π when executed in planning domain P. It is straightforward to define a structure representing all possible executions of the planning domain, by considering the universal policy.

Definition 4 (P-structure). The structure induced by a FOND planning problem P is defined as the Kripke structure KP = KˆπP , where ˆπ stands for the universal policy. ■

So, Daniele et al. [1999; 2000] defined a policy π as a strong cyclic solution for a planning problem P iff KπP , 〈sI, oI〉 |= AGEFφgoal, for all oI ∈ π(sI). In words, starting from the initial state, whatever actions we choose to execute (from the policty) and whatever their outcomes are, we always (AG) have a way of reaching the goal (EFφgoal).

Because goals are achievement goals in planning, what happens after the goal is achieved is irrelevant. Hence, Daniele et al.'s definition was then further refined as follows: Definition 5 ([Pistore and Traverso, 2001]). A policy π is a strong cyclic plan solution for a FOND planning problem P iff KπP , 〈sI, oI〉 |= A(EFφgoalWφgoal), for all oI ∈ π(sI). ■

In words, in all possible executions of the policy, the goal is always eventually reachable, at least until the goal is indeed reached. Observe that this definition precisely captures the notion of closeness and goal-reachable (as in Definition 1).

The availability of a precise notion for strong-cyclic plans has facilitated the development of various techniques capable of synthesising such type of plans. Planning systems like MBP [Cimatti et al., 2003], PRP [Muise et al., 2012], FIP [Fu et al., 2011], and GRENDEL [Ramirez and Sardina, 2014] all search for policies that are closed and goal-reachable.

Nevertheless, besides understanding what a strong-cyclic plan amounts to, we argue here that it is also important to understand and formalize the contexts under which these type of plans will indeed achieve the objectives, namely, bringing about the goal. This has not received much attention and has mostly been discussed informally.

Clearly, under non-determinism, there is in principle the possibility of never achieving the goal, as "strong cyclic solutions can produce executions that loop forever" (without ever reaching the goal) [Cimatti et al., 2003]. However, the common understanding in the literature is that strong cyclic plans are adequate solutions under the assumption that the underlying environment described by the planning domain is ''fair." Unlike strong cyclic plans, which have been formally characterized (see above), this fairness assumption is always stated at an informal level. We shall provide a precise characterization of such fairness in LTL and show that strong cyclic plans are sound and complete plan types for fair domains.

A usual (informal) understanding is that fair domains are those for which "if an action is executed infinitely many times, every non-deterministic outcome will occur infinitely often." Formally, this can be stated as the following strongfairness LTL constraint (on the induced structure KP):

Note that while strong cylic plans have been characterized in CTL (Definition 5), Φfair P above is an LTL formula not expressible in CTL. While simple, D'Ippolito et al. [2011] argued, in the context of reactive synthesis for Software Engineering, that such strong-fairness assumptions are not enough to guarantee success of controllers that are meant to "re-try." Consider the following counter example.

Example 1. Imagine the problem of opening a door that has some operational defects, by inserting the key and then turning the knob. However, both actions may fail nondeterministically and not achieve their objectives. When that happens, the agent has to take the key out (which can only be done with the knob turned) and start all over again. Thus, consider planning problem Psafe = 〈P, O, sI , φgoal〉, where:

• P = {open, kIn, kStuck, turned}.
• O includes the operators:
• INSERT = 〈¬kIn, kIn | kIn ∧ kStuck〉.
• TURN=〈kIn ∧¬turned, open ∧ turned | turned〉.
• REMOVE=〈turned, ¬kIn∧¬kStuck∧¬open∧¬turned〉.
• sI = {¬open, ¬kIn, ¬kStuck, ¬turned}.
• φgoal = open ∧ ¬kStuck.

Take next the following (partial) policy π: (i) if s |= ¬kIn, then perform INSERT; (ii) if s |= ¬turned∧kIn, then perform TURN; and (iii) if s |= turned, then perform REMOVE.

It is not hard to see that π is a strong cyclic solution: it continuously tries to first insert and use the key, and then turn the knob and remove the key, until success is achieved.

Now, the formula Φfair Psafe , as defined above, implies that if the agent tries to use the key infinitely often, then she will succeed infinitely often. Similarly, if the agent keeps turning the knob, then she will keep succeeding getting the door open. It turns out, though, that:

That is, there is an execution of π in P in which all outcomes of INSERT and TURN arise infinitely often, but it is always the case that either the door is closed or the key stuck. In fact, consider the following states of KπPsafe : (i) w0 = 〈sI, INSERT〉; (ii) w1 = 〈{kIn, kStuck}, TURN〉; (iii) w2 = 〈{kIn, turned}, REMOVE〉; and (iv) w3 = 〈{kIn}, TURN〉; (v) w4 = 〈{kIn, open, kStuck, turned}, REMOVE〉. Then, run λ = (w0w1w4w0w3w2)ω does satisfy the assumption formula Φfair Psafe , but it never reaches the goal. Intuitively, the failure of the action TURN is not independent of failure of previous action INSERT-their failures are "synchronized."□

The example above shows that the failures and successes of two non-deterministic actions can be "coordinated" in a way that will preclude goal achievability, despite the fact that all outcomes of both actions ensue infinitely often.

To rule out coordinated outcomes D'Ippolito et al. [2011] provided the stronger notion of t-strong fair environments, but their framework assumes that it is known which action outcomes are "good" (and which ones are considered "failures"). Still, the intuition there is to have action-outcome fairness in every state, as captured by the following definition.

Definition 6 (State Strong Fairness; t-strong fair). Let P be a planning problem and KP = 〈W, R, P〉 its corresponding Kripke structure. The state strong, or simply t-strong, fairness constraint is defined as the following LTL formula:

A run of λ of KP is t-strong fair if λ |= γ sfair

In words, γ sfair P states that if an operator is executed infinitely often in the same state, then all its effects ought to arise infinitely often. This LTL constraint formalizes [Cimatti et al., 2003]'s claim that unfair executions are those where "some actions are executed infinitely often in given states, but some of its outcomes never occur," and corresponds to the semantically expressed requirement used in various FOND planning works (e.g., [Patrizi et al., 2013; Ramirez and Sardina, 2014; Geffner and Bonet, 2013]).

Returning to our example above, the run λ does not satisfy γ sfair Psafe , and KπP |= A[γ sfair Psafe → Fφgoal] holds.

We now have all the machinery to state the main contribution of this section, namely, linking state strong fairness with Pistore and Traverso [2001]'s account of strong cyclic plans (see Definition 5). First we show that all such plans do achieve the goal in state strong fair environments.

Theorem 1. Let π be a strong cyclic plan for a FOND planning problem P. Then, KπP , 〈sI, oI〉 |= A[γ sfair P → F(φgoal)], for all (initial) operators oI ∈ π(sI).

This theorem provides a "soundness" result for state strong fair environments. More importantly and less obvious, if a plan guarantees the goal in a state strong fair environment, then it has to be strong cyclic.

Theorem 2. Let π be a policy and P a FOND problem such that KπP , 〈sI , oI〉 |= A[γ sfair P → F(φgoal)], for all (initial) operators oI ∈ π(sI). Then, π is a strong cyclic plan.

The above two theorems say that state strong fairness is a complete characterization of the type of environment for which strong cyclic plans are successful. We note that, together, the above theorems are closely related to Theorem 2 in [Patrizi et al., 2013], though ours crystallize the assumption-solution relationship directly within Traverso et al.'s FOND planning foundational framework. Having a precise characterization of what adequate environments are opens the door for applying (reactive) synthesis techniques to solve FOND problems. That is the topic of the next section.

4 FOND Planning via Reactive Synthesis

Reactive synthesis or controller synthesis studies techniques that given a model of the assumed behaviour of the environment (E) and a system goal (G), produces an operational behaviour model for a component M that when, executed in an environment consistent with the assumptions, results in a system that is guaranteed to satisfy the goal, namely, E‖M |= G.

Arguably, the application of controller synthesis as means for solving planning problems has been discouraged due to the high complexity of the general approach. Indeed, controller synthesis is, in general, computationally expensive: synthesising for LTL goals is 2EXPTIME complete and known techniques have resisted practical implementations due to complementation [Pnueli and Rosner, 1989; Kupferman et al., 2006]. However, recent advances (e.g., [Bloem et al., 2012; D'Ippolito et al., 2011]) may, under appropriate assumptions, provide efficient solutions to planning problems. The fact is that restricting the form of the specification system goal allows for more effective solutions and implementable systems. For instance, goal specifications consisting uniquely of safety requirements can be solved in polynomial time, and so can particular, yet expressive, subsets of liveness properties such as GR(1) [Piterman et al., 2006].

As stated in Section 3, FOND strong cyclic plans are guaranteed to achieve the goals in t-strong fair environments. Following [Bloem et al., 2012] and relying on Theorems 3 and 4, one can solve a FOND planning task P with goal φgoal by checking LTL realizability of specification formula

where ϕ1P and ϕ2P are simple (safety) LTL formulas encoding structure KP. 1 Unfortunately, ϕP results in an expression that does not allow for efficient synthesis techniques, as it does not fall into known efficient LTL fragments like GR(1). Hence, in general, there is still an efficiency challenge when solving FOND planning via controller synthesis.

In some cases, however, it is possible to reduce a planning problem to an equivalent efficient controller synthesis one. For example, De Giacomo et al. [2010a] does so for standard conditional planning (i.e., planning for strong solutions). Here, we discuss a special such case for FOND planning, namely, when every action of a non-deterministic planning problem can be annotated with its "expected" or "intended" effect-that is, actions have a clear fail/success semantics. For instance, in the example in Section 3, the expected effect of turning the knob is to successfully open the door. All other effects can be considered failures. Arguably, many meaningful FOND planning problems come with a clear success/failure semantics of actions.

In what follows, we show how efficient reactive synthesis techniques developed in the area of Software Engineering can be imported to solve this type of planning problems. Specifically, we rely on D'Ippolito et al. [2011]'s polynomial approach to building LTS controllers for control problems with explicit description of failures against GR(1)-like specifications. Failures are defined by introducing try-response sets that relate the attempt to perform a controlled action and the corresponding environment's reaction. Technically, a tryresponse triple is a tuple t = 〈a, suca, faila 〉 where a and suca are actions in the environment model representing an action and its intended result, respectively, and faila is a set of actions representing failures of a's execution. In planning terms, a try would be an operator, while the responses would its effects. A key aspect of the approach is the Strong Independent Fairness (SIF) condition, which provides restrictions on how failures behave [D'Ippolito et al., 2011, Def. 4.3]. Intuitively, SIF requires a windows of opportunity ("gaps") in which all expected effects are executed without any failures. It turns out that the SIF assumption allows to reduce the problem of having gaps with no failures to one in which failures are assumed to occur finitely.

When interpreting failures as operator's effects, most of the required restrictions for try-response triples are inherently guaranteed (e.g., re-tries cannot occur before a response), except for one restriction that needs to be lifted. While [D'Ippolito et al., 2011] assumes single action representation for failures and successes, here we need failures to be a set of actions-the set of non-intended effects. However, since their approach reduces to solving a control problem where failures occur only finitely often, having multiple failures for the same try action does not affect key fact that effective controllers (re)try actions knowing that success will eventually occur. For lack of space we omit the technical details of such generalization to set of failures.

1 It is possible to, almost directly, transform KP into a game structure G as used in [Bloem et al., 2012], and then extract ϕ1P and ϕ2P fromG. For lack of space, we omit this here.

Next, we formally define try-response sets for a given LTS restricting attention to the requirements described above.

Definition 7 (Try-Response). Let E = (S, A,∆, s0) be an LTS and Ac ⊆ A (the set of controllable actions). Set T is a try-response set for E if:

1. (a, suca, faila ) ∈ T iff a ∈ Ac, suca ∈ A \ Ac, and faila = {fail1a , . . . , failka } ⊆ A \ Ac for some k ≥ 1.
2. For all ta = (a, suca, faila ), tb = (b, sucb, failb ) ∈ T, if a = b then ta = tb.
3. E |= G[X(∨1≤i≤|faila | failia ∨suca) ↔ a], for all a ∈ Ac
4. For all s ∈ S and trya ∈ Ac, faila is enabled from s iff suca is enabled from s. ■

We note that this definition is a special case of that in [D'Ippolito et al., 2011], tailored to the fact that outcomes ensue immediately after operators' executions. In their work, they also need to deal with delayed failures/successes.

Now, the specific control problem we are interested in is defined with an LTS environment model, a GR(1)-like specification, a set of controllable actions, and a try-response set.

Definition 8 (Recurrent Success LTS Control). A recurrent success LTS control (RSGR) problem is a tuple E = 〈E,Ac, ϕ, T〉 where E is an LTS, Ac is a set of controllable actions, ϕ is a GR(1) FLTL formula, and T is a try-response set for E.

A solution for E is an LTS M with controlled actions Ac such that E only disables controllable actions, E‖M is deadlock free, and every trace π inM‖E is such that π |= ϕ. ■

That is, a solution to an RSGR control problem is an LTS controller that, in parallel composition with the environment model, meets the system specification goal. Thanks to the assumed failure semantics, such controller can be computed in polynomial time via a reduction to a GR(1) synthesis task [D'Ippolito et al., 2011].

So, let us next show how to reduce a FOND planning problem with intended effects to an RSGR control problem.

Definition 9 (FOND to RSGR). Let P = 〈P,O, sI, φgoal〉 be a a FOND planning problem, such that each operator o ∈ O is defined as o = 〈Preo, Eff o , Into〉 where Into ∈ Eff o stands for the intended effect of operator o. The corresponding RSGR problem EP = 〈E, Ac, ϕ, T 〉 is defined as follows (here Eff (O) = {e | o ∈ O, e ∈ Eff o} is all the effects of O):

• Ac = O;
• T = {(o, Into, Eo) | o ∈ O and Eo = Eff o \ Into}; and
• ϕ = F(∧l∈φgoal fl ), where:

A trace of E is an interleaving sequence of operators and effects (from where one can reconstruct the fluents that hold true at any point). Observe that a controller for an RSGR control problem only restricts controllable actions (in our case, planning operators). Also, as we deal with reachability goals, it does not require additional memory: effectively, it is a subgraph of the environment model. This last property enables us to produce a strong cyclic policy from it.

Definition 10 (LTS to Policy). Given a planning problem P = 〈P,O, sI, φgoal〉, and an LTS M = (S,A,∆, s0) solution for the RSGR control problem EP obtained from P as described above, we construct M's associated policy πM as follows: for all s ∈ 2P : o ∈ πM(s) iff o ∈ ∆(s). ■

So, the next result states that the induced policy from a solution to the corresponding RSGR control problem is indeed a strong cyclic solution for the planning task of concern.

Theorem 3 (Soundness). Let P be a planning problem with goal φgoal, M be an LTS solution to the RSGR control problem EP, and πM the policy obtained from M. Then, KπM P , 〈sI, oI〉 |= A(EFφgoalWφgoal), for all oI ∈ πM(sI).

Proof Sketch. Suppose KπM P , 〈sI, oI〉 ̸|= A(EFφgoalWφgoal). Hence, there is a state s in KπM P such that every execution λ in KπM P that visits s (i.e., s ∈ λ) is such that λ ̸|= Fφgoal. By construction, s also belongs to M. Further, all traces in M that visit s must also avoid the goal-i.e., never satisfy the FLTL formula (∧l∈L(φgoal) fl ). In particular, every trace t satisfying SIF condition that visits s will not satisfy the goal (i.e. t ̸|= F(∧l∈L(φgoal) fl )), which contradicts our hypothesis. □

A direct consequence of Theorems 1 and 3 is that KπP |= A[γ sfair P → Fφgoal]. Secondly, if the FOND problem has a solution that is based on the operators' intended effects, then it is accounted in the solution to the corresponding RSGR problem. Intuitively, a policy is intention-based if it can reach the goal relying (eventually) only on the intended effects of operators-i.e., it achieves the goal "under no failures."

Definition 11 (Intention-Based Policy). Let P be a FOND planning problem with goal φgoal and operators of the form o = 〈Preo, Eff o , Into〉, where Into ∈ Eff o stands for the intended effect of o. A strong cyclic policy π for P is intentionbased iff for all wI ∈ {sI}×π(sI):

Theorem 4 (Completeness). Let P be a problem, and EP its corresponding RSGR control problem. If an intention-based strong cyclic policy π for P exists, then there exists a solution M for EP such that π ⊆ πM.

Proof Sketch. We construct an LTS M from policy π and show that M is a solution to EP. Let M = (S,A,∆M, s0) be an LTS defined as follows: s0 = sI ; S = 2P ∪ (2P × O);

A = {e | O, e ∈ Eff o } ∪ O; and ∆ = {(s, o, (s, o)) | o = π(s)} ∪ {((s, o), eo, s′ ) | eo ∈ Eff o , s′ ∈ JeoKs}. Now, the proof amounts to proving that for all traces t of M‖E, if t is SIF, then t |= F(∧l∈φgoal fl ). Since t is SIF, we know that t exhibits long enough gaps showing all intended effects of operators and no failures. Consider the prefix ti of t that includes the first such a gap. There exists an execution λti of policy π corresponding to prefix ti , which is "intended base" and hence achieves the goal. Therefore, prefix ti also achieves the goal specification and t |= F(∧l∈φgoal fl ) applies. □

Now, observe that [D'Ippolito et al., 2011] proved that solving a RSGR control problem can be done polynomially, by reducing it to a GR(1) synthesis task [Bloem et al., 2012]. Since the encoding of a FOND problem into a RSGR control one (Definition 9) is exponential, we get that we can use reactive synthesis to obtain intended-based strong cyclic solution in exponential time (which is the complexity of conditional planning). In addition, unlike standard solutions via specialized FOND algorithms, the policy is "maximal," in that it accounts for every initial state for which a solution exists.

5 Conclusions

In this paper we formally studied the kind of environments in which strong cyclic plans are adequate, thus complementing the existing formal characterization of such plans in CTL and contributing to bridging the gap between automated planning and reactive synthesis. We showed that an adequate fairness assumption should encode the independence of different nondeterministic steps, and provided a characterization of such environments in CTL*/LTL. We argued that doing so allows for direct specification of the FOND planning task into a reactive synthesis one. While the general synthesis task is not amenable for efficient computation, we showed a special case of FOND problems-those in which actions have intended effects--for which low complexity techniques are available.

We believe that making the connection between planning and controller synthesis more evident can benefit both areas. Automated planning can exploit recent powerful techniques-like synthesis of GR(1) or safety specifications-and open for more general planning settings. As pointed out in [De Giacomo et al., 2010b], one could be interested in planning under "selective" and/or "conditional" fairness assumptions (e.g., the dice is fair unless an action has "loaded" it), something that specialized planners cannot handle. Indeed, the special case of actions with intended effects is one such case. For reactive synthesis, planning settings can provide concrete applications and inform what types of system goal specifications are meaningful and worth studying.

In future work, we plan to investigate other solution concepts for non-deterministic planning. In particular, we are interested in fault-tolerant planning [Domshlak, 2013].

Acknowledgments

We thank the anonymous reviewers for their very helpful comments. We acknowledge the support of the Australian Research Council under a Discovery Project (DP120100332), and of projects ANPCYT PICT 2012-

0724/2011-1774/2013-2341, UBACYT 036/0384, CONICET PIP 11220110100596CO, and MEALS 295261.