Verification of Conjunctive-Query Based Semantic Artifacts

Proc. of the 24th Int. Workshop on Description Logics (DL 2011). Volume 745 of CEUR Workshop Proceedings, https://ceur-ws.org/. 2011.

We introduce semantic artifacts, which are a mechanism that provides both a semantically rich representation of the information on the domain of interest in terms of an ontology, including the underlying data, and a set of actions to change such information over time. In this paper, the ontology is specified as a DL-Lite TBox together with an ABox that may contain both (known) constants and unknown individuals (labeled nulls, represented as Skolem terms). Actions are specified as sets of conditional effects, where conditions are based on conjunctive queries over the ontology (TBox and ABox), and effects are expressed in terms of new ABoxes. In this setting, which is obviously not finite state, we address the verification of temporal/dynamic properties expressed in mu-calculus. Notably, we show decidability of verification, under a suitable restriction inspired by the notion of acyclicity in data exchange.

@inproceedings{DL-2011-artifacts,
   title = "Verification of Conjunctive-Query Based Semantic Artifacts",
   year = "2011",
   author = "Bagheri Hariri, Babak and Diego Calvanese and De Giacomo,
Giuseppe and De Masellis, Riccardo",
   booktitle = "Proc. of the 24th Int. Workshop on Description Logics
(DL 2011)",
   pages = "48--58",
   volume = "745",
   publisher = "CEUR-WS.org",
   series = "CEUR Workshop Proceedings, https://ceur-ws.org/",
}