Verification of Inconsistency-Aware Knowledge and Action Bases?

Abstract

Description Logic Knowledge and Action Bases (KABs) have been recently introduced as a mechanism to evolve a DL KB over time by means of actions that may acquire new information from the external environment. Decidability of verification in KABs has been studied for properties expressed in first-order variants of -calculus, under a natural assumption of “run-boundedness”. However, the established framework treats inconsistency in a simplistic way, by rejecting inconsistent states produced through action execution. We overcome this limitation by adopting in the application of actions inconsistency-aware semantics based on the notion of repair. We establish decidability and complexity of verification in this extended framework.

Introduction

Recent work in knowledge representation and databases has addressed the problem of dealing with the combination of knowledge, processes and data in the design of complex enterprise systems [ 11,21,1,8,17 ]. The verification of temporal properties in this setting represents a significant research challenge, since data and knowledge makes the system infinite-state, and neither finite-state model checking [ 10 ] nor most of the current techniques for infinite-state model checking [ 4 ] apply to this case.

Along this line, Knowledge and Action Bases (KABs) [ 1 ] have been recently introduced as a mechanism that provides a semantically rich representation of the information on the domain of interest in terms of a Description Logic (DL) KB and a set of actions to change such information over time, possibly introducing new objects. In this setting, decidability of verification of sophisticated temporal properties over KABs, expressed in a variant of first-order -calculus, has been shown.

However, KABs and the majority of approaches dealing with verification in this complex setting assume a rather simple treatment of inconsistency resulting as an effect of action execution: inconsistent states are simply rejected (see, e.g., [ 12,11,2 ]). In general, this is not satisfactory, since the inconsistency may affect just a small portion of the entire KB, and should be treated in a more careful way. Notice also that actions could ? This work has been partially supported by the EU projects ACSI (FP7-ICT-257593) and Optique (FP7-IP-318338). cause an inconsistency only under specific conditions on the data, while otherwise being consistently applicable. Hence, elimination of an action is in general not an acceptable option. Starting from this observation, in this work we leverage on the research on instance-level evolution of knowledge bases [ 22,13,15,9 ], and, in particular, on the notion of knowledge base repair [ 16 ], in order to make KABs inconsistency-aware. In particular, we present a novel setting that extends KABs by assuming the availability of a repair service that is able to compute, from an inconsistent knowledge base resulting from the execution of an action, one or more repairs, in which the inconsistency has been removed with a “minimal” modification to the existing knowledge. This allows us to incorporate, in the temporal verification formalism, the possibility of quantifying over repairs. Notably, our novel setting is able to deal with both deterministic semantics for repair, in which a single repair is computed from an inconsistent knowledge base, and non-deterministic ones, by simultaneously taking into account all possible repairs. We show how the techniques developed for KABs extend to this inconsistency-aware setting, preserving both decidability and complexity results, under the same assumptions required in KABs for decidability.

We also show how our setting is able to accommodate meta-level information about the sources of inconsistency at the intentional level, so as to allow them to be queried when verifying temporal properties of the system. The decidability and complexity results for verification carry over to this extended setting as well. 2

Preliminaries

DL-LiteA Knowledge Bases. For expressing knowledge bases, we use DL-LiteA [ 19,5 ]. The syntax of concept and role expressions in DL-LiteA is as follows

B ! N j 9R

R ! P j P where N denotes a concept name, P a role name, and P an inverse role. A DL-LiteA knowledge base (KB) is a pair (T; A), where: (i) A is an Abox, i.e., a finite set of ABox membership assertions of the form N (t1) j P (t1; t2), where t1, t2 denote individuals (ii) T is a TBox, i.e., T = Tp ] Tn ] Tf , with Tp a finite set of positive inclusion assertions of the form B1 v B2, Tn a finite set of negative inclusion assertions of the form B1 v :B2, and Tf a finite set of functionality assertions of the form (funct R).

We adopt the standard FOL semantics of DLs based on FOL interpretations. We also say that A is T -consistent if (T; A) is satisfiable, i.e., admits at least one model. Queries. Answers to queries are formed by terms denoting individuals explicitly mentioned in the ABox. The domain of an ABox A, denoted by ADOM(A), is the (finite) set of terms appearing in A. A union of conjunctive queries (UCQ) q over a KB (T; A) is a FOL formula of the form W1 i n 9yi.conj i(x; yi) with free variables x and existentially quantified variables y1; : : : ; yn. Each conj i(x; yi) in q is a conjunction of atoms of the form N (z), P (z; z0), where N and P respectively denote a concept and a role name occurring in T , and z, z0 are constants in ADOM(A) or variables in x or yi, for some i 2 f1; : : : ; ng. The (certain) answers to q over (T; A) is the set ans (q; T; A) of substitutions of the free variables of q with constants in ADOM(A) such that q evaluates to true in every model of (T; A). If q has no free variables, then it is called boolean and its certain answers are either true or false.

We compose UCQs using ECQs, i.e., queries of the query language EQLLite(UCQ) [ 6 ], which is the FOL query language whose atoms are UCQs evaluated according to the certain answer semantics above. An ECQ over T and A is a possibly open formula of the form

Q := [q] j :Q j Q1 ^ Q2 j 9x.Q where q is a UCQ. The answer to Q over (T; A), is the set ANS(Q; T; A) of tuples of constants in ADOM(A) defined by composing the certain answers ans (q; T; A) of UCQ q through first-order constructs, and having existential variables range over ADOM(A).

Finally, we recall that DL-LiteA enjoys the FO rewritability property, which states that for every UCQ q, ans (q; T; A) = ans (rew(q); ;; A), where rew(q) is a UCQ computed by the reformulation algorithm in [ 5 ]. Notice that this algorithm can be extended to ECQs [ 6 ], and that its effect is to “compile away” the TBox.

Knowledge and Action Bases. We recall the notion of Knowledge and Action Bases

(KABs), as introduced in [ 1 ]. In the following, we make use of a countably infinite set C of constant to denote all possible value in the system. Moreover, we also make use of a finite set F of functions that represent service calls, and can be used to inject fresh values into the system.

A KAB is a tuple K = (T; A0; ; ) where T and A0 form the knowledge base (KB), and and form the action base. Intuitively, the KB maintains the information of interest. It is formed by a fixed DL-LiteA TBox T and an initial T -consistent DLLiteA ABox A0. A0 represents the initial state of the system and, differently from T , it evolves and incorporates new information from the external world by executing actions , according to the sequencing established by process . is a finite set of actions. An action 2 modifies the current ABox A by adding or deleting assertions, thus generating a new ABox A0. is constituted by a signature and an effect specification. The action signature is constituted by a name and a list of individual input parameters. Such parameters need to be instantiated with individuals for the execution of the action. Given a substitution for the input parameters, we denote by the instantiated action with the actual parameters coming from . The effect specification consists of a set fe1; : : : ; eng of effects, which take place simultaneously. An effect ei has the form [qi+] ^ Qi A0i, where: (i) qi+ is an UCQ, and Qi is an arbitrary ECQ whose free variables occur all among the free variables of qi+; (ii) A0i is a set of facts (over the alphabet of T ) which include as terms: individuals in A0, free variables of qi+, and Skolem terms f (x) having as arguments free variables x of qi+. The process is a finite set of condition/action rules. A condition/action rule 2 is an expression of the form Q 7! , where is an action in and Q is an ECQ over T , whose free variables are exactly the parameters of . The rule expresses that, for each tuple for which condition Q holds, the action with actual parameters can be executed.

Example 1. K = (T; A0; ; ) is a KAB defined as follows: (i) T = fC v :Dg, (ii) A0 = fC(a)g, (iii) = f 1; 2g with 1() : fC(x) D(x); C(x)g and 2(p) : fC(p) G(f (p))g, (iv) = ftrue 7! 1; C(y) 7! 2(y)g.

Verification of Standard KABs

We are interested in verifying temporal/dynamic properties over KABs. To this aim, we fix a countably infinite set C of individual constants (also called values), which act as standard names, and finite set of distinguished constants C0 C. Then, we define the execution semantics of a KAB in terms of a possibly infinite-state transition system. More specifically, we consider transition systems of the form (C; T; ; s0; abox ; )), where: (i) T is a TBox; (ii) is a set of states; (iii) s0 2 is the initial state; (iv) abox is a function that, given a state s 2 , returns an ABox associated to s, which has as individuals values of C and conforms to T ; (v) ) is a transition relation between pairs of states.

The standard execution semantics for a KAB K = (T; A0; ; ) is obtained starting from A0 by nondeterministically applying every executable action with corresponding legal parameters, and considering each possible value returned by applying the involved service calls. Notice that this is radically different from [ 1 ], where service calls are not evaluated when constructing the transition system. The executability of an action with fixed parameters does not only depend on the process , but also on the T -consistency of the ABox produced by the application of the action: if the resulting ABox is T inconsistent, the action is considered as non executable with the chosen parameters.

We consider deterministic services, i.e., services that return always the same value when called with the same input parameters. Nondeterministic services can be seamlessly added without affecting our technical results. To ensure that services behave deterministically, we recast the approach in [ 2 ] to the semantic setting of KABs, keeping track, in the states of the transition system generated by K, of all the service call results accumulated so far. To do so, we introduce the set of (Skolem terms representing) service calls as SC = ff (v1; : : : ; vn) j f =n 2 F and fv1; : : : ; vng Cg, and define a service call map as a partial function m : SC ! C.

A state of the transition system generated by K is a pair hA; mi, where A is an ABox and m is a service call map. Let (p1; : : : ; pr) : fe1; : : : ; ekg be an action in with parameters p1; : : : ; pr, and ei = [qi+] ^ Qi Ei. Let be a substitution for p1; : : : ; pr with values taken from C. We say that is legal for in state hA; mi if there exists a condition-action rule Q 7! in such that hp1; : : : ; pri 2 ANS(Q; A). We denote with DO(T; A; ) the set of facts obtained by evaluating the effects of action with parameters on ABox A, i.e.:

DO(T; A; ) = [ [

Ei [qi+]^Qi

Ei in 2ANS(([qi+]^Qi ) ;T;A) The returned set is the union of the results of applying the effects specifications in , where the result of each effect specification [qi+] ^ Qi Ei is, in turn, the set of facts Ei obtained from Ei grounded on all the assignments that satisfy the query [qi+] ^ Qi over A.

Note that DO() generates facts that use values from the domain C, but also Skolem terms, which model service calls. For any such set of facts E, we denote with CALLS(E) the set of calls it contains, and with EVALS(T; A; ) the set of substitutions that replace all service calls in DO(T; A; ) with values in C:

EVALS(T; A; ) = f j : CALLS(DO(T; A;

)) ! C is a total function g:

Each substitution in EVALS(T ; A; ) models the simultaneous evaluation of all service calls, returning results arbitrarily chosen from C.

Example 2. Consider our running example (Example 1). Starting from A0, the execution of 1 would produce A0 = fD(a); C(a)g, which is T -inconsistent. Thus, the execution of 1 is not allowed in A0. The execution of 2 with legal parameter a instead produces A00 = fG(c)g when the service call f (a) returns c. A00 is T -consistent, and 2(a) is therefore executable in A0.

Given a KAB K = (T ; A0; ; ), we employ DO() and EVALS() to define a transition relation EXECK connecting two states through the application of an action with parameter assignment. In particular, given an action with parameter assignment , we have hhA; mi; ; hA0; m0ii 2 EXECK if the following holds: (i) is a legal parameter assignment for in state hA; mi, according to ; (ii) there exists 2 EVALS(T ; A; ) such that and m agree on the common values in their domains (so as to realize the deterministic service semantics); (iii) A0 = DO(T ; A; ) ; (iv) m0 = m [ (i.e., the history of issued service calls is updated).

Standard transition system. The standard transition system KS for KAB K = (T ; A0; ; ) is a (possibly infinite-state) transition system (C; T ; ; s0; abox ; )) where: (1) s0 = hA0; ;i; (2) abox (hA; mi) = A; (3) and ) are defined by simultaneous induction as the smallest sets satisfying the following properties: (i) s0 2 ; (ii) if hA; mi 2 , then for all actions in , for all substitutions for the parameters of and for all hA0; m0i such that A0 is T -consistent and hhA; mi; ; hA0; m0ii 2 EXECK, we have hA0; m0i 2 and hA; mi ) hA0; m0i. We call S-KAB a KAB interpreted under the standard execution semantics.

Example 3. Consider K of Example 1 and its standard transition system KS . As discussed in Example 2, in state s0 = hA0; ;i only 2 is applicable with parameter a. Since DO(T ; A0; 2(a)) = fG(f (a))g, KS contains infinitely many successors for s0, each of the form hfG(x)g; ff (a) 7! xgi, where x is arbitrarily substituted with a specific value picked from C.

Verification Formalism. To specify sophisticated temporal properties over KABs, we resort to the first-order variant of -calculus [ 20,18 ] defined in [ 1 ]. This variant, here called LEAQL, exploits EQL to query the states, and supports a particular form of firstorder quantification across states: quantification ranges over the individuals explicitly present in the current active domain, and can be arbitrarily referred to in later states of the systems. Formally, LEAQL is defined as follows:

:= Q j : j 1 ^ 2 j 9x: j h i j Z j Z: where Q is a possibly open EQL query that can make use of the distinguished constants in C0, and Z is a second order predicate variable (of arity 0). We make use of the following abbreviations: 8x: = :(9x:: ), 1 _ 2 = :(: 1 ^ : 2), [ ] = :h i: , and Z: = : Z:: [Z=:Z].

The semantics of LEAQL formulae is defined over transition systems hC; T ; ; s0; abox ; )i. Since LEAQL contains formulae with both individual and predicate free variables, given a transition system , we introduce an individual variable valuation v, i.e., a mapping from individual variables x to C, and a predicate variable valuation V , i.e., a mapping from the predicate variables Z to subsets of . All the language primitives follow the standard -calculus semantics, apart from [ 1 ]: (Q)v;V = fs 2 (9x: )v;V = fs 2 j ANS(Qv; T ; abox (s)) = trueg j 9d:d 2 ADOM(abox (s)) and s 2 ( )v[x=d];V g

Here, Qv stands for the query obtained from Q by substituting its free variables according to v. When is a closed formula, ( )v;V does not depend on v or V , and we denote the extension of simply by ( ) . A closed formula holds in a state s 2 if s 2 ( ) . We call model checking verifying whether s0 2 ( ) , and we write in this case j= . Decidability of verification. We are interested in studying the verification of LEAQL properties over S-KABs. We can easily recast the undecidability result in [ 1 ] to the case of S-KABs, obtaining that verification is undecidable even for the very simple temporal reachability property Z:(N(a) _ h iZ), with N atomic concept and a 2 C.

Despite this undecidability result, we can isolate an interesting class of KABs that enjoys verifiability of arbitrary LEAQL properties through finite-state abstraction. This class is based on a semantic restriction named run-boundedness [ 2 ]. Given an SS-Ks AstaBte oKf, AaDrOunM(ab=oxs(0ss)1) < bo.fWeKSsaisy bthoautnKdeids riufnt-hbeoreunedxeidstisf athfierneiteexbisotsunadbobusn.dt. b s.t. every run in KS is bounded by b.

Theorem 1. Verification of LEAQL properties over run-bounded S-KABs is decidable, and can be reduced to finite-state model checking of propositional -calculus.

The crux of the proof is to show, given a run-bounded S-KAB K,EhQoLwptroopceorntisetrsuacst an abstract transition system KS that satisfies exactly the same LA trheleatoioring,inanadltdraenfisniitniogna scyosntsetmructKiSo.nTohfis iSs dbaosneedboyniintetrroatdivuecliyng“parusnuiintagb”lethboissei mbrualnacthioens of KS that cannot be distinguished by LKEAQL properties.

In fact, KS is of size exponential in the size of the initial state of the S-KAB K and the bound b. Hence, considering the complexity of model checking of -calculus on finite-state transition systems [ 10,20 ], we obtain that verification is in EXPTIME. 4

Repair Semantics for KABs

S-KABs are defined by taking a radical approach in the management of inconsistency: simply reject actions leading to T -inconsistent ABoxes. However, an inconsistency could be caused by a small portion of the ABox, making it desirable to handle the inconsistency by allowing the application of the action, taking at the same time care of repairing the resulting state so as to restore consistency while minimizing the information loss. To this aim, we revise the standard execution semantics for KABs so as to manage inconsistency. This is done taking advantage of the research on instance-level evolution of knowledge bases [ 22,13,15,9 ], and, in particular, of the notion of ABox repair, cf. [ 3,16 ].

In particular, we assume that in this case the system is equipped with a repair service that is executed every time an action changes the content of the ABox. In this light, a progression step of the KAB is constituted by two sub-steps: an action step, where an executable action with parameters is chosen and applied over the current ABox, followed by a repair step, where the repair service checks whether the resulting state is T -consistent or not, and, in the negative case, fixes the content of the ABox resulting from the action step, by applying its repair strategy. Repairing ABoxes. We illustrate our approach by considering two specific forms of repair that have been proposed in the literature [ 13 ] and are applicable to the context of DL ontologies [ 16 ].

– Given an ABox A and a TBox T , a bold-repair (b-repair) of A with T is a maximal T -consistent subset A0 of A. Clearly, there might be more than one bold-repair for given A and T . By REP(A; T ) we denote the set of all b-repairs of A with T . – A certain-repair (c-repair) of A with T is the ABox defined as follows: A0 = \A002REP(A;T )A00. That is, a c-repair of A with T contains only those ABox statements that occur in every b-repair of A with T .

Notice that, in general, there are (exponentially) many b-repairs of an ABox A with T , while by definition there is a single c-repair.

Example 4. Continuing Ex. 2, consider the T -inconsistent state hA0; ;i obtained by applying 1() in A0. Its two b-repairs are REP(A0; T ) = fA1; A2g with A1 = fC(a)g, A2 = fD(a)g. Its c-repair is TA2REP(A0;T ) A = fC(a)g \ fD(a)g = ;. 4.1

Bold and Certain Repair Transition Systems

We now refine the execution semantics of KABs by constructing a two-layered transition system reflecting the action and repair step alternation. In particular, we consider the two repair strategies that follow the bold and certain semantics, respectively.

We observe that, if b-repair semantics is applied, then the repair service has, in general, several possibilities to fix an inconsistent ABox. Since, a-priori, no information about the repair service can be assumed beside the repair strategy itself, the transition system capturing this execution semantics must consider the progression of the system for any computable repair, modelling the repair step as the result of a non-deterministic choice taken by the repair service when deciding which among the possible repairs will be the actually enforced one. This issue does not occur with c-repair semantics, because its repair strategy is deterministic.

In order to distinguish whether a state is obtained from an action or repair step, we introduce a special marker State(rep), which is an ABox statement with a fresh concept name State and a fresh constant rep, s.t.: if State(rep) is in the current state, this means that the state has been produced by an action step, otherwise by the repair step.

Formally, the b-transition system Kb (resp. c-transition system Kc ) for a KAB K = (T; A0; ; ) is a (possibly infinite-state) transition system (C; T; ; s0; abox ; )) where s0 = hA0; ;i, and and ) are defined by simultaneous induction as the smallest sets satisfying the following properties: (i) s0 2 ; (ii) (action step) if hA; mi 2 and State(rep) 62 A, then for all actions in , for all substitutions for the parameters of and for all hA0; m0i s.t. hhA; mi; ; hA0; m0ii 2 EXECK, let A00 = A0 [ fState(rep)g, and then hA00; m0i 2 and hA; mi ) hA00; m0i; (iii) (repair step) if hA; mi 2 and State(rep) 2 A, then for b-repair A0 (resp. c-repair

A0) of A fState(rep)g with T , we have hA0; mi 2 and hA; mi ) hA0; mi. We refer to KABs with b-transition (resp. c-transition) system semantics as b-KAB (resp. c-KAB).

Example 5. Under b-repair semantics, the KAB in our running example looks as follows. Since A0 is T -inconsistent, we have two bold repairs, A1 and A2, which in turn give raise to two runs: hA0; ;i ) hA0r; ;i ) hA1; ;i and hA0; ;i ) hA0r; ;i ) hA2; ;i, where A0r = fA0 [ fSTATE(REP)g. Since instead 1 does not lead to any inconsistency, for every candidate successor A00 = fG(x)g with m = f(f (a) 7! x)g (see Ex. 3), we we have hA0; ;i ) hA00 [ fSTATE(REP)g; mi ) hA00; mi, reflecting that in this case the repair service just maintains the resulting ABox unaltered. 4.2

Verification Under Repair Semantics

We observe that the alternation between an action and a repair step makes EQL queries meaningless for the intermediate states produced as a result of action steps, because the resulting ABox could be in fact T -inconsistent (see, e.g., state hA0r; ;i in Ex. 5). In fact, such intermediate states are needed just to capture the dynamic structure that reflects the behaviour of the system. E.g., state hA0r; ;i in Ex. 5 has two successor states, attesting that the repair service with bold semantics will produce one between two possible repairs.

In this light, we introduce the inconsistency-tolerant temporal logic LIAT, which is the fragment of LEAQL defined as:

:= Q j : j 1 ^ 2 j 9x: j h i[ ] j [ ][ ] j Z j Z: Beside the standard abbreviations introduced for LEAQL, we also make use of the following: h ih i = :[ ][ ]: , and [ ]h i = :h i[ ]: . This logic can be used to express interesting properties over b- and c-KABs, exploiting different combinations of the h i and [ ] next-state operators so as to quantify over the possible action steps and corresponding repair steps, ensuring at the same time that only the T -consistent states produced by the repair steps are queried. For example, Z:( _ h ih iZ) models the “optimistic” reachability of , stating that there exists a sequence of action and repair steps, s.t. eventually holds. Conversely, Z:( _ h i[ ]Z) models the “robust” reachability of , stating the existence of a sequence of action steps leading to independently from the behaviour of the repair service. This patterns can be nested into more complex properties that express requirements about the acceptable progressions of the system, taking into account data and repairs. E.g., Z:(8x:Stud(x) ! Y:(Grad(x) _ h i[ ]Y )) ^ [ ][ ]Z states that, for every student x encountered in any state of the system, it is possible to “robustly” reach a state where x becomes graduated.

Since for a given ABox there exist finitely many b-repairs, and one c-repair, the technique used to prove decidability of properties for run-bounded S-KABs can be extended to deal with b- and c-KABs as well.

Theorem 2. Verification of LIAT properties over run-bounded b-KABs and c-KABs is decidable. 5

Extended Repair Semantic for KABs

B-KABs and c-KABs provide an inconsistency-handling semantics to KABs. However, despite dealing with possible repairs when some action step produces a T -inconsistent ABox, they do not explicitly track whether a repair has been actually enforced, nor do they provide finer-grained insights about which TBox assertions were involved in the inconsistency. Here we extend the repair execution semantics so as to equip the transition system with this additional information.

While DL-LiteA does not allow, in general, to uniquely extract from a T -inconsistent ABox a set of individuals that are responsible for the inconsistency [ 7 ], its separability property [ 7 ] guarantees that inconsistency arises because a single negative TBox assertion is violated. More specifically, a T -inconsistency involves the violation of either a functionality assertion or negative inclusion in T . Since DL-LiteA obeys the restriction that no functional role can be specialized, the first case can be detected by just considering the ABox and the functionality assertion alone. Contrariwise, the second requires also to take into account the positive inclusion assertions (since disjointness propagates downward to the subclasses). Thanks to the FO rewritability of ontology satisfiability in DL-LiteA [ 7 ], each such check can be done by constructing a FOL boolean query that corresponds to the considered functional or negative inclusion assertion, and that can be directly evaluated over the ABox, considered as a database of facts.

Following [ 7 ], given a functionality assertion (funct R), we construct the query f qunsat((funct R)) = 9x; x1; x2: (R; x; x1) ^ (R; x; x2) ^ x1 6= x2, where (R; x; y) = P (x; y) if R = P , and (R; x; y) = P (y; x) if R = P . Given a negative concept inclusion B1 v :B2 and a set of positive inclusions Tp, we construct the query qunnsat(B1 v :B2; Tp) = rew (Tp; 9x: (B1; x) ^ (B2; x)), where (B; x) = N (x) if B = N , (B; x) = P (x; ) if B = 9P , and (B; x) = P ( ; x) if B = 9P . Similarly, given a negative role inclusion R1 v :R2, we construct the query qunnsat(R1 v :R2; Tp) = rew (Tp; 9x1; x2: (R1; x1; x2) ^ (R2; x1; x2)). 5.1

Extended Repair Transition System

With this machinery at hand, given a KB (T; A) we can now compute the set of TBox assertions in T that are actually violated by A. To do so, we assume wlog that C0 contains one distinguished constant per TBox assertion in T , and introduce a function LABEL, that, given a TBox assertion, returns the corresponding constant. Let C0 be the set of such constants. We then define the set VIOL(A; T ) of constants labeling TBox assertions in T violated by A, as: fd 2 fd 2 f j 9t 2 Tf s.t. d = LABEL(t) and A j= qunsat(t)g [

n j 9t 2 Tn s.t. d = LABEL(t) and A j= qunsat(t; Tp)g Example 6. Consider K in Ex. 1, with T = fC=vq:unnDsat(gC,anvd :AD0=;;f)D=(a9)x;:CC((ax))g^inDE(xxa)m.Spilnec2e. Assume that LABEL(C v :D) = `. We have A0 j= , we obtain VIOL(A0; T ) = f`g.

We now employ this information assuming that the repair service decorates the states it produces with information about which TBox functional and negative inclusion assertions have been involved in the repair. This is done with a fresh concept Viol that keeps track of the labels of violated TBox assertions.

Formally, we define the eb-transition system Keb (resp. ec-transition system (CKe;cT) ;for; sK0;AaBboxK; )=) c(oTn;sAtr0u;cte;d s)taartsinag (fproomssiblKby (irnefispn.ite-Kcs)tabtey) rterfiannsinitgiotnhesyrespteamir step as follows: if hA; mi 2 and State(rep) 2 A, then for b-repair A0 (resp. c-repair A0) of A fState(rep)g with T , we have hA0v; mi 2 and hA; mi ) hA0v; mi, where A0v = A0 [ fViol(d) j d 2 VIOL(A0; T )g. 5.2

Verification Under Extended Repair Semantics

Thanks to the insertion of information about violated TBox assertions in their transition systems, eb-KABs and ec-KABs support the verification of LIAT properties that mix dynamic requirements with queries over the instance-level information and over the meta-level information related to inconsistency. Notice that such properties can indirectly refer to specific TBox assertions, thanks to the fact that their labels belong to the set of distinguished constants C0. Examples of formulae focused on the presence of violations in the system are: – Z:(:9l:Viol(l)) ^ [ ][ ]Z says that no state of the system is manipulated by the repair service; – Z:(8l:Viol(l) ! ( Y: W::Viol(l) ^ [ ][ ]W _ h i[ ]Y ) ^ [ ][ ]Z says that, in all states, whenever a TBox assertion a is violated, independently from the applied repairs there exists a run that reaches a state starting from which a will never be violated anymore.

Since the TBox assertions are finitely many and fixed for a given KAB, the key decidability result of Theorem 2 carries over seamlessly to these extended repair semantics. Theorem 3. Verification of LIAT properties over run-bounded eb-KABs and ec-KABs is decidable. 5.3

From Standard to Extended Repair KABs

It is clear that extended repair KABs are richer than repair KABs. We now show that eband ec-KABs are also richer than S-KABs, thanks to the fact that information about the violated TBox assertions is explicitly tracked in all states resulting from a repair step. In particular, verification of LEAQL properties over a KAB K under standard semantics can be recast as a corresponding verification problem over K interpreted either under extended bold or extended certain repair semantics. The intuition behind the reduction is that a property holds over Ks if that property holds in the portion of the Keb (or Kec) where no TBox assertion is violated. The absence of violation can be checked over T -consistent states by issuing the EQL query :9x:[Viol(x)]. Technically, we define a translation function that transforms an arbitrary LEAQL property into a LIAT property 0 = ( ). The translation ( ) is inductively defined by recurring over the structure of and substituting each occurrence of h i with h ih i((:9x:Viol(x))^ ( )), and each occurrence of [ ] with [ ]h i((:9x:Viol(x)) ! ( )). Observe that, in , the choice of h i for the nested operator can be substituted by [ ], because for T -consistent states produced by an action step, the repair step simply copy the resulting state, generating a unique successor even in the eb-semantics.

Theorem 4. Given a KAB K and a ec = ( ).

K j The correctness of this result is obtained by considering the semantics of LEAQL and LIAT, and the construction of the transition systems under the three semantics.

EQL property , s = LA K j iff eb =

K j ( ) iff

Weakly Acyclic KABs

So far, all the decidability results here presented have relied on the assumption that the considered KAB is run-bounded. As pointed out in [ 2 ], run boundedness is a semantic condition that is undecidable to check. In [ 2 ], a sufficient, syntactic condition borrowed from weak acyclicity in data exchange [ 14 ] has been proposed to actually check whether the KAB under study is run bounded and, in turn, verifiable.

Intuitively, given a KAB K, this test constructs a dependency graph tracking how the action effect specifications of K transport values from one state to the next one. To track all the actual dependencies, every involved query is first rewritten considering the positive inclusion assertions of the TBox. Two types of dependencies are tracked: copy of values and usage of values as service call parameters. K is said to be weakly acyclic if there is no cyclic chain of dependencies of the second kind. The presence of such a cycle could produce an infinite chain of fresh values generation through service calls.

The crux of the proof showing that weakly acyclicity ensures run boundedness is based on the notion of positive dominant, which creates a simplified version of the KAB that, from the execution point of view, obeys three key properties. First, its execution consists of a single run that closely resembles the chase of a set of tuplegenerating dependencies, which terminates under the assumption of weak acyclicity [ 14 ], guaranteeing that the positive dominant is indeed run-bounded. Second, it considers only the positive inclusion assertions of the TBox, therefore producing always the same behaviour independently from which execution semantics is chosen, among the ones discussed in this paper. Third, for every run contained in each of the transition systems generated under the standard, bold repair, certain repair, and their extended versions, the values accumulated along the run are “bounded” by the ones contained in the unique run of the positive dominant. This makes it possible to directly carry run-boundedness from the positive dominant to the original KAB, independently from which execution semantics is considered.

Theorem 5. Given a weakly acyclic KAB K, we have that s , b , c , eb, ec are all K K K K K run-bounded.

Theorem 5 shows that weak acyclicity is an effective method to check verifiability of KABs under all inconsistency-aware semantics considered in this paper. 7

Conclusion

We have approached the problem of inconsistency handling in Knowledge and Action Bases, by resorting to an approach based on ABox repairs. An orthogonal approach to the one taken is to maintain ABoxes that are inconsistent with the TBox as states of the transition system, and rely, both for the progression mechanism and for answering queries used in verification, on consistent query answering [ 3,16 ]. Notably, we are able to show that the decidability and complexity results established for the repair-based approaches carry over also to this setting. It remains open to investigate the relationship between these orthogonal approaches to dealing with inconsistency in KABs.

References

1. Bagheri Hariri , B. , Calvanese , D. , De Giacomo , G. , De Masellis , R. , Montali , M. , Felli , P. : Verification of description logic Knowledge and Action Bases . In: Proc. of the 20th Eur. Conf. on Artificial Intelligence (ECAI 2012 ). pp. 103 - 108 ( 2012 )

2. Bagheri Hariri , B. , Calvanese , D. , De Giacomo , G. , Deutsch , A. , Montali , M. : Verification of relational data-centric dynamic systems with external services . CoRR Technical Report arXiv:1203.0024 , arXiv.org e-Print archive ( 2012 ), available at http://arxiv.org/ abs/1203.0024

3. Bertossi , L.E. : Consistent query answering in databases . SIGMOD Record 35 ( 2 ), 68 - 76 ( 2006 )

4. Burkart , O. , Caucal , D. , Moller , F. , Steffen , B. : Verification of infinite structures . In: Handbook of Process Algebra. Elsevier Science ( 2001 )

5. Calvanese , D. , De Giacomo , G. , Lembo , D. , Lenzerini , M. , Poggi , A. , Rodr´ıguez- Muro , M. , Rosati , R.: Ontologies and databases: The DL-Lite approach . In: Tessaris, S. , Franconi , E. (eds.) Reasoning Web. Semantic Technologies for Informations Systems - 5th Int. Summer School Tutorial Lectures (RW 2009), Lecture Notes in Computer Science , vol. 5689 , pp. 255 - 356 . Springer ( 2009 )

6. Calvanese , D. , De Giacomo , G. , Lembo , D. , Lenzerini , M. , Rosati , R.: EQL-Lite: Effective first-order query processing in description logics . In: Proc. of the 20th Int. Joint Conf. on Artificial Intelligence (IJCAI 2007 ). pp. 274 - 279 ( 2007 )

7. 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 )

8. Calvanese , D. , De Giacomo , G. , Lembo , D. , Montali , M. , Santoso , A. : Ontology-based governance of data-aware processes . In: Proc. of the 6th Int. Conf. on Web Reasoning and Rule Systems (RR 2012). Lecture Notes in Computer Science , vol. 7497 , pp. 25 - 41 . Springer ( 2012 )

9. Calvanese , D. , Kharlamov , E. , Nutt , W. , Zheleznyakov , D. : Evolution of DL-Lite knowledge bases . In: Proc. of the 9th Int. Semantic Web Conf. (ISWC 2010). Lecture Notes in Computer Science , vol. 6496 , pp. 112 - 128 . Springer ( 2010 )

10. Clarke , E.M. , Grumberg , O. , Peled , D.A. : Model checking . The MIT Press, Cambridge, MA, USA ( 1999 )

11. Deutsch , A. , Hull , R. , Patrizi , F. , Vianu , V. : Automatic verification of data-centric business processes . In: Proc. of the 12th Int. Conf. on Database Theory (ICDT 2009 ). pp. 252 - 267 ( 2009 )

12. Deutsch , A. , Sui , L. , Vianu , V. : Specification and verification of data-driven web applications . J. of Computer and System Sciences 73 ( 3 ), 442 - 474 ( 2007 )

13. Eiter , T. , Gottlob , G.: On the complexity of propositional knowledge base revision, updates and counterfactuals . Artificial Intelligence 57 , 227 - 270 ( 1992 )

14. Fagin , R. , Kolaitis , P.G. , Miller , R.J. , Popa , L. : Data exchange: Semantics and query answering . Theoretical Computer Science 336 ( 1 ), 89 - 124 ( 2005 )

15. Flouris , G. , Manakanatas , D. , Kondylakis , H. , Plexousakis , D. , Antoniou , G.: Ontology change: Classification and survey . Knowledge Engineering Review 23 ( 2 ), 117 - 152 ( 2008 )

16. Lembo , D. , Lenzerini , M. , Rosati , R. , Ruzzi , M. , Savo , D.F. : Inconsistency-tolerant semantics for description logics . In: Proc. of the 4th Int. Conf. on Web Reasoning and Rule Systems (RR 2010 ). pp. 103 - 117 ( 2010 )

17. Limonad , L. , De Leenheer , P. , Linehan , M. , Hull , R. , Vaculin , R.: Ontology of dynamic entities . In: Proc. of the 31st Int. Conf. on Conceptual Modeling (ER 2012 ) ( 2012 )

18. Park , D.M.R. : Finiteness is Mu-ineffable . Theoretical Computer Science 3 ( 2 ), 173 - 181 ( 1976 )

19. Poggi , A. , Lembo , D. , Calvanese , D. , De Giacomo , G. , Lenzerini , M. , Rosati , R.: Linking data to ontologies . J. on Data Semantics X , 133 - 173 ( 2008 )

20. Stirling , C. : Modal and Temporal Properties of Processes. Springer ( 2001 )

21. Vianu , V. : Automatic verification of database-driven systems: a new frontier . In: Proc. of the 12th Int. Conf. on Database Theory (ICDT 2009 ). pp. 1 - 13 ( 2009 )

22. Winslett , M. : Updating Logical Databases. Cambridge University Press ( 1990 )