=Paper= {{Paper |id=Vol-1350/paper-17 |storemode=property |title=Inconsistency Management in Generalized Knowledge and Action Bases |pdfUrl=https://ceur-ws.org/Vol-1350/paper-17.pdf |volume=Vol-1350 |dblpUrl=https://dblp.org/rec/conf/dlog/CalvaneseMS15 }} ==Inconsistency Management in Generalized Knowledge and Action Bases== https://ceur-ws.org/Vol-1350/paper-17.pdf
                   Inconsistency Management in
              Generalized Knowledge and Action Bases? .

                     Diego Calvanese, Marco Montali, and Ario Santoso

                         Free University of Bozen-Bolzano, Bolzano, Italy
                                 lastname@inf.unibz.it



1      Introduction
The combination of static and dynamic aspects in modeling complex organizational
domains is a challenging task that has led to study the combination of formalisms
from knowledge representation, database theory, and process management [18,23,11].
Specifically, Knowledge and Action Bases (KABs) [3] have been put forward recently
to provide a semantically rich representation of a domain. In KABs, static aspects are
modeled using a Description Logic (DL) [1] knowledge base (KB), while actions are
used to evolve its extensional part over time, possibly introducing fresh individuals.
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, both in KABs and
in related approaches, is typically handled naively by just rejecting updates in actions
when they would lead to inconsistency, see e.g., [16,4,9,2].
     To overcome this limitation, KABs have been extended lately with mechanisms to
handle inconsistency [12]. However, this has been done by defining ad-hoc execution
semantics and corresponding ad-hoc verification techniques geared towards specific
semantics for inconsistency management. It has also been left open whether adding
inconsistency management to the rich setting of KABs, actually increases expressive
power. This work attacks these issues by: (i) Proposing (standard) GKABs, which enrich
KABs with a compact action language inspired by Golog [20] 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 se-
mantics based on the well-known notion of repair [17,5,19,13]. (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.


2      Setting
We use DL-LiteA [8,6] to express KBs, and consider queries such as EQL-Lite(UCQ)
(briefly ECQs) [7], to access KBs and extract individuals of interest. To handle inconsis-
 ?
     This paper is an abridged version of [14]. Full proofs can be found in [15]
tency in KBs, we follow the repair-based approaches in [12], and distinguish between
two kinds of approaches: (i) those that compute repairs agnostically from the updates
(the added/deleted facts) [19,12], among which we have b-repairs, which are defined
as the maximal (w.r.t. set containment) subsets of an ABox that are consistent with the
TBox, and c-repairs, which are defined as the intersection of all b-repairs; (ii) those that
take into account the updates by giving higher priority to the new facts during the repair,
as in bold semantics for instance-level KB evolution (c.f., [13]).
    Here, we consider KABs that are obtained by combining the framework in [3,12]
with the action specification formalism in [22], which allows us to have actions that
only update an ABox (instead of creating a new ABox at each execution, as in [3,12]).
Formally, a KAB is composed by (i) a DL-LiteA TBox T ; (ii) an initial DL-LiteA
ABox A0 ; (iii) a finite set Γ of parametric actions that evolve the ABox; (iv) a finite
set Π of condition-action rules that describe when actions can be executed, and with
which parameters. 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 [12]. As in [12], we call S-KAB a KAB under the standard execution
semantics, where inconsistency is naively managed by simply rejecting those updates
that lead to an inconsistent state.
    To specify temporal properties over KABs, we use the µLEQL  A    logic, the FO variant
of µ-calculus defined in [3]. Given a transition system Υ and a closed µLEQLA    formula Φ,
verification is the problem of checking whether Φ holds in the initial state of Υ.


3   Golog-KABs and Inconsistency Management

We enrich KABs with a high-level action language inspired by Golog [20]. This allows
modelers to represents the dynamics of systems much more compactly. On the other
hand, we introduce a parametric execution semantics, which elegantly accommodates
the different kinds of inconsistency-aware semantics based on the notion of repair.
     A Golog-KAB (GKAB) is a tuple G = hT, A0 , Γ, δi, 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 of Golog based on the action language in [10], and define a Golog program as:
  δ ::= ε | pick Q(~    p).α(~p) | δ1 |δ2 | δ1 ; δ2 | if ϕ then δ1 else δ2 | while ϕ do δ
where: (i) ε is the empty program; (ii) 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; (iii) δ1 |δ2 is a non-deterministic choice between
programs; (iv) δ1 ; δ2 is sequencing; (v) if ϕ then δ1 else δ2 , and while ϕ do δ are
respectively conditional and loop constructs, using a boolean ECQ ϕ as condition.
     We adopt the functional approach by [21] in defining the semantics of action exe-
cution 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. Here the ASK
operator corresponds to certain answers computation. The TELL operation is parameter-
ized by filter relations f , which are used to refine the way in which an ABox is updated,
based on a set of facts to be added and deleted (specified by the action), and we require
that the result of the TELL operation is a T -consistent ABox. In this light, filter relations
provide an abstract mechanism to accommodate several inconsistency management
approaches in the execution semantics. For instance, we define GKABs with standard
execution semantics, briefly S-GKABs, by defining a filter relation fS that updates an
ABox based on the facts to be added and deleted, and does nothing w.r.t. inconsistency
(i.e., updates that lead to an inconsistent state are simply rejected). To obtain GKABs
with inconsistency-aware semantics, we introduce filter relations fB , fC , and fE , where
fB (resp., fC ) returns a b-repair (resp., c-repair) [12] of the updated ABox, and fE
updates the ABox using the bold semantics of KB evolution [13]. Consecutively, we
call the GKABs adopting the execution semantics obtained by employing those filter
relations B-GKABs, C-GKABs, and E-GKABs, respectively, and we group them under
the umbrella of inconsistency-aware GKABs (I-GKABs).
Verification Results. With respect to verification of µLEQL
                                                          A    properties, we have proved
the results summarized below, where an arrow indicates that we can reduce verification
in (G)KABs in the source to verification in (G)KABs in the target:
                           B-GKABs C-GKABs        E-GKABs

                                      S-GKABs           S-KABs
     To encode S-KABs into S-GKABs, we simulate the standard execution semantics
using a Golog program that continues forever to non-deterministically pick an executable
action with parameters, or stops if no action is executable. For the opposite direction, the
key idea is to inductively interpret a Golog program as a structure consisting of nested
processes, suitably composed through the Golog operators. We mark the starting and
ending point of each Golog subprogram, and use accessory facts in the ABox to track
states corresponding to subprograms. Each subprogram is then inductively translated
into a set of actions and condition-action rules encoding its entrance and termination
conditions. For all reductions from I-GKABs to S-GKABs, our general strategy is to show
that S-GKABs are sufficiently expressive to incorporate the repair-based approaches, 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.
     It is also interesting to observe that the semantic property of run-boundedness (which
guarantees the decidability of S-KAB verification) [2,3] is preserved by all our reductions.
It follows that verification of µLEQLA   properties over run-bounded GKABs and I-GKABs
is decidable, and reducible to standard µ-calculus finite-state model checking.

4   Conclusion
We introduced GKABs, which extend KABs with Golog-inspired high-level programs,
and allow for an elegant treatment of inconsistency. We have also shown that verification
of rich temporal properties over (inconsistency-aware) GKABs can be recast as verifica-
tion over standard KABs. Our approach is very general, and can be easily extended to
account for other inconsistency handling mechanisms, 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).
References
 1. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The De-
    scription Logic Handbook: Theory, Implementation and Applications. Cambridge University
    Press (2003)
 2. Bagheri Hariri, B., Calvanese, D., De Giacomo, G., Deutsch, A., Montali, M.: Verification of
    relational data-centric dynamic systems with external services. In: Proc. of the 32nd ACM
    SIGACT SIGMOD SIGAI Symp. on Principles of Database Systems (PODS). pp. 163–174
    (2013)
 3. Bagheri Hariri, B., Calvanese, D., Montali, M., De Giacomo, G., De Masellis, R., Felli, P.:
    Description logic Knowledge and Action Bases. J. of Artificial Intelligence Research 46,
    651–686 (2013)
 4. Belardinelli, F., Lomuscio, A., Patrizi, F.: An abstraction technique for the verification of
    artifact-centric systems. In: Proc. of the 13th Int. Conf. on the Principles of Knowledge
    Representation and Reasoning (KR). pp. 319–328 (2012)
 5. Bertossi, L.E.: Consistent query answering in databases. SIGMOD Record 35(2), 68–76
    (2006)
 6. 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), Lecture Notes in Computer Science, vol. 5689, pp. 255–356.
    Springer (2009)
 7. 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). pp. 274–279 (2007)
 8. 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)
 9. 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). Lecture Notes in Computer Science, vol. 7497, pp. 25–41. Springer
    (2012)
10. Calvanese, D., De Giacomo, G., Lenzerini, M., Rosati, R.: Actions and programs over
    description logic knowledge bases: A functional approach. In: Lakemeyer, G., McIlraith,
    S.A. (eds.) Knowing, Reasoning, and Acting: Essays in Honour of Hector Levesque. College
    Publications (2011)
11. Calvanese, D., De Giacomo, G., Montali, M.: Foundations of data aware process analysis: A
    database theory perspective. In: Proc. of the 32nd ACM SIGACT SIGMOD SIGAI Symp. on
    Principles of Database Systems (PODS) (2013)
12. Calvanese, D., Kharlamov, E., Montali, M., Santoso, A., Zheleznyakov, D.: Verification of
    inconsistency-tolerant knowledge and action bases. In: Proc. of the 23rd Int. Joint Conf. on
    Artificial Intelligence (IJCAI) (2013)
13. Calvanese, D., Kharlamov, E., Nutt, W., Zheleznyakov, D.: Evolution of DL-Lite knowledge
    bases. In: Proc. of the 9th Int. Semantic Web Conf. (ISWC). Lecture Notes in Computer
    Science, vol. 6496, pp. 112–128. Springer (2010)
14. Calvanese, D., Montali, M., Santoso, A.: Verification of generalized inconsistency-aware
    knowledge and action bases. In: Proc. of the 24th Int. Joint Conf. on Artificial Intelligence
    (IJCAI) (2015)
15. Calvanese, D., Montali, M., Santoso, A.: Verification of generalized inconsistency-aware
    knowledge and action bases (extended version). CoRR Technical Report arXiv:1504.08108,
    arXiv.org e-Print archive (2015), available at http://arxiv.org/abs/1504.08108
16. 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). pp. 252–267 (2009)
17. Eiter, T., Gottlob, G.: On the complexity of propositional knowledge base revision, updates
    and counterfactuals. Artificial Intelligence 57, 227–270 (1992)
18. Hull, R.: Artifact-centric business process models: Brief survey of research results and chal-
    lenges. In: Proc. of the 7th Int. Conf. on Ontologies, DataBases, and Applications of Semantics
    (ODBASE). Lecture Notes in Computer Science, vol. 5332, pp. 1152–1163. Springer (2008)
19. 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). pp. 103–117 (2010)
20. Levesque, H.J., Reiter, R., Lesperance, Y., Lin, F., Scherl, R.: GOLOG: A logic programming
    language for dynamic domains. J. of Logic Programming 31, 59–84 (1997)
21. Levesque, H.J.: Foundations of a functional approach to knowledge representation. Artificial
    Intelligence 23, 155–212 (1984)
22. Montali, M., Calvanese, D., De Giacomo, G.: Verification of data-aware commitment-based
    multiagent systems. In: Proc. of the 13th Int. Conf. on Autonomous Agents and Multiagent
    Systems (AAMAS). pp. 157–164 (2014)
23. Vianu, V.: Automatic verification of database-driven systems: a new frontier. In: Proc. of the
    12th Int. Conf. on Database Theory (ICDT). pp. 1–13 (2009)