Verification of Inconsistency-Aware Knowledge and Action Bases

1 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 [Deutsch et al., 2009; Vianu, 2009; Bagheri Hariri et al., 2012; Calvanese et al., 2012; Limonad et al., 2012]. The verification of temporal properties in this setting represents a significant research challenge, since data and knowledge makes the system infinite-state, and neither finitestate model checking [Clarke et al., 1999] nor most of the current techniques for infinite-state model checking [Burkart et al., 2001] apply to this case.

Along this line, Knowledge and Action Bases (KABs) [Bagheri Hariri et al., 2012] have 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.

∗The authors are supported by the EU project ACSI (FP7-ICT257593) and Optique (FP7-IP-318338). Kharlamov was also supported by the ERC grant Webdam, agreement n. 226513.

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., [Deutsch et al., 2007; 2009; Bagheri Hariri et al., 2013]). 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.

Starting from this observation, in this work we leverage on the research on instance-level evolution of knowledge bases [Winslett, 1990; Eiter and Gottlob, 1992; Flouris et al., 2008; Calvanese et al., 2010], and, in particular, on the notion of knowledge base repair [Lembo et al., 2010], 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 metalevel 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.

The proofs of all presented theorems are contained in an extended version of this paper [Calvanese et al., 2013].

2 Preliminaries

2.1 DL-LiteA Knowledge Bases

For expressing knowledge bases, we use DL-LiteA [Poggi et al., 2008; Calvanese et al., 2009]. The syntax of concept and role expressions in DL-LiteA is as follows

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 formN(t1) | 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 ⊑ B2, Tn a finite set of negative inclusion assertions of the form B1 ⊑ ¬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 I = (∆I , ·I ) such that cI ∈ ∆I , N I ⊆ ∆I , and P I ⊆ ∆I ×∆I . The semantics of the construct, of TBox and ABox assertions, and the notions of satisfaction and of model are as usual. We also say that A is T-consistent if (T,A) is satisfiable, i.e., admits at least one model, otherwise we say A is T -inconsistent.

Queries. As usual (cf. OWL 2 QL), 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 ∨1≤i≤n ∃⃗ yi.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 formN(z), P(z, z′ ), where N and P respectively denote a concept and a role name occurring in T , and z, z′ are constants in ADOM(A) or variables in ⃗x or ⃗ yi, for some i ∈ {1, . . . , n}. 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 EQL-Lite(UCQ) [Calvanese et al., 2007a], 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

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 UCQs q through first-order constructs, and interpreting existential variables as ranging 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 [Calvanese et al., 2009]. Notice that this algorithm can be extended to ECQs [Calvanese et al., 2007a], and that its effect is to "compile away" the TBox.

2.2 Knowledge and Action Bases

We recall the notion of Knowledge and Action Bases (KABs), as introduced in [Bagheri Hariri et al., 2012]. 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 Tconsistent DL-LiteA 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 actions. An action γ ∈ Γ generates a new ABox A′ from the current ABox A, by adding or deleting assertions. γ 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 {e1, . . . , en} of effects, which take place simultaneously. An effect ei has the form [q+ i ] ∧Q-i ⇝A′i , where: (i) q+ i is an UCQ, and Q-i is an arbitrary ECQ whose free variables occur all among the free variables of q+ i ; (ii) A′i is a set of facts (over the alphabet of T) which include as terms: individuals in A0, free variables of q+ i , and Skolem terms f(⃗x) having as arguments free variables ⃗x of q+ i . The distinction between q+ i and Q-i is needed for technical reasons (see [Calvanese et al., 2013]).

The process Π is a finite set of condition/action rules. A condition/action rule π ∈ Π is an expression of the form Q ↦→ γ, 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 2.1. K = (T,A0, Γ,Π) is a KAB defined as follows: (i) T = {C ⊑ ¬D}, (ii) A0 = {C(a)}, (iii) Γ = {γ1, γ2} with γ1() : {C(x) ⇝ D(x),C(x)} and γ2(p) : {C(p) ⇝ G(f(p))}, (iv) Π = {true ↦→ γ1, C(y) ↦→ γ2(y)}.

3 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 ∈ Σ is the initial state; (iv) abox is a function that, given a state s ∈ Σ, 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 [Bagheri Hariri et al., 2012], 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 Tconsistency 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 [Bagheri Hariri et al., 2013] 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 = {f(v1, . . . , vn) | f/n ∈ F and {v1, . . . , vn} ⊆ C}, 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 〈A,m〉, where A is an ABox and m is a service call map. Let γ(p1, . . . , pr) : {e1, . . . , ek} be an action in Γ with parameters p1, . . . , pr, and ei = [q+ i ] ∧Q-i ⇝ Ei. Let σ be a substitution for p1, . . . , pr with values taken from C. We say that σ is legal for γ in state 〈A,m〉 if there exists a conditionaction rule Q ↦→ γ in Π such that 〈p1, . . . , pr〉σ ∈ 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, so as to progress (cf. planning [Ghallab et al., 2004]) the system from the current state to the next:

The returned set is the union of the results of applying the effects specifications in γ, where the result of each effect specification [q+ i ]∧Q-i ⇝Ei is, in turn, the set of facts Eiσρ obtained from Eiσ grounded on all the assignments ρ that satisfy the query [q+ i ] ∧Q-i 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:

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

Example 3.1. Consider our running example (Example 2.1). Starting from A0, the execution of γ1 would produce A′ = {D(a), C(a)}, which is T -inconsistent. Thus, the execution of γ1 in A0 should either be rejected or its effect should be repaired (cf. Section 4). The execution of γ2 with legal parameter a instead produces A′′ = {G(c)} when the service call f(a) returns c. A′′ 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 〈〈A,m〉, γσ, 〈A′ ,m′ 〉〉 ∈ EXECK if the following holds: (i) σ is a legal parameter assignment for γ in state 〈A,m〉, according to Π; (ii) there exists θ ∈

EVALS(T,A, γσ) such that θ and m agree on the common values in their domains (so as to realize the deterministic service semantics); (iii) A′ = DO(T, A, γσ)θ; (iv) m′ = m∪θ (i.e., the history of issued service calls is updated).

Standard transition system. The standard transition system ΥSK for KAB K = (T,A0, Γ,Π) is a (possibly infinitestate) transition system (C, T, Σ, s0, abox , ⇒) where: (i) s0 = 〈A0, ∅〉; (ii) abox (〈A, m〉) = A; (iii) Σ and ⇒ are defined by simultaneous induction as the smallest sets satisfying the following properties: (i) s0 ∈ Σ; (ii) if 〈A,m〉 ∈ Σ , then for all actions γ in Γ, for all substitutions σ for the parameters of γ and for all 〈A′ ,m′ 〉 such that A′ is T-consistent and 〈〈A, m〉, γσ, 〈A′ , m′ 〉〉 ∈ EXECK, we have 〈A′ , m′ 〉 ∈ Σ and 〈A, m〉 ⇒ 〈A′ , m′ 〉. We call S-KAB a KAB interpreted under the standard execution semantics.

Example 3.2. Consider K of Example 2.1 and its standard transition system ΥSK. As discussed in Example 3.1, in state s0 = 〈A0, ∅〉 only γ2 is applicable with parameter a. Since DO(T, A0, γ2(a)) = {G(f(a))}, ΥSK contains infinitely many successors for s0, each of the form 〈{G(x)}, {f(a) ↦→ x}〉, 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 [Stirling, 2001; Park, 1976] defined in [Bagheri Hariri et al., 2012]. This variant, here called µLEQL A , 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, µLEQL A is defined as follows:

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: ∀x.Φ = ¬(∃x.¬Φ), Φ1∨Φ2 = ¬(¬Φ1∧¬Φ2), [-]Φ = ¬〈-〉¬Φ, and νZ.Φ = ¬µZ.¬Φ[Z/¬Z].

The semantics of µLEQL A formulae is defined over transition systems 〈C, T, Σ, s0, abox , ⇒〉. Since µLEQL A 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 a subset of Σ. All the language primitives follow the standard µ-calculus semantics, apart from the two listed below [Bagheri Hariri et al., 2012]:

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 ∈ Σ if s ∈ (Φ)Υ . We call model checking verifying whether s0 ∈ (Φ)Υ , and we write in this case Υ |= Φ.

Decidability of verification. We are interested in studying the verification of µLEQL A properties over S-KABs. We can easily recast the undecidability result in [Bagheri Hariri et al., 2012] to the case of S-KABs, obtaining that verification is undecidable even for the very simple temporal reachability property µZ.(N(a)∨〈-〉Z), with N atomic concept and a ∈ C.

Despite this undecidability result, we can isolate an interesting class of KABs that enjoys verifiability of arbitrary µLEQL A properties through finite-state abstraction. This class is based on a semantic restriction named run-boundedness [Bagheri Hariri et al., 2013]. Given an S-KAB K, a run τ = s0s1 · · · of ΥSK is bounded if there exists a finite bound b s.t. ∣∣⋃s state of τ ADOM(abox(s))∣∣ < b. We say that K is runbounded if there exists a bound b s.t. every run τ in ΥSK is bounded by b.

Theorem 3.3. Verification of µLEQL A properties over runbounded S-KABs is decidable, and can be reduced to finitestate model checking of propositional µ-calculus.

The crux of the proof is to show, given a run-bounded SKAB K, how to construct an abstract transition system ΘSK that satisfies exactly the same µLEQL A properties as the original transition system ΥSK. This is done by introducing a suitable bisimulation relation, and defining a construction of ΘSK based on iteratively "pruning" those branches of ΥSK that cannot be distinguished by µLEQL A properties.

In fact, ΘSK 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 [Clarke et al., 1999; Stirling, 2001], 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 that lead 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 action execution, and taking care of repairing the resulting state so as to restore consistency while minimizing the information loss. To this aim, we revise the standard semantics for KABs so as to manage inconsistency, relying on the research on instance-level evolution of knowledge bases [Winslett, 1990; Eiter and Gottlob, 1992; Flouris et al., 2008; Calvanese et al., 2010], and, in particular, on the notion of ABox repair, cf. [Bertossi, 2006; Lembo et al., 2010].

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 [Eiter and Gottlob, 1992] and are applicable to the context of DL ontologies [Lembo et al., 2010].

• Given an ABox A and a TBox T , a bold-repair (b-repair) of A with T is a maximal T-consistent subset A′ 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: A′ = ∩A′′∈REP(A,T)A′′ . That is, a crepair of A with T contains only those ABox statements that occur in every b-repair of A with T .

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.1. Continuing Example 3.1, consider the Tinconsistent state 〈A′ , ∅〉 obtained from γ1() in A0. Its two b-repairs are REP(A′ , T) = {A1,A2} with A1 = {C(a)}, A2 = {D(a)}. Its c-repair is ⋂A∈REP(A′,T ) A = {C(a)} ∩ {D(a)} = ∅.

4.1 Bold and Certain Repair Transition Systems

We now refine the execution semantics of KABs by constructing a two-layered transition system that reflects the alternation between the action and the repair steps. In particular, we consider the two cases for which the repair strategy either follows the bold or certain semantics. We observe that, if b-repair semantics is applied, then the repair service has, in general, several possibilities to fix an inconsistent ABox. Since, apriori, 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(temp), which is an ABox statement with a fresh concept name State and a fresh constant temp, s.t.: if State(temp) 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ΥbK (resp. c-transition system ΥcK) for a KAB K = (T, A0, Γ, Π) is a (possibly infinitestate) transition system (C, T, Σ, s0, abox , ⇒) where:

1. s0 = 〈A0, ∅〉;
2. Σ and ⇒ are defined by simultaneous induction as the smallest sets satisfying the following properties:
3. (i) s0 ∈ Σ;
4. (ii) (action step) if 〈A,m〉 ∈ Σ and State(temp) ̸∈ A, then for all actions γ in Γ, for all substitutions σ for the parameters of γ and for all 〈A′ ,m′ 〉 s.t. 〈〈A,m〉, γσ, 〈A′ ,m′ 〉〉 ∈ EXECK, let A′′ = A′ ∪ {State(temp)}, and then 〈A′′ ,m′ 〉 ∈ Σ and 〈A, m〉 ⇒ 〈A′′ , m′ 〉;
5. (iii) (repair step) if 〈A,m〉 ∈ Σ and State(temp) ∈ A, then for b-repair A′ (resp. c-repair A′ ) of A{State(temp)} with T , we have 〈A′ , m〉 ∈ Σ and 〈A, m〉 ⇒ 〈A′ , m〉.

We refer to KABs with b-transition (resp. c-transition) system semantics as b-KAB (resp. c-KAB).

Example 4.2. Under b-repair semantics, the KAB in our running example looks as follows. Since A′ is T-inconsistent, we have two bold repairs, A1 and A2, which in turn give rise to two runs: 〈A0, ∅〉 ⇒ 〈A′r, ∅〉 ⇒ 〈A1, ∅〉 and 〈A0, ∅〉 ⇒ 〈A′r, ∅〉 ⇒ 〈A2, ∅〉, where A′r = {A′ ∪ {State(temp)}. Since instead γ1 does not lead to any inconsistency, for every candidate successor A′′ = {G(x)} with m = {(f(a) ↦→ x)} (see Example 3.2), we have 〈A0, ∅〉 ⇒ 〈A′′ ∪ {State(temp)},m〉 ⇒ 〈A′′ ,m〉, 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 〈A′r , ∅〉 in Example 4.2). In fact, such intermediate states are needed just to capture the dynamic structure that reflects the behaviour of the system. E.g., state 〈A′r , ∅〉 in Example 4.2 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 µLIT A , which is a fragment of µLEQL A defined as:

Beside the standard abbreviations introduced for µLEQL A , we also make use of the following: 〈-〉〈-〉Φ = ¬[-][-]¬Φ, and [-]〈-〉Φ = ¬〈-〉[-]¬Φ. This logic can be used to express interesting properties over b- and c-KABs, exploiting different combinations of the 〈-〉 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.(Φ ∨ 〈-〉〈-〉Z) models the "optimistic" reachability of Φ, stating that there exists a sequence of action and repair steps, s.t. Φ eventually holds. Conversely, µZ.(Φ ∨ 〈-〉[-]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.(∀x.Stud(x) → µY.(Grad(x) ∨ 〈-〉[-]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 4.3. Verification of µLIT A properties over runbounded b-KABs and c-KABs is decidable.

The precise relationship between b-KABs and c-KABs remains to be investigated.

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. We extend the repair execution semantics of so as to equip the transition systemwith 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 [Calvanese et al., 2007b], its separability property [Calvanese et al., 2007b] 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 to 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 [Calvanese et al., 2007b], 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 [Calvanese et al., 2007b], given a functionality assertion (funct R), we construct the query qf unsat((funct R)) = ∃x, x1, x2.η(R, x, x1) ∧ η(R, x, x2) ∧ x1 ̸= 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 ⊑ ¬B2 and a set of positive inclusions Tp, we construct the query qn unsat (B1 ⊑ ¬B2, Tp) = rew(Tp, ∃x.γ(B1, x) ∧ γ(B2, x)), where γ(B, x) = N(x) if B = N, γ(B, x) = P(x, ) if B = ∃P, and γ(B, x) = P( , x) if B = ∃P -. Similarly, given a negative role inclusion R1 ⊑ ¬R2, we construct the query qn unsat (R1 ⊑ ¬R2, Tp) = rew(Tp, ∃x1, 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. We then define the set VIOL(A, T) of constants labeling TBox assertions in T violated by A, as:

Example 5.1. Consider K in Example 2.1, with T = {C ⊑ ¬D}, and A′ = {D(a), C(a)} in Example 3.1. Assume that LABEL(C ⊑ ¬D) = ℓ. We have φ = qn unsat (C ⊑ ¬D, ∅) = ∃x.C(x) ∧D(x). Since A′ |= φ, we get VIOL(A′ , T) = {ℓ}.

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 Υeb K (resp. ectransition system Υec K ) for KAB K = (T, A0, Γ, Π) as a (possibly infinite-state) transition system (C, T,Σ, s0, abox,⇒)

constructed starting from ΥbK (resp. ΥcK) by refining the repair step as follows: if 〈A,m〉 ∈ Σ and State(temp) ∈ A, then for b-repair A′ (resp. c-repair A′ ) of A-{State(temp)} with T , we have 〈A′v , m〉 ∈ Σ and 〈A, m〉 ⇒ 〈A′v , m〉, where A′v = A′ ∪ {Viol(d) | d ∈ VIOL(A′ , T)}.

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 µLIT A 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.(¬∃l.Viol(l))∧[-][-]Z says that no state of the system is manipulated by the repair service;
• νZ.(∀l.Viol(l) → (µY.νW.¬Viol(l) ∧ [-][-]W ∨ 〈-〉[-]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 4.3 can be seamlessly carried over to these extended repair semantics.

Theorem 5.2. Verification of µLIT A properties over runbounded 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 eb- and 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 µLEQL A 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 ΥsK if that property holds in the portion of the Υeb K (or Υec K ) where no TBox assertion is violated. The absence of violation can be checked over T -consistent states by issuing the EQL query ¬∃x.[Viol(x)]. Technically, we define a translation function τ that transforms an arbitrary µLEQL A property Φ into a µLIT A property Φ′ = τ(Φ). The translation τ(Φ) is inductively defined by recurring over the structure of Φ and substituting each occurrence of 〈-〉Ψ with 〈-〉〈-〉((¬∃x.Viol(x)) ∧ τ (Ψ)), and each occurrence of [-]Ψ with [-]〈-〉((¬∃x.Viol(x)) → τ (Ψ)). Observe that, in τ , the choice of 〈-〉 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.

The correctness of this result can be directly obtained by considering the semantics of µLEQL A and µLIT A , and the construction of the transition systems under the three semantics.

6 Weakly Acyclic KABs

So far, all the decidability results here presented have relied on the assumption that the considered KAB is state-bounded. As pointed out in [Bagheri Hariri et al., 2013], run boundedness is a semantic condition that is undecidable to check. In [Bagheri Hariri et al., 2013], a sufficient, syntactic condition borrowed from weak acyclicity in data exchange [Fagin et al., 2005] 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 actions 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 use of values as parameters of a service call. 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 to three key properties. First, its execution consists of a single run that closely resembles the chase of a set of tuple-generating dependencies, which terminates under the assumption of weak acyclicity [Fagin et al., 2005], 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 runboundedness from the positive dominant to the original KAB, independently from which execution semantics is considered.

Theorem 6.1. Given a weakly acyclic KAB K, we have that ΥsK, ΥbK, ΥcK, Υeb K , Υec K are all run-bounded.

Theorem 6.1 shows that weak acyclicity is an effective method to check verifiability of KABs under all inconsistencyaware 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 [Bertossi, 2006; Lembo et al., 2010]. Notably, we are able to show that the decidability and complexity results established for the repairbased approaches carry over also to this setting. It remains open to investigate the relationship between these orthogonal approaches to dealing with inconsistency in KABs.