We introduce description logic (DL) Knowledge and Action Bases (KAB), a mechanism that provides both 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. We resort to a variant of DL-Lite where UNA is not enforced and where equality between objects may be asserted and inferred. Actions are specified as sets of conditional effects, where conditions are based on epistemic queries over the KB (TBox and ABox), and effects are expressed in terms of new ABoxes. We address the verification of temporal properties expressed in a variant of first-order μ-calculus where a controlled form of quantification across states is allowed. Notably, we show decidability of verification, under a suitable restriction inspired by the notion of weak acyclicity in data exchange.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com