Verification of Inconsistency-Aware Knowledge and Action Bases

摘要

Description Logic Knowledge and Action Bases (KABs) 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 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,the established framework treats inconsistency in a simplistic way,by rejecting inconsistent states produced through action execution.We address this problem by showing how inconsistency handling based on the notion of repairs can be integrated into KABs,resorting to inconsistency-tolerant semantics.In this setting,we establish decidability and complexity of verification.