Verification of Description Logic Knowledge and Action Bases

Proc. of the 20th European Conf. on Artificial Intelligence (ECAI 2012). Volume 242 of Frontiers in Artificial Intelligence and Applications. 2012.

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 mu-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.

@inproceedings{ECAI-2012-kabs,
   title = "Verification of Description Logic Knowledge and Action Bases",
   year = "2012",
   author = "Bagheri Hariri, Babak and Diego Calvanese and Marco Montali
and De Giacomo, Giuseppe and De Masellis, Riccardo and Paolo Felli",
   booktitle = "Proc. of the 20th European Conf. on Artificial Intelligence
(ECAI 2012)",
   pages = "103--108",
   volume = "242",
   publisher = "IOS Press",
   series = "Frontiers in Artificial Intelligence and Applications",
   doi = "10.3233/978-1-61499-098-7-103",
}