Plan Synthesis for Knowledge and Action Bases

1 Introduction

Recently, there has been an increasing interest in formalisms that integrate static structural knowledge, as expressed, e.g., in description logics (DLs) [Baader et al., 2003], with actionbased mechanisms, to capture a domain's evolution over time. Combining these two aspects into a single logical system is known to be difficult and easily leading to undecidability, even for simple forms of inference about system dynamics, when the logics used are rather limited [Wolter and Zakharyaschev, 1999; Gabbay et al., 2003]. To overcome these restrictions, a recent line of work by Bagheri Hariri et al. [2013b] has introduced Knowledge and Action Bases (KABs). Such systems rely on Levesque's functional approach [Levesque, 1984] to operate over a full-fledged DL knowledge base (KB), by means of actions: actions evolve the system by querying the current state using logical inference (ASK operation), and then using the derived facts to assert new knowledge in the resulting state (TELL operation).

⇤We acknowledge the support of: Rip. Diritto allo Studio, Universit`a e Ricerca Scientifica of Prov. Autonoma di Bolzano-Alto Adige, project VERISYNCOPATED; the EU FP7 large-scale integrating project Optique (FP7-IP-318338); and the UniBZ CRC projects KENDO and OnProm.

Michele Stawowy

IMT Lucca, Italy michele.stawowy@imtlucca.it

A prominent feature of KABs is that actions allow one to incorporate into the KB external input provided by fresh objects taken from an infinite domain. This gives rise, in general, to an infinite-state system, in which reasoning is undecidable. Nevertheless, decidability of verification of first-order temporal properties has been obtained for KABs that are statebounded [Bagheri Hariri et al., 2013a; 2014], i.e., in which the number of objects in each single state is bounded a-priori, but is unbounded along single runs, and in the whole system.

Here, we study the problem of planning, specifically plan existence and synthesis [Ghallab et al., 2004; Cimatti et al., 2008], for knowledge-intensive dynamic systems over infinite domains. For doing so we consider a variation of KABs, termed Explicit-Input KABs (eKABs), more suited for our purposes, in which the input-related information for an action is made explicit in its signature, and not hidden in its conditional effects. In fact, eKABs can be considered as a concrete instantiation of the more abstract framework of Description Logic-based Dynamic Systems (DLDS) [Calvanese et al., 2013b], and inherit its possibility of abstracting away the specific DL formalism used to capture the underlying KB.

We show that, in line with previous work on planning in rich settings [Erol et al., 1995], plan existence is undecidable even for severely restricted eKABs. We prove decidability in PSPACE data complexity of such problem, for state-bounded eKABs, by combining techniques based on standard planning, DL query answering, and finite-state abstractions for DLDSs. Our work is similar in spirit to the one by Hoffmann et al. [2009], as combining a rich knowledge-based setting with the possibility of incorporating external input. However, to the best of our knowledge, our setting is the first one where planning is decidable without severe restrictions, in particular on how the external input is handled. We present a sound and complete algorithm, returning plans that represent templates for the original synthesis problem, defined over an infinite domain. We then concentrate on eKABs based on lightweight DLs of the DL-Lite family [Calvanese et al., 2007b; 2009] and show that, in this case, plan synthesis can also be tackled by compilation into standard ADL, which can then be processed by any off-the-shelf ADL planner [Pednault, 1994].

2 Description Logic Knowledge Bases

Let ∆ be a countably infinite universe of objects, acting as standard names [Levesque and Lakemeyer, 2001]. A (DL)

knowledge base (KB) hT↪Ai consists of a TBox T, capturing the intensional knowledge on the domain of interest, and an ABox A, capturing the extensional knowledge: T is a finite set of universal, first-order (FO) assertions based on concepts (unary predicates) and roles (binary relations); A is a finite set of assertions, or facts, i.e., atomic formulas N(d) and P(d↪ d0 ), with N a concept name, P a role name, and d↪ d0 2 ∆. By ADOM(A) we denote the set of objects occurring in A. For details on DLs, we refer to [Baader et al., 2003]. To maintain a clear separation between the intensional and the extensional levels, we disallow nominals (concepts interpreted as singletons) in T .

We adopt the standard FO semantics for DL KBs. When hT↪Ai is satisfiable, i.e., admits at least one model, we also say that A is T -consistent. A KB hT↪ Ai logically implies an ABox assertion ↵, written hT↪Ai ♣= ↵, if every model of hT↪Ai is also a model of ↵. Two ABoxes A1 and A2 are logically equivalent modulo renaming wrt. a TBox T , if they imply the same assertions, up to object renaming. When this holds, we write A1 ⇠=hT A2, where h denotes the bijection that renames the objects occurring in A1 into those in A2.

We use queries to extract information from a KB. A union of conjunctive queries (UCQ) q over a KB hT↪ Ai is a FO formula W1in 9~ yi.conj i(~x↪ ~ yi), where conj i(~x↪ ~ yi) is a conjunction of equality assertions and atoms mentioning concept/role names of T, with variables from ~x [ ~yi and objects as terms. A boolean UCQ is one without free variables. By ANS(q↪ T↪A) we denote the set of (certain) answers of a query q over a KB hT↪Ai, consisting of all the substitutions ✓ of q's free variables with objects from ADOM(A), s.t. q✓ holds in every model of hT↪Ai. We also consider the EQLLite extension of UCQs [Calvanese et al., 2007a], referred to as ECQs. The language of ECQs over a TBox T is: 1

where q is a UCQ. The certain answers ANS(Q↪ T↪A) of an ECQ Q over hT↪ Ai are obtained by first computing, for each atomic ECQ [q], the certain answers of q, and then composing the obtained answers through the FO constructs in Q, with existential variables ranging over ADOM(A). Hence [q] acts as a minimal knowledge operator, and negation and quantification applied over UCQs are interpreted epistemically [Calvanese et al., 2007a]. Under this semantics, ECQs are generic, in the sense of genericity in databases [Abiteboul et al., 1995]: a query evaluated over two logically equivalent ABoxes returns the same answer, modulo object renaming.

As customary, we consider DLs for which query answering (and hence the standard reasoning tasks of KB satisfiability and logical implication) is decidable. In our examples, we use ALCQIH [Baader et al., 2003]. We also consider lightweight DLs of the DL-Lite family, in particular DL-LiteA [Calvanese et al., 2009], for which checking KB satisfiability and answering ECQs over a KB are both FO-rewritable [Calvanese et al., 2007a; 2009]. The latter means that every ECQ Q expressed over a DL-LiteA TBox T can be effectively rewritten into a FO query rew(Q↪ T) s.t., for every ABox A, the certain answers ANS(Q↪ T↪ A) can be computed by evaluating rew(Q↪ T) over A seen as a database under the closedworld assumption. Also, T -consistency of A can be checked by evaluating over A an ECQ QTunsat (depending on T only).

1 We consider ECQs that are domain-independent and hT↪Airange restricted [Calvanese et al., 2007a].

3 Explicit-input Knowledge and Action Bases

We define Explicit-input Knowledge and Action Bases (eKABs) parametrically wrt a DL L. An L-eKAB K is a tuple hC↪ C0↪ T↪ A0↪ ⇤↪ Γi, where:

• ÷ C0 ⇢ C is a finite set of distinguished objects;
• ÷ C ✓ ∆ is the (possibly infinite) object domain of K;
• ÷ T is an L-TBox;
• ÷ ⇤ is a finite set of parametric actions;
• ÷ A0 is an L-ABox all of whose objects belong to C0;
• ÷ Γ is a finite set of condition-action rules.

A parametric action ↵ has the form a(~ p) : ¶e1↪ ▷ ▷ ▷ ↪ en♦, where: a is the action's name, ~ p are the input parameters, and ¶e1↪ ▷ ▷ ▷ ↪ en♦ is the finite set of conditional effects. Each effect ei has the formQi add F + i ↪ del F - i , where:

When the specific DL L is irrelevant, we omit it.

• ÷ Qi is the effect condition, i.e., an ECQ over T, whose terms can be action parameters ~ p (acting as variables), additional free variables ~xi, or objects from C0;

Given an action ↵ and a substitution ✓ assigning objects of C to ~ p, ↵✓ denotes the action instance of ↵ obtained by assigning values to ~ p according to ✓. We write ↵(~ p) to explicitly name the input parameters of ↵. The ABox resulting from the application of an action instance ↵✓ on an ABox A, denoted DO(↵✓↪ A↪ T ), is the ABox (A ∩ A-↵✓ ) [ A+↵✓ , where:

• ÷ F + i and F - i are two sets of atoms over the vocabulary of T , with terms from ~ p [ ~xi [ C0.
• ÷ A+↵✓ = Si2¶1↪▷▷▷↪n♦ Sσ2ANS(Qi✓↪T↪A) F + i σ;

Importantly, ↵✓ is applicable to A only if DO(↵✓↪A↪ T) is consistent with T .

• ÷ A-↵✓ = Si2¶1↪▷▷▷↪n♦ Sσ2ANS(Qi✓↪T↪A) F - i σ.

A condition-action rule (CA rule) γ↵ for an action ↵ has the form Q↵(~x) 7! ↵(~ p), where Q↵ is an ECQ mentioning only objects from C0 and whose free variables ~x come from ~ p. We assume that each action ↵ in ⇤ has exactly one corresponding condition-action rule γ↵ in Γ (multiple rules can be combined into a single disjunctive rule). The ECQ Q↵ is used to constrain the set of action instances potentially applicable to a certain Abox A. Specifically, let ✓ be a parameter substitution for ~ p, and let ✓[~x] denote the parameter substitution obtained by projecting ✓ on ~x. Then, ✓ is a K-legal parameter substitution in A for ↵, if:

• ÷ ✓ : ~ p ! C;
• ÷ DO(↵✓↪A↪ T) is T-consistent.
• ÷ ✓[~x] 2 ANS(Q↵↪ T↪A);

When this is the case, ↵✓ is a K-legal action instance in A. Any variable in ~ p ∩ ~x is also referred to as an external input parameter of ↵. Note that, when present, such parameters are not constrained by Q↵ and can be assigned to any object, including fresh ones not occurring in ADOM(A).

The semantics of eKABs is defined in terms of transition systems (TSs) with states and transitions labeled by ABoxes and action instances, respectively [Calvanese et al., 2013b]. A TS ⌥ is a tuple hC↪ T↪ ⌃↪ s0↪ abox ↪ !i, where:

• ÷ T is a TBox;
• ÷ C is the object domain;
• ÷ ⌃ is a (possibly infinite) set of states;
• ÷ abox is the labeling function, mapping states from⌃ into T -consistent ABoxes with terms from C only;
• ÷ s0 2 ⌃ is the initial state;
• ÷ ! ✓ ⌃ ⇥ L ⇥ ⌃ is a labeled transition relation, with L the (possibly infinite) set of labels.

We write s l-! s0 as a shortcut for hs↪ l↪ s0 i 2!. An eKAB K = hC↪ C0↪ T↪ A0↪ ⇤↪ Γi generates a TS ⌥K = hC↪ T↪ ⌃↪ s0↪ abox ↪ !i, where:

• ÷ s0 = A0;
• ÷ abox is the identity function;
• ÷ ! ✓ ⌃ ⇥ LK ⇥ ⌃ is a labelled transition relation with LK the set of all possible action instances;
• ÷ ⌃ and ! are defined by mutual induction as the smallest sets s.t. if A 2 ⌃, then for every K-legal action instance ↵✓ in A, we have that DO(↵✓↪A↪ T) 2 ⌃ and A ↵✓ --! DO(↵✓↪ A↪ T ).

In general, ⌥K is infinite, if C is so.

• ÷ Eng v Emp and Tech v Emp (engineers and technicians are employees);

Example 1. An eKAB K = hC↪ C0↪ T↪A0↪⇤↪ Γi is used to support decision making in a company, where employees work on tasks. C contains infinitely many objects. T is expressed in ALCQIH, and contains the following axioms:

• ÷ 9hasTask - v Emp and 9hasTask v Task (hasTask role links employees to tasks),
• ÷ similar axioms can be used to express that worksIn links employees to company branches;
• ÷ Emp v (= 1worksIn) (employees work in exactly one one branch);
• ÷ hasResp v ( 1Emp) and hasResp v hasTask - (a task may have at most one responsible, among the employees associated to the task);
• ÷ 9hasResp - v ≻Tech (technicians are not task responsible).

As for the dynamic aspects, to model that a new engineer can be hired in a branch provided that the planning agent does not know whether there already exists an engineer there, K contains the rule

Branch(b)^≻[9x▷Eng(x)^worksIn(x↪ b)] 7! HireEng(x↪ b) where:

A similar action HireTech(t↪ b) can be used to hire a technician. Rule

states that an employee can be made responsible of a task, where

removes the previous task responsible, if any, and makes the selected employee the new responsible. Finally, rule

models that an employee can be anonymized, where action

models anonymization by removing the explicit information on the branch to which the selected employee belongs.

Note that there is a complex interplay between the TBox and the dynamic component of K. E.g., the last TBox axioms forbids to hire a technician and make it responsible for a task. However, notice that this is not explicitly forbidden in the condition-action rule that defines the (potential) applicability of the MakeResp action.

4 eKAB planning

Let K be an eKAB and ⌥K its generated TS. A plan for K is a finite sequence ⇡ = ↵1✓1 · · · ↵n✓n of action instances over LK. The plan ⇡ is executable on K if there exists a (unique) run ⇢ = A0 ↵1✓1 ---! A1 ↵2✓2 ---! · · · ↵n✓n ---! An of K. We call ⇢ the run induced by ⇡, and An the final state of ⇢. An eKAB planning problem is a pair hK↪ Gi, with K an eKAB and G, the goal, a boolean ECQ mentioning only objects from C0. A plan ⇡ for K achieves G, if ANS(G↪An↪ T) = true, for An the final state of the run induced by ⇡.

Example 2. Given the eKAB in Example 1, a goal G could express the intention to have an engineer and a technician working for a given task t, provided that, for privacy reasons, it is not known to the planning agent whether the two work in the same branch. Formally:

where negation is in fact interpreted epistemically, in accordance with the semantics of ECQs.

We first consider plan existence, i.e., the problem of checking whether, for a planning problem hK↪Gi, an executable plan ⇡ for K exists that achieves G.

Theorem 4.1. Let L be a DL for which answering ECQs 2 is in CONP in data complexity. Then plan existence for LeKABs with a finite object domain is decidable in PSPACE in the size of the object domain.

2 For a significant class of DLs, UCQ-query answering is known to be in CONP in data complexity [Glimm et al., 2008; Ortiz et al., 2008; Calvanese et al., 2013a]. ECQs inherit this result, since they simply combine the certain answers returned by the embedded UCQs with the evaluation of the FO operators present in the query.

When the object domain is infinite, plan existence is undecidable even by considering severely limited eKABs. The following result is similar in spirit to the undecidability result by Erol et al. [1995] in the classical planning setting but with an infinite object domain. Also, a similar result was presented in [Zarrieß and Claßen, 2015], in a knowledge-based setting that is radically different from ours, since in their case the TBox is considered only in the initial state, while subsequent states may violate its assertions. This makes the proof technique significantly more complex in our case.

Theorem 4.2. Plan existence for eKABs with an infinite object domain is undecidable, even if the goal is a ground CQ, and the input eKAB has: (i) an empty TBox; (ii) actions/rules employing UCQs only.

We next attack undecidability by focusing on infinitedomain eKABs that are state-bounded [Bagheri Hariri et al., 2013a; Calvanese et al., 2013b; Belardinelli et al., 2014]. Specifically, an eKAB K is b-bounded if its generated TS ⌥K = hT↪⌃↪ s0↪ abox↪!i is s.t. for every state s 2 ⌃, we have ♣ADOM(abox(s))♣  b, that is, every state (or ABox) of ⌥K contains at most b distinct objects. Note that a b-bounded eKAB still has, in general, infinitely many states. Indeed, from an infinite C, one can obtain infinitely many distinct ABoxes, each containing a bounded number of objects.

For state-bounded eKABs, we have the following result, which follows from the verification results by Calvanese et al. [2013b]. The result implies that, for state-bounded eKABs, checking plan existence is not more difficult than in the standard setting of propositional planning [Bylander, 1994].

Theorem 4.3. Plan existence over state b-bounded eKABs is decidable in PSPACE in the bound b.

We observe that while boundedness is undecidable in general (by reduction to checking whether a Turing Machine uses a bounded number of cells on a given input), checking whether an eKAB is bounded for a given bound is decidable, as proven in [De Giacomo et al., 2014], although in the Situation Calculus framework.

5 Plan Synthesis

We now consider plan synthesis for eKABs. We first introduce a technique based on classical planning [Brachman and Levesque, 2003]. A classical planning domain is a triple D = hS↪A↪ ⇢i, where S is a finite set of states, A is a finite set of actions, and ⇢ : S ⇥ A ! S is a transition function. Domain states are propositional assignments, and actions are operators that change them, according to ⇢. A classical planning problem is a triple P = hD↪ s0↪Gi, where D is a planning domain, s0 2 S is the initial state, and G ✓ S is a set of goal states. A solution to P is a finite sequence of actions, called plan, that takes D from s0 to a goal state, as a result of the changes made by the sequence of actions.

A problem P induces a labelled graph G = hN↪ Ei, where N = S and E contains a (labelled) edge s a! s0 iff s0 = ⇢(s↪ a). Essentially, planning algorithms amount to searching (in an effective way) a path in G from s0 to a goal state.

Algorithm 1 Forward planning algorithm schema

1: function FINDPLAN(Prob) 2: input: A planning problemProb 3: output: A plan that solves Prob, or fail if there is no solution 4: V := ; . Global set of visited states 5: return FWSEARCH(Prob,INITIALSTATE(Prob),✏) 6: function FWSEARCH(Prob↪ s↪ ⇡) 7: input: A planning problem Prob, the current state s, and the sequence ⇡ of actions that led to s 8: output: A plan that solves Prob, or fail if there is no solution 9: if s 2 V then return fail . Loop! 10: V := V [ ¶s♦ 11: if HOLDS(GOAL(Prob)↪ s) then return ⇡ 12: for all ha↪ s 0 i 2 SUCCESSORS(Prob↪ s) do 13: ⇡n := FWSEARCH(Prob↪ s 0 ↪ ⇡ · a) 14: if ⇡n 6= fail then return ⇡n 15: return fail

Algorithm 1 shows the schema of a basic algorithm that synthesizes a plan through a forward search on the induced graph. The auxiliary functions INITIALSTATE(Prob), GOAL(Prob), HOLDS(G↪ s), and SUCCESSORS(Prob↪ s) are self-explicative. Note that the schema above abstracts from the specific interpretation of states, that is, it is applicable no matter how states and actions are represented, once the functions above are instantiated on the case at hand. For instance, for a classical planning problem P = hD↪ s0↪Gi with D = hS↪A↪ ⇢i, we have INITIALSTATE(P) = s0, GOAL(P) = G, HOLDS(G↪ s) = true iff s 2 G, and SUCCESSORS(P↪ s) = ¶ha↪ s0 i ♣ s0 = ⇢(s↪ a)♦.

Next, we show how this schema can be lifted to handle plan synthesis for eKABs. The lifting we propose results in an algorithm that is correct, i.e., it

• (i) terminates,
• (ii) preserves plan existence, and
• (iii) produces proper plans, i.e., if it does not fail, the returned result corresponds to a proper solution to the input planning problem.

We stress that while we present the lifting on Algorithm 1, the same approach applies to any other, possibly optimized, algorithm. Indeed, the lifting strategy is agnostic wrt how the search space is traversed.

5.1 Plan Synthesis for eKABs

We consider the two classes of eKABs for which decidability of plan existence has been established in Section 4.

eKABs with Finite Domain. This case differs from classical planning in that eKABs have ABoxes as states, and they provide an implicit representation of successor states in terms of actions and condition-action rules. The former aspect requires to replace propositional entailment with ECQ query answering when checking whether the goal has been reached. The latter requires to use DO to compute a state's successors. Specifically, given an eKAB planning problem E = hK↪Gi, where K = hC↪ C0↪ T↪ A0↪ ⇤↪ Γi, with finite C, Algorithm 1 can be instantiated as follows:

• ÷ INITIALSTATE(E) = A0;

Algorithm 2 Plan synthesis for state-bounded eKABs.

• 1: function FINDPLAN-EKABSB(E↪ b)
• 3: output: A plan that solves E, or fail if there is no solution
• 2: input: An eKAB planning problem E = hK↪Gi, where K = hC↪ C0↪ T↪ A0↪ ⇤↪ Γi is b-bounded and C is infinite
• 4: n :=max¶k ♣ there is ↵ 2 ⇤with k parameters♦
• 5: pick b C s.t. (C0 ✓ b C ⇢ C ♣ b C♣ = b + n + ♣C0♣ . Abstract dom. 6: bK := hb C↪ C0↪ T↪ A0↪ ⇤↪ Γi 7: return FINDPLAN-EKABFD(h bK↪ Gi)
• ÷ GOAL(E) = G;
• ÷ SUCCESSORS(E↪A) returns the set of pairs h↵✓↪A0 i, where
• ÷ HOLDS(E↪A) = ANS(G↪ T↪A);
• ↵ 2 ⇤,
• A0 = DO(↵✓↪A↪ T).
• ✓ is a K-legal parameter substitution in A for ↵, and

We call the resulting algorithm FINDPLAN-EKABFD. By this instantiation, the search space of FINDPLAN-EKABFD is exactly ⌥K, which is finite, so being the eKAB domain. Thus, we have:

Theorem 5.1. FINDPLAN-EKABFD is correct.

Plan Synthesis for State-Bounded eKABs. We now consider state-bounded eKABs over infinite object domains. In this case, the search space is potentially infinite, thus FINDPLAN-EKABFD is not readily applicable, as termination is not guaranteed. To tackle this problem, instead of visiting the original, infinite, search space, we work on a finitestate abstraction of the eKAB. We first argue that the execution semantics of eKABs has two properties:

• ÷ it is driven by ECQ-query answering, which is generic (cf. Section 2);
• ÷ all allowed configurations of external input parameters are considered when applying an action.

These imply that eKABs are generic DLDSs in the sense of Calvanese et al. [2013b], which, together with stateboundedness, allows us to apply the same abstraction technique used by Calvanese et al. [2013b]. In particular, reachability is preserved if the infinite-state TS induced by the input eKAB is shrunk into a finite-state TS over a finite, but sufficiently large, object domain. We leverage this technique as the core of the FINDPLAN-EKABSB procedure shown in Algorithm 2, which reduces the original planning problem over an infinite search space to a classical planning problem.

It can be checked that all correctness conditions are satisfied: (i) is a consequence of Theorem 5.1; (ii) holds because the finite-state abstraction preserves reachability; (iii) holds because the search space of the finite-state abstraction is contained into that of the original eKAB. Thus, we have:

Theorem 5.2. FINDPLAN-EKABSB is correct.

Example 3. Consider again the eKAB K in Example 1, together with goal G in Example 2. Notice that K is statebounded, as the only way to increase the number of objects present in the system is by hiring someone, but the number of hirings is in turn bounded by the number of company branches (which is fixed once and for all in the initial state). Now assume that the initial state indicates the known existence of a main and a subsidiary branch for the company, as well as the fact that task t has an assigned technician from the main branch:

A possible plan leading from A0 to a state where G holds is

This plan achieves G by hiring an engineer in a different branch from that of 123, with whom the engineer shares task t. Observe, again, the interplay between the actions and the TBox: while no action explicitly indicates that 452 has task t, this is implicitly obtained from the fact that such an engineer is made responsible for t.

Another, quite interesting plan achieving G is:

• ⇡2 = HireEng(521↪ main) MakeResp(t↪ 521) Anon(521)

In this case, an engineer is hired in the same branch of technician 123, and made responsible for task t. These two actions do not suffice to achieve G, since the planning agent knows that the two employees work in the same branch. This knowledge is somehow "retracted" by anonymizing the hired engineer: after the execution of Anon(521), the planning agent still knows that 521 must work in some branch (this is enforced by a dedicated TBox axiom), but does not know which one, thus satisfying also the (epistemic) negative part of the goal.

5.2 Plan Templates and Online Instantiation

FINDPLAN-EKABSB returns plans with ground actions mentioning only objects in b C, as those in C ∩ b C are not used in bK. Such plans can be regarded as templates from which we can obtain regular plans for K. This is a consequence of genericity, which yields that a plan keeps achieving a goal even under consistent renaming of the objects it mentions.

To formalize this intuition, we recast the notion of equality commitment [Calvanese et al., 2013b] in this setting. Let B be a set of objects, and I a set of external input parameters. An equality commitment (EC) H over a finite set S ✓ B[I is a partition ¶H1↪ ▷ ▷ ▷ ↪Hn♦ of S s.t. each Hj contains at most one object from B. A substitution ✓ : I ! B is compatible with H if:

• ÷ for every pair of parameters i1↪ i2 2 I, we have that i1✓ = i2✓ iff i1 and i2 belong to the same Hj;
• ÷ whenever Hj contains an object d 2 B, then i✓ = d for every i 2 Hj .

Intuitively, ✓ is compatible with H if it maps parameters from the same class into the same object, and parameters from different classes into distinct objects. Finally, given a finite set B0 ⇢ B and a substitution ✓ : I ! B, fix an ordering O = hd1↪ ▷ ▷ ▷ ↪ dni over the set Bcur = B0 [ IM(✓) of the objects that are either mentioned in B0 or assigned to I by ✓. The EC H induced by ✓ over B0 (under O) is the partition H = ¶H1↪ ▷ ▷ ▷ ↪Hn♦, s.t., for j 2 ¶1↪ ▷ ▷ ▷ ↪ n♦:

Algorithm 3 Online instantiation of a plan template.

1: procedure ONLINEEXEC(K↪ ⇡) 2: input: An eKAB K = hC↪ C0↪ T↪A0↪⇤↪ Γi, and a plan ⇡ = ↵1✓1 · · · ↵m✓m 3: Ao := A0 . old, effective state 4: An := A0 . current, effective state 5: h : C0 ! C0 s.t. h(d) = d for each d 2 C0 . cur. bijection 6: for k 2 ¶1↪ ▷ ▷ ▷ ↪m♦ do 7: H := eq. commitment induced by ✓i over ADOM(A) 8: pick ✓0k that is compatible with h(H) . Agent choice 9: A0o := DO(↵i✓k↪Ao↪ T) 10: A0n := DO(↵i✓0k↪An↪ T) 11: hn : C0 [ ADOM(Ao) ! C0 [ ADOM(An) s.t. 12: 8><>: hn(d) = d↪ for d 2 C0 hn(d) = h(d)↪ for d 2 ADOM(A0o) \ ADOM(Ao) hn(✓k(i)) = ✓0k (i)↪ for i parameter of ↵k s.t. ✓k(i) ◁2 ADOM(Ao) 13: h := hn, Ao := A0o, An := A0n

• ÷ Hj contains dj iff dj 2 B0 , i.e., objects mentioned by ✓ but not present in B0 are discarded;
• ÷ Hj contains i 2 DOM(✓) iff ✓(i) = dj, i.e., all parameters mapped to the same, j-th object are included in the j-th equivalence class.

Example 4. Let B = ¶d1 ▷ ▷ ▷ ↪ d5♦, B0 = ¶d1↪ d2↪ d3♦, I = ¶i1↪ ▷ ▷ ▷ ↪ i4♦, and ✓ : I ! B, s.t.: ✓(i1) = d1↪ ✓(i2) = ✓(i3) = d5↪ ✓(i4) = d4. The EC induced by ✓ over B [ ¶d4↪ d5♦ is H = ¶H1↪ ▷ ▷ ▷ ↪H5♦, where: H1 = ¶d1↪ i1♦↪H2 = ¶d2♦↪H3 = ¶d3♦↪H4 = ¶i4♦↪H5 = ¶i2↪ i3♦. Notice that Hi ✓ B.

We can now state the following key result.

Lemma 5.3. Let K = hC↪ C0↪ T↪ A0↪ ⇤↪ Γi be an eKAB, and A1↪A01 ABoxes over T, s.t. A1 ⇠=hT A01 for some object renaming h. Let ↵(~ p↪~i) be an action in ⇤ with external input parameters~i, and ✓ a K-legal substitution in A1 for ↵. Let H be the equality commitment induced by ✓ over ADOM(A1), and H0 = h(H) the equality commitment obtained from H by renaming each d 2 ADOM(A1) as h(d) 2 ADOM(A2). If ✓0 is a parameter substitution for ~ p and~i compatible with H0 , then:

• ÷ ✓0 is a K-legal parameter for ↵ in A01 ;
• ÷ DO(↵✓↪A1↪ T) ⇠=h0 T DO(↵✓0 ↪A01 ↪ T), where h0 extends h as follows: for every parameter i of ↵ s.t. ✓(i) 62 ADOM(A1), we have h0 (✓(i)) = ✓0 (i).

Intuitively, Lemma 5.3 states that, modulo object renaming consistent with a parameter substitution that induces the same equality commitment, the same action can be applied to two logically equivalent ABoxes. Furthermore, such action induces the same update, modulo renaming of the objects mentioned in the two ABoxes and the involved parameters. In Algorithm 3, we exploit this result to build, in an online fashion, a plan for K starting from one for bK. This provides the freedom of dynamically choosing which actual objects to use when actions are executed, provided that the choice induces the same equality commitment induced by the parameter substitution in the original plan. By Lemma 5.3, we obtain:

Theorem 5.4. Let E = hK↪Gi be an eKAB planning problem. If ⇡ is a plan that achieves G, then ONLINEEXEC(K↪ ⇡) is guaranteed to achieve G for each possible choice.

Example 5. Consider plan ⇡2 of Example 3. This plan can be lifted online by the planning agent as follows: when hiring the engineer, the planning agent can freely inject a fresh employee identifier in place of 521, provided that the chosen identifier is then consistently used in the subsequent actions. In other words, ⇡2 acts as a footprint for the infinite family of plans of the form

HireEng(Id ↪ main) MakeResp(t↪ Id ) Anon(Id )

where Id is selected on-the-fly when the planning agent executes HireEng, and is s.t. it is different from all the objects present in A0 (this reconstructs the same equality commitment as in the case of 521). All such infinite plans are guaranteed to achieve G.

6 Plan Synthesis for Lightweight eKABs

We consider plan synthesis for state-bounded eKABs over the lightweight DL DL-LiteA [Calvanese et al., 2009], and devise a technique based on compilation into ADL planning [Pednault, 1994; Drescher and Thielscher, 2008].

6.1 ADL Planning

An ADL planning problem is a tuple hC↪ C0↪F↪A↪ '↪ i, where:

• ÷ C is a finite object domain;
• ÷ F is a finite set of fluents, i.e., predicates whose extension can vary over time;
• ÷ C0 ✓ C is the set of initial objects;
• ÷ A is a finite set of ADL operators;
• ÷ is the goal description, i.e., a closed FO formula using predicates in F and objects in C0.
• ÷ ' is the initial state, i.e., a conjunction of ground literals using predicates in F and objects in C0; and

Each ADL operator in A is a tuple hN↪ ~x↪ ⇢(~x)↪ "(~x)i, where:

• ÷ variables ~x are the parameters;
• ÷ N is the name;
• ÷ ⇢(~x) is the precondition, i.e., a FO formula over F, and whose terms are quantified variables, objects in C0, and parameters ~x;
• ÷ "(~x) is the effect, i.e., the universal closure of a FO conjunction built from admissible components, inductively defined as follows:
• Fluent literals over F and whose terms are variables, objects in C0, or parameters in ~x, are admissible.
• If φ1(~y1) and φ2(~ y2) are admissible, then φ1(~y1) ^ φ2(~y2) and 8~y1▷φ1(~y1) are also admissible.
• Let φ1(~y1) be a FO formula over F, whose terms are quantified variables, objects in C0, variables ~ y1, or parameters ~x. If φ2(~y2) is admissible and does not contain any occurrence of ! nor 8, then φ1(~y1) ! φ2(~y2) is also admissible. This is used to tackle so-called ADL conditional effects.

6.2 Translation Procedure

We now define a syntactic, modular translation procedure LEKAB2ADL that takes as input a DL-LiteA-eKAB planning problem E = hK↪Gi with K = hC↪ C0↪ T↪A0↪⇤↪ Γi, and produces a corresponding ADL planning problem PK = hCK↪ C0↪FK↪AK↪ 'K↪ Gi.

Fluents. FK is obtained by encoding concept and role names in T into corresponding unary and binary fluents. It also contains two special nullary fluents: ChkCons, distinguishing normal execution modality from check consistency modality of PK, and Error , marking when the consistency check fails.

Object domain. As in Section 5, if C is finite, so is CK. If instead C is infinite but K is b-bounded, we fix CK to contain C0 plus n + b objects from C.

Operators. AK is obtained by transforming every action in ⇤, with its condition-action rule in Γ, into an ADL operator: each action's effect produces a conditional effect in the ADL operator, and the condition-action rule its precondition.

Since in ADL, FO formulae are directly evaluated over FO structures (without ontological reasoning), we have to suitably consider the contribution of T . Indeed (cf. Section 3), T is used both during query answering and to check whether the ABox resulting from an action instance is T-consistent. We tackle both problems by relying on DL-LiteA's FO rewritability of both ECQs and T -consistency checks (cf. Section 2). To embed such checks into ADL, we force AK to alternate between two phases: the normal execution modality, where a "normal" ADL operator is applied, mirroring the execution of an action instance of K; and the check consistency modality, where a special ADL operator checks if the obtained state is T-consistent. Alternation is realized by toggling the fluent ChkCons, and activating Error when the consistency check fails, thus blocking operator application.

Technically, consider an action ↵ = a(~ p) : ¶e1↪ ▷ ▷ ▷ ↪ en♦ in ⇤ and its corresponding condition-action rule Q↵(~x) 7! a(~ p) in Γ. Let ~z = ~ p ∩ ~x. We produce a corresponding ADL operator ha↪ ~ p↪ ⇢↵(~ p)↪ "↵(~ p)i. Its precondition ⇢↵(~ p) corresponds to the FO formula rew(Q↵(~x)↪ T ) ^ ≻ChkCons ^ ≻Error , which leaves the external input parameters ~z unconstrained. The operator effect "↵(~ p) is the FO conjunction of the translation of e1↪ ▷ ▷ ▷ ↪ en. Each ei = Qi(~ p↪ ~xi) addF + i ↪ del F - i generates the following conjunct:

Finally, the special ADL operator used to check Tconsistency is hcheck↪ ;↪ ⇢chk↪ "chki, where ⇢chk = ChkCons just checks whether the check flag is on, while "chk takes care of toggling the check flag, as well as of triggering the error flag if an inconsistency is detected:

Initial state specification. 'K is by constructing the con-

junction of all facts contained in A0: 'K = VPi(~o)2A0 Pi(~o). Goal description. The goal description G is obtained from goal G in E as G = rew(G↪ T) ^≻ChkCons ^≻Error.

The two-fold contribution of T is taken care of, as in the operators, by rewriting G (via rew(G↪ T)) and ensuring that the ending state is T-consistent (by requiring the absence of the consistency check and error flags in G).

We close by considering the following algorithm, called FINDPLAN-LEKABADL:

1. take as input a DL-LiteA-eKAB planning problem E;
2. translate E into an ADL planning problem using LEKAB2ADL;
3. invoke an off-the-shelf ADL planner;
4. if the planner returns fail, return fail as well;
5. if the planner returns a plan ⇡, filter away all check operators from ⇡, and return it as a result.

Theorem 6.1. FINDPLAN-LEKABADL is correct.

7 Conclusion

We have studied plan synthesis over eKABs, rich dynamic systems operating over a full-fledged DL KB. We have shown that checking plan existence is undecidable even under severe restrictions on the eKAB of interest. Nonetheless, we have demonstrated that, under the state-boundedness assumption for eKABs, plan existence is PSPACE in data complexity. In this setting, we have presented sound, complete and terminating algorithms for plan synthesis. We have then studied plan synthesis in the case where the eKAB is equipped with a lightweight DL of the DL-Lite family. In particular, we have proposed a technique to compile plan synthesis for statebounded, lightweight eKABs into standard ADL planning.

To test the feasibility of our proposal for knowledgeintensive planning, we ran a preliminary empirical evaluation of the framework of Section 6. We considered a DL-LiteAeKAB over the domain of Example 1, translated it into ADL, and fed it as input via PDDL to an off-the-shelf planner (we used FastDownward 3 ). We varied the difficulty by increasing the bound on the object domain, thus affecting the number of ground atoms for the planner. With 9 domain elements, resulting in ⇠2 000 atoms, a plan was found in under 1s. For 30 elements (⇠300 000 atoms) a plan was found in 120s, while for 35 elements (⇠1200000 atoms) the planner timed out. Although preliminary, we consider these results positive, given the complexity of the setting and the absence of optimizations, which we left for future work. In this respect, a promising line of research is to combine our approach with that of [Fan et al., 2012]. There, the authors study a knowledgeintensive variant of Golog operating over an infinite object domain, and where incomplete knowledge is captured using proper KBs instead of DLs. In particular, they propose a semidecidable technique to handle progression and query evaluation. In spite of the key differences between that approach and ours, their approach is reminiscent to the abstraction technique we adopt towards decidability. We intend to leverage this similarity with the aim of understanding if, and how, the optimization strategies proposed in [Fan et al., 2012] can be lifted to our setting.

3 http://www.fast-downward.org/