Synthesizing and Executing Plans in Knowledge and Action Bases? ??

Abstract

We study plan synthesis for a variant of Knowledge and Action Bases (KABs). KABs have been recently introduced as a rich, dynamic framework where states are full-fledged description logic (DL) knowledge bases (KBs) whose extensional part is manipulated by actions that can introduce new objects from an infinite domain. We show that, in general, plan existence over KABs is undecidable even under severe restrictions. We then focus on the class of statebounded KABs, for which plan existence is decidable, and we provide sound and complete plan synthesis algorithms, through a novel combination of techniques based on standard planning, DL query answering, and finite-state abstractions. All results hold for any DL with decidable query answering. We finally show that for lightweight DLs, plan synthesis can be compiled into standard ADL planning.

Introduction

Recently, there has been an increasing interest in the study of formalisms that integrate static structural knowledge, as expressed, e.g., in description logics (DLs) [ 2 ], with action-based mechanisms, to capture a domain’s evolution over time. Combining these two aspects into a single logical system is well-known to be difficult and easily leading to undecidability, even for simple forms of inference about system dynamics, when the logics used to describe the structural properties are rather limited [ 25, 17 ]. To overcome these restrictions, a recent line of work by [ 5 ] has introduced Knowledge and Action Bases (KABs). Such systems rely on Levesque’s functional approach [21] 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).

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 ? A revised version of this work has been published in the Proceedings of IJCAI 2016. ?? The authors acknowledge the support of: Rip. Diritto allo Studio, Universita` e Ricerca Scientifica of Provincia Autonoma di Bolzano–Alto Adige, under project VERISYNCOPATED; the EU project Optique (FP7-IP-318338); and the UNIBZ internal projects KENDO and OnProm. KABs that are state-bounded [ 3, 4 ], 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 [ 18, 14 ], 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) [ 13 ], and inherit its possibility of abstracting away the specific DL formalism used to capture the underlying KB.

We show that, in general, plan existence is undecidable even for severely restricted eKABs, in line with previous work on planning in rich settings [ 16 ]. We then prove decidability in PSPACE data complexity of such problem, for state-bounded eKABs, by combining techniques based on standard planning, DL query answering, and finitestate abstractions for DLDSs. In spirit, our work is similar to the one by [ 20 ], since it combines a rich knowledge-based setting with the possibility of incorporating external input during the system evolution. However, we provide the first setting we are aware of where planning stays decidable without imposing severe restrictions, in particular on how external input is handled. Additionally, we present a sound and complete plan synthesis algorithm. Notably, the plans it returns represent plan templates for the original synthesis problem, which is over an infinite domain. We then concentrate on eKABs based on lightweight DLs of the DL-Lite family [ 11, 9 ], 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 [24]. 2

Description Logic Knowledge Bases

Let be a countably infinite universe of objects, acting as standard names [22]. A (DL) knowledge base (KB) hT ; Ai consists of a TBox T , capturing the intensional knowledge about 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 [ 2 ]. 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 j= , if every model of hT ; Ai is also a model of . Two ABoxes A1 and A2 are logically equivalent modulo renaming w.r.t. 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 9yi.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. 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 ECQ [ 10 ], the extension of UCQs defined as:

Q ::= [q] j :Q j Q1 ^ Q2 j 9x.Q; 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 [ 10 ]. Under this semantics, ECQs are generic, in the classical sense of [ 1 ]: a query evaluated over two logically equivalent ABoxes returns the same answer modulo object renaming.

As customary, we consider only DLs for which query answering (and hence the standard reasoning tasks of KB satisfiability and logical implication) is decidable. In our examples, we use the standard DL ALCQIH [ 2 ]. We also consider lightweight DLs of the DL-Lite family, in particular DL-LiteA [ 9 ], for which both checking KB satisfiability and answering ECQs over a KB are FO-rewritable [ 10, 9 ]. 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 ) such that, for every ABox A, the certain answers ANS(Q; T; A) can be computed by directly evaluating rew (Q; T ) over A seen as a database under the closed-world assumption. Also, T -consistency of A can be checked by evaluating over A an ECQ QuTnsat (that depends on T only). 3

Explicit-input Knowledge and Action Bases

We define Explicit-input Knowledge and Action Bases (eKABs) parametrically w.r.t. a DL L. An L-eKAB K is a tuple hC; C0; T; A0; ; i, where: (i) C is the (possibly infinite) object domain of K; (ii) C0 C is a finite set of distinguished objects; (iii) T is an L-TBox; (iv) A0 is an L-ABox all of whose objects belong to C0; (v) is a finite set of parametric actions; (vi) is a finite set of condition-action rules. When the specific DL L is irrelevant, we omit it. We detail the latter two items below.

A parametric action has the form a(p) : fe1; : : : ; eng, where: a is the action’s name, p are the input parameters, and fe1; : : : ; eng is the finite set of conditional effects. Each effect ei has the form Qi add Fi+; del Fi , where: (i) 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; (ii) Fi+ and Fi are two sets of atoms over the vocabulary of T , with terms from p [ xi [ 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 n A ) [ A+ , where: (i) A+ = Si2f1;:::;ng S 2ANS(Qi ;T;A) Fi+ ; (ii) A = Si2f1;:::;ng S 2ANS(Qi ;T;A) Fi . Importantly, is applicable to A only if DO( ; A; T ) is consistent with T .

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 conditionaction 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: (i) : p ! C; (ii) [x] 2 ANS(Q ; T ; A); and (iii) DO( ; A; T ) is T -consistent. When this is the case, is a K-legal action instance in A. Any variable in p n 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 resp. labeled by ABoxes and action instances [ 13 ]. A TS is a tuple hC; T ; ; s0; abox ; !i, where: (i) C is the object domain; (ii) T is a TBox; (iii) is a (possibly infinite) set of states; (iv) s0 2 is the initial state; (v) abox is the labeling function, mapping states from into T -consistent ABoxes with terms from C only; (vi) ! L is a labeled transition relation, with L the (possibly infinite) set of labels. An eKAB K = hC; C0; T ; A0; ; i generates a TS

K = hC; T ; ; s0; abox ; !i, where: (i) abox is the identity function; (ii) s0 = A0; (iii) ! LK is a labelled transition relation with LK the set of all possible action instances; (iv) 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 ; A; T ). In general,

! DO( K is infinite, if C is so.

Example 1. Consider an eKAB K = hC; C0; T ; A0; ; i used to support decision making in a company, where employees work on tasks. C contains infinitely many objects. The TBox T is expressed in ALCQIH, and contains the following axioms: Eng v Emp and Tech v Emp indicate that engineers and technicians are employees. 9hasTask v Emp and 9hasTask v Task type the hasTask role, which links employees to tasks. Similar axioms can be used to express that worksIn links employees to branches of the company. Emp v (= 1 worksIn) states that employees work in one and only one branch. hasResp v ( 1 Emp) and hasResp v hasTask indicate that a task may have at most one responsible, among those employees associated to that task. Finally, 9hasResp v :Tech states that technicians cannot be responsible for tasks.

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 has rule

Branch(b) ^ :[9x:Eng (x) ^ worksIn(x; b)] 7! HireEng(x; b); where: HireEng(e; b) : ftrue add fEng (e); worksIn(e; b)gg. A similar action HireTech(t; b) can be used to hire a technician. Rule Task (t) ^ Emp(e) 7! MakeResp(t; e) states that an employee can be made responsible of a task, where

MakeResp(t; e) : hasResp(t; prteruve) addeldffhhaassRReesspp((tt;;per)egv)g removes the previous responsible of the selected task if there existed one, and makes the selected employee the new responsible. Finally, rule Emp(e) 7! Anon(e) models that an employee can be anonymized, where action Anon(e) : fworksIn(e; b) delfworksIn(e; b)gg 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 . A 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: 9e1; e2:Tech(e1) ^ Eng(e2) ^ hasTask (e1; t) ^ hasTask (e2; t)

^ :[9b:worksIn(e1; b) ^ worksIn(e2; b)] 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 1. Let L be a DL for which answering ECQs3 is in CONP in data complexity. Then plan existence for L-eKABs with a finite object domain is decidable in PSPACE in the size of the object domain.

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

We observe that the latter result is similar in spirit to an undecidability result by [ 16 ] for the propositional case, but cannot be derived from it, and required a separate proof.

Next, we attack this undecidability result. To do so, we focus on a class of infinitedomain eKABs that enjoy the property of state-boundedness [ 3, 13, 6 ]. Specifically, an eKAB K is b-bounded if its generated TS K = h T; ; s0; abox ; !i is such that for every state s 2 , we have jADOM(abox (s))j 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, by applying [ 13 ] we get that checking plan existence is not more difficult than in the standard setting of propositional planning [ 8 ]. Theorem 3. Plan existence over state b-bounded eKABs is decidable in PSPACE in b. 3 For a significant class of DLs, UCQ-query answering is known to be in CONP in data complexity [ 19, 23, 12 ]. 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. Algorithm 1 Forward planning algorithm schema

Plan Synthesis

We now focus on plan synthesis for eKABs. We first introduce a technique based on classical planning [ 7 ]. 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) for a path in G from s0 to a goal state. 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. In other words, it is applicable independently of the specific form of states and actions, once the functions above are instantiated on the case at hand. For instance, for classical planning problems 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) = fha; s0i j s0 = (s; a)g.

Next, we show how this schema can be used for eKABs plan synthesis. Our proposal results in an algorithm that is correct, i.e., that (i) terminates, (ii) preserves plan existence, and (iii) produces proper plans, i.e., if it does not fail, the output 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 to the search space traversal fashion. Algorithm 2 Plan synthesis for state-bounded eKABs. 1: function FINDPLAN-EKABSB(E; b) 2: input: An eKAB planning problem E = hK; Gi, where K = hC; C0; T; A0; ; i is bbounded and C is infinite 3: output: A plan that solves E, or fail if there is no solution 4: n := maxfk j th(ere is 2 with k parametersg 5: pick Cb such that C0 Cb C . Abstract dom.

jCbj = b + n + jC0j 6: 7:

Kb := hCb; C0; T; A0; ; i return FINDPLAN-EKABFD(hKb; Gi) 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: (i) INITIALSTATE(E ) = A0; (ii) GOAL(E ) = G; (iii) HOLDS(E ; A) = ANS(G; T; A); (iv) SUCCESSORS(E ; A) returns the set of pairs h ; A0i, where (a) 2 , (b) is a K-legal parameter substitution in A for , and (c) A0 = DO( ; A; T ). 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 4. FINDPLAN-EKABFD terminates and is sound and complete.

Plan Synthesis for State-Bounded eKABs. We now consider state-bounded eKABs

over an infinite object domain. In this case, the search space is potentially infinite. Thus, FINDPLAN-EKABFD is not readily applicable anymore, as termination is not guaranteed. To tackle this problem, instead of visiting the original, infinite, search space, we work on a finite-state abstraction of the eKAB. We first argue that the execution semantics of eKABs has two properties: (i) it is driven by ECQ-query answering, which is generic (cf. Section 2); (ii) all allowed configurations of external input parameters are considered when applying an action. These imply that eKABs are generic DLDSs in the sense of [ 13 ], which, together with state-boundedness, allows us to apply the same abstraction technique used by [ 13 ]. 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 4; (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. FINDPLAN-EKABSB terminates and is sound and complete. Example 3. Consider again the eKAB K in Example 1, together with goal G in Example 2. Notice that K is state-bounded, 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: A0 = fBranch(main), Branch(sub), Tech(123), worksIn(123, main), hasTask (123, t)g.

A possible plan leading from A0 to a state where G holds is 1 = HireEng(452; sub) MakeResp(t; 452). 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 Cb, as objects from C n Cb are not used in Kb. Such plans can be regarded as plan templates from which we can obtain regular plans for K. This comes as a consequence of genericity, which, intuitively, implies that a plan keeps achieving a goal even if the objects mentioned in its actions are consistently renamed.

To formalize this intuition, we recast the notion of equality commitment [ 13 ] 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 fH1; : : : ; Hng of S s.t. each Hj contains at most one object from B. A substitution : I ! B is compatible with H if: (i) for every pair of parameters i1; i2 2 I , we have that i1 = i2 iff i1 and i2 belong to the same Hj ; and (ii) 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 = fH1; : : : ; Hng, s.t., for j 2 f1; : : : ; ng: (i) Hj contains dj iff dj 2 B0, i.e., objects mentioned by but not present in B0 are discarded; (ii) 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.

We can now state the following key result.

Algorithm 3 Online instantiation of a previously returned plan template. 12: 13: 1: procedure ONLINEEXEC(K; ) 2: input: An eKAB K = hC; C0; T; A0; ; i, and a plan = 1 1 3: Ao := A0 4: An := A0 5: h : C0 ! C0 s.t. h(d) = d for each d 2 C0 6: for k 2 f1; : : : ; mg do 7: H := eq. commitment induced by i over ADOM(A) 8: pick k0 that is compatible with h(H) 9: A0o := DO( i k; Ao; T ) 10: A0n := DO( i k0; An; T ) 11: hn : C0 [ ADOM(Ao) ! C0 [ ADOM(An) s.t.

>8hn(d) = d; for d 2 C0 >><hn(d) = h(d); for d 2 ADOM(A0o) \ ADOM(Ao) >>hn( k(i)) = k0(i); for i param. of k > :

s.t. k(i) 2= ADOM(Ao) h := hn, Ao := A0o, An := A0n m m . old, effective state . current, effective state . cur. bijection . Agent choice Lemma 1. Let K = hC; C0; T; A0; ; i be a eKAB, and A1; A01 two ABoxes over T such that 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) with h(d) 2 ADOM(A2). If 0 is a parameter substitution for p and i compatible with H0, then: (i) 0 is a K-legal parameter for in A01; (ii) DO( ; A1; T ) =hT0 DO( 0; A01; T ), where h0 extends h in such a way that for every parameter i of , if (i) 62 ADOM(A1), then h0( (i)) = 0(i).

Intuitively, Lemma 1 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 Kb. 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 1, we obtain: Theorem 6. 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 4. 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 blueprint 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 such that 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 [ 9 ], and devise a technique based on compilation into ADL planning [ 24, 15 ]. An ADL planning problem is a tuple hC; C0; F ; A; '; i, where: (i) C is a finite object domain; (ii) C0 C is the set of initial objects; (iii) F is a finite set of fluents, i.e., predicates whose extension can vary over time; (iv) A is a finite set of ADL operators; (v) ' is the initial state, i.e., a conjunction of ground literals using predicates in F and objects in C0; and (vi) is the goal description, i.e., a closed FO formula using predicates in F and objects in C0. Each ADL operator in A is a tuple hN; x; (x); "(x)i, where: (i) N is the name; (ii) variables x are the parameters; (iii) (x) is the precondition, i.e., a FO formula over F , and whose terms are quantified variables, objects in C0, and parameters x; (iv) "(x) is the effect, i.e., the universal closure of a FO conjunction built from admissible components, inductively defined as follows: (a) fluent literals over F whose terms are variables, objects in C0, or parameters in x, are admissible; (b) if 1(y1) and 2(y2) are admissible, then 1(y1) ^ 2(y2) and 8y1: 1(y1) are also admissible; (c) given a FO formula 1(y1) 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).

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.

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.

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.

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) : fe1; : : : ; eng in and its corresponding condition-action rule Q (x) 7! a(p) in . Let z = p n 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) add Fi+; del Fi generates the conjunct: rew (Qi(p; xi); T ) ! ^Pj (p; xi) ^ ^:Pk(p; xi) ^ ChkCons

Pj(p;xi)2Fi+ Pk(p;xi)2Fi Finally, the special ADL operator used to check T -consistency is hcheck ; ;; chk; "chki, where chk = ChkCons, just checks whether the check flag is on, while "chk takes care of toggling the flag, as well as of triggering the error flag if an inconsistency is detected: "chk = :ChkCons ^ (QuTnsat ! Error ) Initial state specification. 'K is by constructing the conjunction 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, 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: (i) take as input a DL-LiteA-eKAB planning problem E ; (ii) translate E into an ADL planning problem using LEKAB2ADL; (iii) invoke an off-the-shelf ADL planner; (iv) if the planner returns fail, return fail as well; (v) if the planner returns a plan , filter away all check operators from , and return it as a result.

Theorem 7. FINDPLAN-LEKABADL terminates and is sound and complete. 7

Conclusion

To test the feasibility of our proposal for knowledge-intensive planning, we ran a preliminary empirical evaluation of the framework of Section 6. We considered a DLLiteA-eKAB 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 FastDownward4). 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 ( 1 200 000 atoms) the planner timed out. Although preliminary, we consider these result positive, given the complexity of the setting, and the fact that we did not apply any optimization. Optimizations are left for future work. 4 http://www.fast-downward.org/ 21. Levesque, H.J.: Foundations of a functional approach to knowledge representation. Artificial

Intelligence 23, 155–212 (1984) 22. Levesque, H.J., Lakemeyer, G.: The Logic of Knowledge Bases. The MIT Press (2001) 23. Ortiz, M., Calvanese, D., Eiter, T.: Data complexity of query answering in expressive description logics via tableaux. J. of Automated Reasoning 41(1), 61–98 (2008) 24. Pednault, E.P.D.: ADL and the state-transition model of action. J. of Logic and Computation 4(5), 467–512 (1994) 25. Wolter, F., Zakharyaschev, M.: Temporalizing description logic. In: Gabbay, D., de Rijke, M. (eds.) Frontiers of Combining Systems, pp. 379–402. Studies Press/Wiley (1999)

References

1. Abiteboul , S. , Hull , R. , Vianu , V. : Foundations of Databases. Addison Wesley Publ. Co . ( 1995 )

2. Baader , F. , Calvanese , D. , McGuinness , D. , Nardi , D. , Patel-Schneider , P.F . (eds.): The Description Logic Handbook: Theory, Implementation and Applications . Cambridge University Press ( 2003 )

3. Bagheri Hariri , B. , Calvanese , D. , De Giacomo , G. , Deutsch , A. , Montali , M. : Verification of relational data-centric dynamic systems with external services . In: Proc. of PODS 2013 . pp. 163 - 174 ( 2013 )

4. Bagheri Hariri , B. , Calvanese , D. , Deutsch , A. , Montali , M. : State-boundedness in dataaware dynamic systems . In: Proc. of KR 2014 . AAAI Press ( 2014 )

5. Bagheri Hariri , B. , Calvanese , D. , Montali , M. , De Giacomo , G. , De Masellis , R. , Felli , P. : Description logic Knowledge and Action Bases . J. of Artificial Intelligence Research 46 , 651 - 686 ( 2013 )

6. Belardinelli , F. , Lomuscio , A. , Patrizi , F. : Verification of agent-based artifact systems . J. of Artificial Intelligence Research 51 , 333 - 376 ( 2014 )

7. Brachman , R.J. , Levesque , H.J. : Knowledge Representation and Reasoning . Morgan Kaufmann ( 2003 )

8. Bylander , T. : The computational complexity of propositional STRIPS planning . Artificial Intelligence 69 ( 1-2 ), 165 - 204 ( 1994 )

9. Calvanese , D. , De Giacomo , G. , Lembo , D. , Lenzerini , M. , Poggi , A. , Rodriguez-Muro , M. , Rosati , R.: Ontologies and databases: The DL-Lite approach . In: Tessaris, S. , Franconi , E. (eds.) RW 2009 Tutorial Lectures , LNCS, vol. 5689 , pp. 255 - 356 . Springer ( 2009 )

10. Calvanese , D. , De Giacomo , G. , Lembo , D. , Lenzerini , M. , Rosati , R.: EQL-Lite: Effective first-order query processing in description logics . In: Proc. of IJCAI 2007 . pp. 274 - 279 ( 2007 )

11. Calvanese , D. , De Giacomo , G. , Lembo , D. , Lenzerini , M. , Rosati , R. : Tractable reasoning and efficient query answering in description logics: The DL-Lite family . J. of Automated Reasoning 39 ( 3 ), 385 - 429 ( 2007 )

12. Calvanese , D. , De Giacomo , G. , Lembo , D. , Lenzerini , M. , Rosati , R. : Data complexity of query answering in description logics . Artificial Intelligence 195 , 335 - 360 ( 2013 )

13. Calvanese , D. , De Giacomo , G. , Montali , M. , Patrizi , F. : Verification and synthesis in description logic based dynamic systems . In: Proc. of RR 2013. LNCS , vol. 7994 , pp. 50 - 64 . Springer ( 2013 )

14. Cimatti , A. , Pistore , M. , Traverso , P. : Automated planning . In: Handbook of Knowledge Representation, Foundations of Artificial Intelligence , vol. 3 , pp. 841 - 867 . Elsevier ( 2008 )

15. Drescher , C. , Thielscher , M.: A fluent calculus semantics for ADL with plan constraints . In: Proc. of JELIA 2008. LNCS , vol. 5293 , pp. 140 - 152 . Springer ( 2008 )

16. Erol , K. , Nau , D.S. , Subrahmanian , V.S. : Complexity, decidability and undecidability results for domain-independent planning . Artificial Intelligence 76 ( 1-2 ), 75 - 88 ( 1995 )

17. Gabbay , D. , Kurusz , A. , Wolter , F. , Zakharyaschev , M. : Many-dimensional Modal Logics: Theory and Applications . Elsevier ( 2003 )

18. Ghallab , M. , Nau , D.S. , Traverso , P. : Automated planning - Theory and Practice . Elsevier ( 2004 )

19. Glimm , B. , Lutz , C. , Horrocks , I. , Sattler , U. : Conjunctive query answering for the description logic SHIQ . J. of Artificial Intelligence Research 31 , 151 - 198 ( 2008 )

20. Hoffmann , J. , Bertoli , P. , Helmert , M. , Pistore , M. : Message-based web service composition, integrity constraints, and planning under uncertainty: A new connection . J. of Artificial Intelligence Research 35 , 49 - 117 ( 2009 )