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.