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 ?-calculus. Notably, we show decidability of verification, under a suitable restriction inspired by the notion of acyclicity in data exchange.
Verification of conjunctive-query based semantic artifacts? / Babak Bagheri, Hariri; Diego, Calvanese; DE GIACOMO, Giuseppe; DE MASELLIS, Riccardo. - 745:(2011), pp. 48-58. (Intervento presentato al convegno 24th International Workshop on Description Logics, DL 2011 tenutosi a Barcelona nel 13 July 2011 through 16 July 2011).
Verification of conjunctive-query based semantic artifacts?
DE GIACOMO, Giuseppe;DE MASELLIS, RICCARDO
2011
Abstract
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 ?-calculus. Notably, we show decidability of verification, under a suitable restriction inspired by the notion of acyclicity in data exchange.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
