Verification of Context-Sensitive Knowledge and Action Bases

Proc. of the 14th European Conf. on Logics in Artificial Intelligence (JELIA 2014). Volume 8761 of Lecture Notes in Computer Science. 2014.

Knowledge and Action Bases (KABs) have been recently proposed as a formal framework to capture the dynamics of systems which manipulate over time Description Logic (DL) Knowledge Bases (KBs) through action execution. In this work, we enrich the KAB setting with contextual information, making use of different context dimensions. On the one hand, context is determined by the environment using context-changing actions that make use of the current state of the KB and the current context. On the other hand, it affects the set of TBox assertions that are relevant at each time point, and that have to be considered when processing queries posed over the KAB. Here we extend to our enriched setting the results on verification of rich temporal properties expressed in #-calculus, which had been established for standard KABs. Specifically, we show that under a run-boundedness condition, verification stays decidable. We also show how to extend syntactic conditions ensuring run-boundedness to the presence of contextual information, taking into account context-dependent activation of TBox assertions.

@inproceedings{JELIA-2014-kabs,
   title = "Verification of Context-Sensitive Knowledge and Action Bases",
   year = "2014",
   author = "Diego Calvanese and Ismail Ilkan Ceylan and Marco Montali and
Ario Santoso",
   booktitle = "Proc. of the 14th European Conf. on Logics in Artificial
Intelligence (JELIA 2014)",
   pages = "514--528",
   volume = "8761",
   publisher = "Springer",
   series = "Lecture Notes in Computer Science",
   doi = "10.1007/978-3-319-11558-0_36",
}