Verification of Generalized Inconsistency-Aware Knowledge and Action Bases

1 Introduction

The combination of static and dynamic aspects in modeling complex organizational domains is a challenging task that has received increased attention, and has led to the study of settings combining formalisms from knowledge representation, database theory, and process management [Hull, 2008; Vianu, 2009; Calvanese et al., 2013a]. Specifically, Knowledge and Action Bases (KABs) [Bagheri Hariri et al., 2013b] have been put forward to provide a semantically rich representation of a domain. In KABs, static aspects are modeled using a knowledge base (KB) expressed in the lightweight Description Logic (DL) [Baader et al., 2003] DL-LiteA [Calvanese et al., 2007b; 2009], while actions are used to evolve its extensional part over time, possibly introducing fresh individuals from the external environment. An important aspect that has received little attention so far in such systems is the management of inconsistency with respect to domain knowledge that may arise when the extensional information is evolved over time. In fact, inconsistency is typically handled naively by just rejecting updates in actions when they would lead to inconsistency. This shortcoming is not only present in KABs, but virtually in all related approaches in the literature, e.g., [Deutsch et al., 2009; Belardinelli et al., 2012; Bagheri Hariri et al., 2013a].

To overcome this limitation, KABs have been extended lately with mechanisms to handle inconsistency [Calvanese et al., 2013b]. However, this has been done by defining adhoc execution semantics and corresponding ad-hoc verification techniques geared towards specific semantics for inconsistency management. Furthermore, it has been left open whether introducing inconsistency management in the rich setting of KABs, effectively leads to systems with a different level of expressive power. In this paper, we attack these issues by: (i) Proposing (standard) GKABs, which enrich KABs with a compact action language inspired by Golog [Levesque et al., 1997] that can be conveniently used to specify processes at a high-level of abstraction. As in KABs, standard GKABs still manage inconsistency naively. (ii) Defining a parametric execution semantic for GKABs that is able to elegantly accomodate a plethora of inconsistency-aware semantics based on the well-known notion of repair [Eiter and Gottlob, 1992; Bertossi, 2006; Lembo et al., 2010; Calvanese et al., 2010]. (iii) Providing several reductions showing that verification of sophisticated first-order temporal properties over inconsistency-aware GKABs can be recast as a corresponding verification problem over standard GKABs. (iv) Showing that verification of standard and inconsistency-aware GKABs can be addressed using known techniques, developed for standard KABs. Full proofs can be found in an extended technical report [Calvanese et al., 2015].

2 Preliminaries

We start by introducing the necessary technical preliminaries.

2.1 DL-LiteA

We fix a countably infinite set ∆ of individuals, acting as standard names. To model KBs, we use the lightweight logic DL-LiteA [Calvanese et al., 2007b; 2009], whose concepts and roles are built according to B ::= N | ∃R and R ::= P | P -, where N is a concept name, B a basic concept, P a role name, P - an inverse role, and R a basic role.

ADL-LiteA KB is a pair 〈T,A〉, where: (i) A is an Abox, i.e., a finite set of ABox assertions (or facts) of the formN(c1) or P(c1, c2), where c1, c2 are individuals. (ii) T = Tp ⊎ Tn ⊎ Tf is a TBox, i.e., a finite set constituted by a subset Tp of positive inclusion assertions of the form B1 ⊑ B2 and R1 ⊑ R2, a subset Tn of negative inclusion assertions of the form B1 ⊑ ¬B2 and R1 ⊑ ¬R2, and a subset Tf of functionality assertions of the form (funct R). We denote by ADOM(A) the set of individuals explicitly present in A.

We rely on the standard semantics of DLs based on FOL interpretations I = (∆I , ·I ), where cI ∈ ∆I , N I ⊆ ∆I , and P I ⊆ ∆I ×∆I . The semantics of the DL-LiteA constructs and of TBox and ABox assertions, and the notions of satisfaction and of model are as usual (see, e.g., [Calvanese et al., 2007b]). We say that A is T-consistent if 〈T,A〉 is satisfiable, i.e., admits at least one model. We also assume that all concepts and roles in T are satisfiable, i.e., for every concept N in T, there exists at least one model I of T such that N I is non-empty, and similarly for roles.

Queries. We use queries to access KBs and extract individuals of interest. 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), where each conj i(⃗x, ⃗ yi) is a conjunction of atoms, whose predicates are either concept/role names of T, or equality assertions involving variables ⃗x and ⃗yi, and/or individuals.

The (certain) answers of q over 〈T, A〉 are defined as the set ans(q, T, A) of substitutions σ of the free variables in q with inviduals 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 the empty substitution (corresponding to true), or the empty set (corresponding to false). We also consider the extension of UCQs named EQLLite(UCQ) [Calvanese et al., 2007a] (briefly, ECQs), that is, the FOL query language whose atoms are UCQs evaluated according to the certain answer semantics above. Formally, an ECQ over a TBox T is a (possibly open) formula of the form 1 :

where q is a UCQ, and [q] denotes the fact that q is evaluated under the (minimal) knowledge operator [Calvanese et al., 2007a]. 2 Intuitively, the certain answers ANS(Q, T,A) of an ECQ Q over 〈T, A〉 are obtained by computing the certain answers of the UCQs embedded in Q, then composing such answers through the FO constructs in Q (interpreting existential variables as ranging over ADOM(A)).

2.2 InconsistencyManagement in DLKBs

Retrieving certain answers from a KB makes sense only if the KB is consistent: if it is not, then each query returns all possible tuples of individuals of the ABox. In a dynamic setting where the ABox evolves over time, consistency is a too strong requirement, and in fact a number of approaches have been proposed to handle the instance-level evolution of KBs, managing inconsistency when it arises. Such approaches typically follow one of the two following two strategies: (i) inconsistencies are kept in the KBs, but the semantics of query answering is refined to take this into account (consistent query answering [Bertossi, 2006]); (ii) the extensional part of an inconsistent KB is (minimally) repaired so as to remove inconsistencies, and certain answers are then applied over the curated KB. In this paper, we follow the approach in [Calvanese et al., 2013b], and consequently focus on repair-based approaches. However, our results seamlessly carry over the setting of consistent query answering. We then recall the basic notions related to inconsistency management via repair, distinguishing approaches that repair an ABox and those that repair an update.

1 In this work we only consider domain independent ECQs.

2 We omit the square brackets for single-atomUCQs.

ABox repairs. Starting from the seminal work in [Eiter and Gottlob, 1992], in [Lembo et al., 2010] two approaches for repairing KBs are proposed: ABox repair (AR) and intersection ABox repair (IAR). In [Calvanese et al., 2013b], these approaches are used to handle inconsistency in KABs, and are respectively called bold-repair (b-repair) and certain-repair (c-repair). Formally, a b-repair of an ABox A w.r.t. a TBox T is a maximal T-consistent subset A′ of A, i.e.: (i) A′ ⊆ A, (ii) A′ is T-consistent, and (iii) there does not exists A′′ such that A′ ⊂ A′′ ⊆ A and A′′ is T-consistent. We denote by B-REP(T,A) the set of all b-repairs of 〈T,A〉. The c-repair of an ABox A w.r.t. a TBox T is the (unique) set C-REP(T,A) = ∩Ai∈B-REP(T,A)Ai of ABox assertions, obtained by intersecting all b-repairs.

Inconsistency in KB evolution. In a setting where the KB is subject to instance-level evolution, b- and c-repairs are computed agnostically from the updates: each update is committed, and only secondly the obtained ABox is repaired if inconsistent. In [Calvanese et al., 2010], a so-called bold semantics is proposed to apply the notion of repair to the update itself. Specifically, the bold semantics is defined over a consistent KB 〈T,A〉 and an instance-level update that comprises two ABoxes F - and F +, respectively containing those assertions that have to be deleted from and then added to A. It is assumed that F + is consistent with T , and that new assertions have "priority": if an inconsistency arises, newly introduced facts are preferred to those already present in A. Formally, the evolution of an ABox A w.r.t. a TBox T by F + and F -, written EVOL(T,A, F +, F -), is an ABox Ae = F + ∪ A′ , where (i) A′ ⊆ (A \ F -), (ii) F + ∪A′ is T-consistent, and (iii) there does not exists A′′ such that A′ ⊂ A′′ ⊆ (A \ F -) and F + ∪A′′ is T-consistent.

2.3 Knowledge and Action Bases

Knowledge and Action Bases (KABs) [Bagheri Hariri et al., 2013b] have been proposed as a unified framework to simultaneously account for the static and dynamic aspects of an application domain. This is done by combining a semantically-rich representation of the domain (via a DL KB), with a process that evolves the extensional part of such a KB, possibly introducing, through service calls, new individuals from the external world. We briefly recall the main aspects of KABs, by combining the framework in [Bagheri Hariri et al., 2013b] with the action specification formalism in [Montali et al., 2014].

We consider a finite set of distinguished individuals ∆0 ⊂ ∆, and a finite set F of functions representing service calls, which abstractly account for the injection of fresh individuals from ∆ into the system. A KAB is a tuple K = 〈T, A0, Γ, Π〉 where: (i) T is a DL-LiteA TBox that captures the intensional aspects of the domain of interest; (ii) A0 is the initial DLLiteA ABox, describing the initial configuration of data; (iii) Γ is a finite set of parametric actions that evolve the ABox; (iv) Π is a finite set of condition-action rules forming a process, which describes when actions can be executed, and with which parameters. We assume that ADOM(A0) ⊆ ∆0.

An action α ∈ Γ has the form α(⃗ p) : {e1, . . . , em}, where (i) α is the action name, (ii) ⃗ p are the input parameters, and (iii) {e1, . . . , em} is the set of effects. Each effect has the formQ(⃗x) ⇝ add F +, del F -, where: (i) Q(⃗x) is an ECQ, possibly mentioning individuals in ∆0 and action parameters ⃗ p. (ii) F + is a set of atoms (over the alphabet of T) to be added to the ABox, each having as terms: individuals in ∆0, action parameters ⃗ p, free variables ⃗x of Q, and service calls, represented as Skolem terms formed by applying a function f ∈ F to one of the previous kinds of terms. (iii) F - is a set of atoms (over the alphabet of T ) to be deleted from the ABox, each having as terms: individuals in ∆0, input parameters ⃗ p, and free variables of Q. We denote by EFF(α) the set of effects in α. Intuitively, action α is executed by grounding its parameters, and then applying its effects in parallel. Each effect instantiates the atoms mentioned in its head with all answers of Q, then issues the corresponding service calls possibly contained in F +, and substitutes them with the obtained results (which are individuals from∆). The update induced by α is produced by adding and removing the ground atoms so-obtained to/from the current ABox, giving higher priority to additions.

The process Π comprises a finite set of condition-action rules of the form Q(⃗x) ↦→ α(⃗x), where: α ∈ Γ is an action, and Q(⃗x) is an ECQ over T , whose terms are free variables ⃗x, quantified variables, and individuals in ∆0. Each conditionaction rule determines the instantiations of parameters with which to execute the action in its head over the current ABox.

The execution semantics of a KAB is given in terms of a possibly infinite-state transition system, whose construction depends on the adopted semantics of inconsistency [Calvanese et al., 2013b]. In general, the transition systems we consider are of the form 〈∆, T,Σ, s0, abox,⇒〉, where: (i) T is a DL-LiteA TBox; (ii) Σ is a (possibly infinite) 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; (v) ⇒ ⊆ Σ×Σ is a transition relation between pairs of states.

Following the terminology in [Calvanese et al., 2013b], we call S-KAB a KAB under the standard execution semantics of KABs, where inconsistency is naively managed by simply rejecting those updates that lead to an inconsistent state. The transition system Υ S K accounting for the standard execution semantics of KAB K is then constructed by starting from the initial ABox, applying the executable actions in all possible ways, and generating the (consistent) successor states by applying the corresponding updates, then iterating through this procedure. As for the semantics of service calls, in line with [Calvanese et al., 2013b] we adopt the deterministic semantics, i.e., services return always the same result when called with the same inputs. Nondeterministic services can be seamlessly added without affecting our technical results.

To ensure that services behave deterministically, the states of the transition system are also equipped with a service call map that stores the service calls issued so far, and their corresponding results. Technically, a service call map is a partial function m : SC → ∆, where SC = {sc(v1, . . . , vn) | sc/n ∈ F and {v1, . . . , vn} ⊆ ∆} is the set of (Skolem terms representing) service calls.

2.4 Verification Formalism

To specify sophisticated temporal properties to be verified over KABs, taking into account the system dynamics as well as the evolution of data over time, we rely on the µLEQL A logic, the FO variant of the µ-calculus defined in [Bagheri Hariri et al., 2013b]. µLEQL A combines the standard temporal operators of the µ-calculus with EQL queries over the states. FO quantification is interpreted with an active domain semantics, i.e., it ranges over those individuals that are explicitly present in the current ABox, and fully interacts with temporal modalities, i.e., it applies across states. The µLEQL A syntax is:

where Q is a possibly open EQL query that can make use of the distinguished individuals in ∆0, Z is a second-order variable denoting a predicate (of arity 0), 〈-〉Φ indicates the existence of a next state where Φ holds, and µ is the least fixpoint operator, parametrized with the free variables of its bounding formula. We make use of the following standard abbreviations: ∀x.Φ = ¬(∃x.¬Φ), Φ1∨Φ2 = ¬(¬Φ1∧¬Φ2), [-]Φ = ¬〈-〉¬Φ, and νZ.Φ = ¬µZ.¬Φ[Z/¬Z].

For the semantics of µLEQL A , which is given over transition systems of the form specified in Section 2.3, we refer to [Bagheri Hariri et al., 2013b]. Given a transition system Υ and a closed µLEQL A formula Φ, we call model checking verifying whether Φ holds in the initial state of Υ, written Υ |= Φ.

3 Golog-KABs and Inconsistency

In this section, we leverage on the KAB framework (cf. Section 2.3) and provide a twofold contribution. On the one hand, we enrich KABs with a high-level action language inspired by Golog [Levesque et al., 1997]. This allows modelers to represents processes much more compactly, and will be instrumental for the reductions discussed in Sections 4 and 5. On the other hand, we introduce a parametric execution semantics, which elegantly accomodates a plethora of inconsistencyaware semantics based on the notion of repair.

A Golog-KAB (GKAB) is a tuple G = 〈T, A0, Γ, δ〉, where T, A0, and Γ are as in standard KABs, and δ is the Golog program characterizing the evolution of the GKAB over time, using the atomic actions in Γ. For simplicity, we only consider a core fragment 3 of Golog based on the action language in [Calvanese et al., 2011], and define a Golog program as:

where: (1) ε is the empty program; (2) pick Q(⃗ p).α(⃗ p) is an atomic action invocation guarded by an ECQ Q, such that α ∈ Γ is applied by non-deterministically substituting its parameters ⃗ p with an answer of Q; (3) δ1|δ2 is a nondeterministic choice between programs; (4) δ1; δ2 is sequencing; (5) if ϕ then δ1 else δ2 and while ϕ do δ are conditional and loop constructs, using a boolean ECQ ϕ as condition.

3 The other Golog constructs, including non-deterministic iteration and unrestricted pick, can be simulated with the constructs considered here.

Execution Semantics. As for normal KABs, the execution semantics of a GKAB G is given in terms of a possibly infinite-state transition system ΥG, whose states are labelled with ABoxes. The states we consider, are tuples of the form 〈A, m, δ〉, where A is an ABox, m a service call map, and δ a program. Together, A and m constitute the data-state, which captures the result of the actions executed so far, together with the answers returned by service calls issued in the past. Instead, δ is the process-state, which represents the program that still needs to be executed from the current data-state.

We adopt the functional approach by Levesque [1984] in defining the semantics of action execution over G, i.e., we assume G provides two operations: (i) ASK, to answer queries over the current KB; (ii) TELL, to update the KB through an atomic action. Since we adopt repairs to handle inconsistency, the ASK operator corresponds to certain answers computation.

We proceed now to formally define TELL. Given an action invocation pick Q(⃗ p).α(⃗ p) and an ABox A, we say that substitution σ of parameters ⃗ p with individuals in ∆ is legal for α in A if ANS(Qσ, T,A) is true. If so, we also say that ασ is executable in A, and we define the sets of atoms to be added and deleted by pick Q(⃗ p).α(⃗ p) with σ in A as follows: ADDAασ = ⋃(Q⇝add F +,del F -) in EFF(α) ⋃ρ∈ANS(Qσ,T,A) F +σρ

In general, ADDAασ is not a proper set of facts, because it could contain (ground) service calls, to be substituted with corresponding results. We denote by CALLS(ADDAασ ) the set of ground service calls in ADDAασ , and by EVAL(ADDAασ ) the set of call substitutions with individuals in ∆, i.e., the set

Given two ABoxes A and A′ where A is assumed to be T-consistent, and two sets F + and F - of facts, we introduce a so-called filter relation to indicate that A′ is obtained fromA by adding the F + facts and removing the F - ones. To account for inconsistencies, the filter could drop some additional facts when producing A′ . Hence, a filter consists of tuples of the form 〈A, F +, F -, A′ 〉 satisfying ∅ ⊆ A′ ⊆ ((A\F -) ∪F +). In this light, filter relations provide an abstract mechanism to accommodate several inconsistency management approaches.

We now concretize TELL as follows. Given a GKAB G and a filter f, we define TELLf as the following relation over pairs of data-states in ΥG: tuple 〈〈A,m〉, ασ, 〈A′ ,m′ 〉〉 ∈ TELLf if

• σ is a legal parameter substitution for α in A, and
• there exists θ ∈ EVAL(ADDAασ ) such that: (i) θ and m agree on the common values in their domains (this enforces the deterministic semantics for services); (ii) m′ = m ∪ θ; (iii) 〈A, ADDAασ θ, DELAασ ,A′ 〉 ∈ f, where ADDAασ θ denotes the set of facts obtained by applying θ over the atoms in ADDAασ ; (iv) A′ is T-consistent.

As a last preliminary notion towards the parametric execution semantics of GKABs, we specify when a state 〈A, m, δ〉 is considered to be final by its program δ, written 〈A, m, δ〉 ∈ F. This is done by defining the set F of final states as follows:

1. 〈A,m, ε〉 ∈ F;
2. 〈A,m, δ1|δ2〉 ∈ F if 〈A,m, δ1〉 ∈ F or 〈A,m, δ2〉 ∈ F;
3. 〈A,m, δ1; δ2〉 ∈ F if 〈A,m, δ1〉 ∈ F and 〈A,m, δ2〉 ∈ F;
4. 〈A,m, if ϕ then δ1 else δ2〉 ∈ F if ANS(ϕ, T, A) = true, and 〈A, m, δ1〉 ∈ F;
5. 〈A,m, if ϕ then δ1 else δ2〉 ∈ F if ANS(ϕ, T, A) = false, and 〈A, m, δ2〉 ∈ F;
6. 〈A,m,while ϕ do δ〉 ∈ F if ANS(ϕ, T,A) = false;
7. 〈A,m,while ϕ do δ〉 ∈ F if ANS(ϕ, T,A) = true, and 〈A, m, δ〉 ∈ F.

Now, given a filter relation f , we define the program execution relation ασ,f ---→, describing how an atomic action with parameters simultaneously evolves the data- and program-state:

Given a GKAB G = 〈T,A0, Γ, δ〉 and a filter relation f, we finally define the transition system of G w.r.t. f, written Υ f G , as 〈∆, T,Σ, s0, abox,⇒〉, where s0 = 〈A0, ∅, δ〉, and Σ and ⇒ are defined by simultaneous induction as the smallest sets such that s0 ∈ Σ, and if 〈A,m, δ〉 ∈ Σ and 〈A,m, δ〉 ασ,f ---→ 〈A′ ,m′ , δ′ 〉, then 〈A′ ,m′ , δ′ 〉 ∈ Σ and 〈A, m, δ〉 ⇒ 〈A′ , m′ , δ′ 〉. By suitbably concretizing the filter relation, we can obtain a plethora of execution semantics.

Standard and Inconsistency-Aware Semantics. Given a GKAB G = 〈T,A0, Γ, δ〉, we exploit filter relations to define its standard execution semantics (reconstructing that of [Calvanese et al., 2013b] for normal KABs), and three inconsistency-aware semantics that incorporate the repair-based approaches reviewed in Section 2.2. In particular, we introduce 4 filter relations fS, fB, fC, fE, as follows. Given an ABox A, an atomic action α(⃗ p) ∈ Γ, a legal parameter substitution σ for α in A, and a service call evaluation θ ∈ EVAL(ADDAασ ), let F + = ADDAασ θ and F - = DELAασ . We then have 〈A, F +, F -,A′ 〉 ∈ f, where

Filter fS gives rise to the standard execution semantics for G, since it just applies the update induced by the ground atomic action ασ (giving priority to additions over deletions). Filter fB gives rise to the b-repair execution semantics for G, where inconsistent ABoxes are repaired by non-deterministically picking a b-repair. Filter fC gives rise to the c-repair execution semantics for G, where inconsistent ABoxes are repaired by computing their unique c-repair. Filter fE gives rise to the b-evol execution semantics for G, where for updates leading to inconsistent ABoxes, their unique bold-evolution is computed. We call the GKABs adopting these semantics S-GKABs, B-GKABs, C-GKABs, and E-GKABs, respectively, and we group the last three forms of GKABs under the umbrella of inconsistency-aware GKABs (I-GKABs).

Transforming S-KABs to S-GKABs. We close this section by showing that our S-GKABs are able to capture normal SKABs in the literature [Bagheri Hariri et al., 2013b; Calvanese et al., 2013b]. In particular, we show the following.

Theorem 1. Verification of µLEQL A properties over S-KABs can be recast as verification over S-GKABs.

Proof sketch. We provide a translation τS that, given an SKAB K = 〈T, A0, Γ, Π〉 with transition system Υ S K , generates an S-GKAB τS(K) = 〈T,A0, Γ, δ〉. Program δ is obtained from Π as δ = while true do (a1|a2| . . . |a|Π|), where, for each condition-action rule Qi(⃗x) ↦→ αi(⃗x) ∈ Π, we have ai = pick Qi(⃗x).αi(⃗x). The translation produces a program that continues forever to non-deterministically pick an executable action with parameters (as specified by Π), or stops if no action is executable. It can be then proven directly that for every µLEQL A property Φ, Υ S K |= Φ iff Υ fS τS(K) |= Φ.

4 Compilation of InconsistencyManagement

This section provides a general account of inconsistency management in GKABs, proving that all inconsistency-aware variants introduced in Section 3 can be reduced to S-GKABs.

Theorem 2. Verification of µLEQL A properties over I-GKABs can be recast as verification over S-GKABs.

The remainder of this section is devoted to prove this result, case by case. Our general strategy is to show that S-GKABs are sufficiently expressive to incorporate the repair-based approaches of Section 2.2, so that an action executed under a certain inconsistency semantics can be compiled into a Golog program that applies the action with the standard semantics, and then explicitly handles the inconsistency, if needed.

We start by recalling that checking whether a DL-LiteA KB 〈T,A〉 is inconsistent is FO rewritable, i.e., can be reduced to evaluating a boolean query QTunsat over A (interpreted as a database) [Calvanese et al., 2007b]. To express such queries compactly, we make use of the following abbreviations. For role R = P -, atom R(x, y) denotes P(y, x). For concept B = ∃P, atom B(x) denotes P(x, ), where ' ' stands for an anonymous existentially quantified variable. Similarly, for B = ∃P -, atom B(x) denotes P( , x).

In particular, the boolean query QTunsat is:

where:

• qf unsat((funct R), x, y, z) = R(x, y)∧R(x, z)∧¬[y = z];
• qn unsat (B1 ⊑ ¬B2, x) = B1(x) ∧ B2(x);
• qn unsat (R1 ⊑ ¬R2, x, y) = R1(x, y) ∧ R2(x, y).

4.1 FromB-GKABs to S-GKABs

To encode B-GKABs into S-GKABs, we use a special fact M(rep) to distinguish stable states, where an atomic action can be applied, from intermediate states used by the S-GKABs to incrementally remove inconsistent facts from the ABox. Stable/repair states are marked by the absence/presence of M(rep). To set/unset M(rep), we define set Γrep = {α+ rep (), αrep ()} of actions, where α+ rep () : {true ⇝ add {M(rep)}}, and αrep () : {true ⇝ del {M(rep)}}.

Given a B-GKAB G = 〈T,A0, Γ, δ〉, we define the set ΓTb of b-repair actions and the set ΛTb of b-repair atomic action invocations as follows. For each functionality assertion (funct R) ∈ T, we include in ΓTb and ΛTb respectively:

• αF (x, y) : {R(x, z) ∧¬[z = y] ⇝ del {R(x, z)}} ∈ ΓTb This invocation repairs an inconsistency related to (funct R) by removing all tuples causing the inconsistency, except one. For each negative concept inclusion B1 ⊑ ¬B2 s.t. T |= B1 ⊑ ¬B2, we include in ΓTb and ΛTb respectively:
• pick ∃z.qf unsat((funct R), x, y, z).αF (x, y) ∈ ΛTb , and
• pick qn unsat (B1 ⊑ ¬B2, x).αB1 (x) ∈ ΛTb , and
• αB1 (x) : {true ⇝ del {B1(x)}} ∈ ΓTb

This invocation repairs an inconsistency related to B1 ⊑ ¬B2 by removing an individual that is both in B1 and B2 from B1. Similarly for negative role inclusions. Given ΛTb = {a1, . . . , an}, we then define the b-repair program

Intuitively, δT b iterates while the ABox is inconsistent, and at each iteration, non-deterministically picks one of the sources of inconsistency, and removes one or more facts causing it. Consequently, the loop is guaranteed to terminate, in a state that corresponds to one of the b-repairs of the initial ABox.

With this machinery at hand, we are ready to define a translation τB that, given G, produces S-GKAB τB(G) = 〈Tp, A0, Γ∪ΓTb ∪Γrep, δ′ 〉, where only the positive inclusion assertions Tp of the original TBox T are maintained (guaranteeing that τB(G) never encounters inconsistency). Program δ′ is obtained from program δ of G by replacing each occurrence of an atomic action invocation pick Q(⃗ p).α(⃗ p) with

pick Q(⃗ p).α(⃗ p); pick true.α+ rep (); δT b ; pick true.αrep () This program concatenates the original action invocation with a corresponding "repair" phase. Obviously, this means that when an inconsistent ABox is produced, a single transition in G corresponds to a sequence of transitions in τB(G). Hence, we need to introduce a translation tB that takes a µLEQL A formula Φ over G and produces a corresponding formula over τB(G). This is done by first obtaining formula Φ′ = NNF(Φ), where NNF(Φ) denotes the negation normal form of Φ. Then, every subformula of Φ of the form 〈-〉Ψ becomes 〈-〉〈-〉µZ.((M(rep)∧〈-〉Z)∨(¬M(rep)∧tB(Ψ))), so as to translate a next-state condition over G into reachability of the next stable state over τB(G). Similarly for [-]Ψ.

With these two translations at hand, we can show that Υ fB G |= Φ iff Υ fS τB(G) |= tB(Φ).

4.2 FromC-GKABs to S-GKABs

Making inconsistency management for C-GKABs explicit requires just a single action, which removes all individuals that are involved in some form of inconsistency. Hence, given a TBox T , we define a 0-ary c-repair action αT c , where EFF(αT c ) is the smallest set containing the following effects:

• for each assertion (funct R) ∈ T , qf unsat((funct R), x, y, z) ⇝ {del {R(x, y), R(x, z)}}
• for each assertion B1 ⊑ ¬B2 s.t. T |= B1 ⊑ ¬B2, qn unsat (B1 ⊑ ¬B2, x) ⇝ {del {B1(x), B2(x)}};
• similarly for negative role inclusions.

Notice that all effects are guarded by queries that extract only individuals involved in an inconsistency. Hence, other facts are kept unaltered, which also means that αT c is a no-op when applied over a T-consistent ABox. We define a translation τC that, given a C-GKAB G = 〈T,A0, Γ, δ〉, generates an S-GKAB τC(G) = 〈Tp, A0, Γ ∪ {αT c }, δ′ 〉, which, as for BGKABs, only maintains positive inclusion assertions of T. Program δ′ is obtained from δ by replacing each occurrence of an atomic action invocation of the form pick Q(⃗ p).α(⃗ p) with pick Q(⃗ p).α(⃗ p); pick true.αT c (). This attests that each transition in G corresponds to a sequence of two transitions in τC(G): the first mimics the action execution, while the second computes the c-repair of the obtained ABox.

A µLEQL A property Φ over G can then be recast as a corresponding property over τC(G) that substitutes each subformula 〈-〉Ψ of Φ with 〈-〉〈-〉Ψ (similarly for [-]Φ). By denoting this translation with tdup, we get Υ fC G |= Φ iff Υ fS τC(G) |= tdup(Φ).

4.3 FromE-GKABs to S-GKABs

Differently from the case of B-GKABs and C-GKABs, EGKABs pose two challenges: (i) when applying an atomic action (and managing the possibly arising inconsistency) it is necessary to distinguish those facts that are newly introduced by the action from those already present in the system; (ii) the evolution semantics can be applied only if the facts to be added are consistent with the TBox, and hence an additional check is required to abort the action execution if this is not the case. To this aim, given a TBox T , we duplicate concepts and roles in T , introducing a fresh concept name N n for every concept name N in T (similarly for roles). The key idea is to insert those individuals that are added to N also in N n , so as to trace that they are part of the update.

The first issue described above is then tackled by compiling the bold evolution semantics into a 0-ary evolution action αT e , where EFF(αT e ) is the smallest set of effects containing:

• for each assertion (funct R) ∈ T ,
• ∃z.qf unsat((funct R), x, y, z)∧Rn (x, y) ⇝ {del {R(x, z)}} · for each assertion B1⊑ ¬B2 s.t. T |= B1 ⊑ ¬B2, qn unsat (B1 ⊑ ¬B2, x) ∧ Bn 1 (x) ⇝ {del {B2(x)}};
• similarly for negative role inclusion assertions;
• for each concept name N, N n (x) ⇝ {del {N n (x)}};
• similarly for role names.

These effects mirror those of Section 4.2, with the difference that they asymmetrically remove old facts when inconsistency arises. The last two bullets guarantee that the content of concept and role names tracking the newly added facts are flushed. We then define a translation τE that, given an E-GKAB G = 〈T, A0, Γ, δ〉, generates an S-GKAB τE(G) = 〈Tp ∪ T n , A0, Γ′ ∪ {αT e }, δ′ 〉, where:

• T n is obtained from T by renaming each concept name N in T into N n (similarly for roles). In this way, the original concepts/roles are only subject in τE(G) to the positive inclusion assertions of T, while concepts/roles tracking newly inserted facts are subject also to negative constraints. This blocks the generation of the successor state when the facts to be added to the current ABox are T -inconsistent.
• Γ′ is obtained by translating each action in α(⃗ p) ∈ Γ into action α′ (⃗ p), such that for each effect Q ⇝ add F +, del F - ∈ EFF(α), we have Q ⇝ add F + ∪ F +n , del F - ∈ EFF(α′ ) where F +n duplicates F + by using the vocabulary for newly introduced facts.
• δ′ is obtained from δ by replacing each action invocation pick Q(⃗ p).α(⃗ p) with pick Q(⃗ p).α′ (⃗ p); pick true.αT e ().

By exploiting the same µLEQL A translation used in Section 4.2, we obtain that Υ fE G |= Φ iff Υ fS τE(G) |= tdup(Φ).

5 FromGolog to Standard KABs

We close our tour by showing that S-GKABs can be compiled into the normal S-KABs of [Bagheri Hariri et al., 2013b; Calvanese et al., 2013b].

Theorem 3. Verification of µLEQL A properties over S-GKABs can be recast as verification over S-KABs.

Proof sketch. We introduce a translation from S-GKABs to S-KABs, and from µLEQL A properties over S-GKABs to corresponding properties over S-KABs, in such a way that verification in the first setting can be reduced to verification in the second setting. The translation is quite involved, so for space reasons we refer to [Calvanese et al., 2015] for details.

From Theorems 1 and 3, we obtain that S-KABs and SGKABs are expressively equivalent. From Theorems 2 and 3, we get our second major result: inconsistency-management can be compiled into an S-KAB by concatenating the two translations from I-GKABs to S-GKABs, and then to S-KABs.

Theorem 4. Verification of µLEQL A properties over I-GKABs can be recast as verification over S-KABs.

Even more interesting is the fact that the semantic property of run-boundedness [Bagheri Hariri et al., 2013a; 2013b] is preserved by all translations presented in this paper. Intuitively, run-boundedness requires that every run of the system cumulatively encounters at most a bounded number of individuals. Unboundedly many individuals can still be present in the overall system, provided that they do not accumulate in the same run. Thanks to the preservation of run-boundedness, and to the compilation of I-GKABs into S-KABs, we get:

Theorem 5. Verification of µLEQL A properties over runbounded I-GKABs is decidable, and reducible to standard µ-calculus finite-state model checking.

Proof sketch. The claim follows by combining the fact that all translations preserve run-boundedness, Theorem 4, and the results in [Bagheri Hariri et al., 2013a; 2013b] for runbounded S-KABs.

6 Conclusion

We introduced GKABs, which extend KABs with Gologinspired high-level programs, and provided a parametric execution semantics supporting an elegant treatment of inconsistency. We have shown that verification of rich temporal properties over (inconsistency-aware) GKABs can be recast as verification over standard KABs, by encoding the semantics of inconsistency in terms of Golog programs and specific inconsistency-management actions, and Golog programs into standard KAB condition-action rules. An overview of our reductions is depicted below. Our approach is very general, and can be seamlessly extended to account for other mechanisms for handling inconsistency, and more in general data cleaning.

Acknowledgments. This research has been partially supported by the EU IP project Optique (Scalable End-user Access to Big Data), grant agreement n. FP7-318338, and by the UNIBZ internal project KENDO (Knowledge-driven ENterprise Distributed cOmputing).