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.
The artifact-centric approach to service modeling, introduced recently, considers both data and processes as first-class citizens in service design and analysis. Artifacts are advocated as a sort of middle ground between a conceptual formalization of a dynamic system and an actual implementation of the system itself [1]. The verification of temporal properties in the presence of data represents a significant challenge for the research community, since the system becomes infinite-state, and hence the usual analysis based on model checking of finite-state systems [2] is impossible in general. Recently, there have been some advancements on this issue, considering suitably constrained relational database settings for the data component (which acts also as a data storage for the process), see e.g., [3,4].
In this paper, we follow the line of [3], and rely on the work in knowledge representation to propose a more conceptual treatment of artifacts. We do so by enriching artifacts with a semantic layer constituted by a full-fledged ontology expressed in description logics. In particular, our semantic artifacts include an ontology specified in DL-Lite R [5], which is the core of the web ontology language OWL2 QL 1 , and it is particularly well suited for data management. The TBox of the ontology captures intensional information on the domain of interest, similarly to conceptual data models, such as UML class diagram, though as a software component to be used at runtime. The ABox, which acts as the artifact state, maintains the data of interest, which are accessed by relying on query answering through ontologies. As a query language, we use unions of conjunctive queries, possibly composing their certain answers through full FOL constructs [6]. A semantic artifact has associated actions whose execution changes the state of the artifact, i.e., its ABox. Such actions are specified as sets of conditional effects, where conditions are queries over the ontology and effects are expressed in terms of new ABoxes. To capture data that are acquired from external users/environments during the execution of actions, such ABoxes may contain special constants called labeled nulls, represented as Skolem terms. These represent individuals that the artifact does not know, but on which it knows some facts. Actions have no pre-condition, instead processes over the semantic artifact are used to specify which actions can be executed at each step. We model such processes as condition/action rules, where the condition is again expressed as a query over the ontology.
In this setting, which is obviously not finite state, we address the verification of temporal/dynamic properties expressed in µ-calculus [7], where atomic formulas are queries over the ontology that can refer only to known individuals. Unsurprisingly, we show that even for very simple semantic artifacts and dynamic properties verification is undecidable. However, we also show that for a very rich class of semantic artifacts, verification is indeed decidable and reducible to finite-state model checking. To obtain this result, we rely on recent results on the finiteness of the chase of tuple-generating dependencies in the data exchange literature [8].
As ontology language, we make use of DL-Lite R , a member of the DL-Lite family [5], and hence a tractable DL particularly suited for dealing with ontologies (or KBs) with very large ABoxes, which can be managed through relational database technology. DL-Lite R is also the core of the standard web ontology language OWL2 QL. In DL-Lite R , concepts and roles are formed according to the following syntax:
N , B, and C respectively denote a concept name, a basic concept, and an arbitrary concept. P , P − , U , and V respectively denote a role name, an inverse role, a basic role, and an arbitrary role. A DL-Lite R ontology is a pair (T, A), where T is a TBox, i.e., a finite set of (concept and role) inclusion assertions of the forms B C and U V ; and A is an ABox, i.e., a finite set of facts (also called membership assertions) of the forms N (c 1 ) and P (c 1 , c 2 ), where N and P occur in T , and c 1 and c 2 are constants. We denote with C A the set of constants appearing in A. The semantics of a DL-Lite R ontology is the usual one for DLs, see [5]. Notice that in DL-Lite R the unique name assumption is immaterial, since there is no way of deducing facts about equality. We say that A is consistent wrt T if (T, A) is satisfiable, i.e., admits at least one model.
A union of conjunctive queries (UCQ) q over a DL-Lite R TBox T and constants C is a FOL formula of the form ∃y 1 .conj 1 (x, y 1 ) ∨ • • • ∨ ∃y n .conj n (x, y n ), with free variables x, existentially quantified variables y 1 , . . . , y n . Each conj i (x, y i ) in q is a conjunction of atoms of the form N (z), P (z, z ), z = z , where N and P respectively denote a concept and a role name occurring in T , and z, z are constants in C or variables in x or y i , for some i ∈ {1, . . . , n}. Given constants C (typically C A ), the (certain-)answers to q over (T, A) wrt C is the set ans C (q, T, A) of substitutions2 θ of the free variables of q with constants in C such that qθ evaluates to true in every model of (T, A). We also consider an extension of UCQs, called ECQs, which are the range-restricted queries of the query language EQL-Lite(UCQ) [6], that is, the FOL query language whose atoms are UCQs evaluated according to the certain answer semantics above. Formally, an ECQ over T and C is a possibly open formula of the form
where q denotes a UCQ over T and C, with the proviso that every free variable of a negative subquery, i.e., of the form ¬Q, must occur in a positive subquery (to guarantee range-restriction). Given constants C the answer to Q over (T, A) wrt C, is the set ans C (Q, T, A) of tuples of constants in C obtained by evaluating the FOL formula Q in the standard way, while considering each UCQ q appearing in it as a primitive predicate with extension ans C (q, T, A). For the connection with epistemic logic, see [6].
A semantic artifact S = (T, A 0 , R) is a stateful device constituted by the information ontology (T, A 0 ) and the action specification R.
-T is a DL-Lite R TBox, fixed once and for all, and capturing the intensional knowledge about the domain modeled by the semantic artifact. -A 0 is a DL-Lite R ABox, which expresses extensional information, and constitutes the initial state of the artifact. We call proper constants the constants C A0 in A 0 , and labeled nulls all new constants introduced by action execution. -R is a set of actions, which change the state of the semantic artifact, i.e., the extensional information component. An action ρ is constituted by a signature and an effect specification. The action signature is constituted by a name and a list of individual input parameters. Such parameters need to be substituted by constants for the execution of the action. Given a substitution θ for the input parameters, we denote by ρθ the action with actual parameters. 3The effect specification consists of a set {e 1 , . . . , e n } of effects, which are assumed to take place simultaneously. Their formalization is inspired by the notion of mappings in data exchange [8]. Specifically, an effect e i has the form q + i ∧ Q − i A i where: q + i ∧ Q − i is a query over T and C A0 with x as free variables, that may include some of the input parameters as query constants, q + i is a UCQ, and Q − i is an arbitrary ECQ whose free variables are included in those of q + i , namely in x. Intuitively, q + i selects the tuples to instantiate the effect, and Q − i filters aways some of them. -A i is a set of facts over T , which include as constants: constants in C A0 , parameters, free variables of q + i , and implicitly existentially quantified variables. Given a state A of S, and a substitution σ for the parameters of the action ρ, the effect e i extracts from A the set ans
) of tuples of constants (proper constants and labeled nulls), and for each such tuple θ asserts a set A i σθ of facts obtained from A i σ by applying the substitution θ for the free variables of q + i . For each existentially quantified variable z in A i σ, a labeled null is introduced having the form f z,ei (x)σθ, where f z,ei (x) is a Skolem function, depending on the existential variable z and the effect e i , having as arguments the free variables x of q + i . We denote by e i σ(A) the overall set of facts, i.e., e i σ(A) = θ∈ans C A (Qiσ,T,A) A i σθ. The overall effect of the action ρ with parameter substitution σ over A is a new state do(ρσ, T, A) = 1≤i≤n e i σ(A) for S. Notice that do(ρσ, T, A) may be inconsistent wrt T . In this case, the action ρ with σ over A is not executable.
Let's make some observations on such actions. The effects of an action are naturally a form of update of the previous state, and not of belief revision [9]. That is, we never learn new facts on the state in which an action is executed, but only on the state resulting from the action execution. We also observe that existentially quantified variables introduced by actions effects are used as witnesses of values chosen by the external user/environment when executing the action. We assume that such a choice depends only on the specific effects and the information retrieved by the query in the premises. We model such a choice by introducing suitable labeled nulls generated by appropriate Skolem functions. Finally, we observe that we do not make any persistence (or frame) assumption in our formalization [10]. In principle at every move we substitute the whole old state, i.e., ABox, with a new one. On the other hand, it should be clear that we can easily write effect specifications that copy big chunks of the old state into the new one. For example, P (x, y) P (x, y) copies the entire set of assertions involving the role P .
Example 1. Let us consider a semantic artifact S = (T, A0, R), where T is the DL-LiteR formalization of the UML diagram in Figure 1, which can be described as follows. A bank considers two specific types of customers: in-debt customers have a loan with the bank, while gold customers have access to special privileges. In-debt customers may have closed their loan.
A relationship peer(c, p) between two customers denotes that p can vouch for c. The initial state is A0 = {Gold(john), Cust(ann), peer(mark, john)}. R includes the following actions (we use brackets to isolate UCQs in ECQs):
That is, customer c gets a loan provided that s/he has a peer that is "gold". We use CopyAll as a shortcut to denote effects that copy all concepts and roles.
That is, customer c closes all his/her loans which are moved to the closed relation.
That is, "remove" from owes those tuples that are in closed, and remove in-debt customers whose loans are all closed from InDebt, keeping them in Cust. CopyAllExceptOwesClosedInDebt copies everything except owes, closed, and InDebt.
Notice that semantic artifacts include information and actions to change such information. However, they do not say anything about how or when to apply a certain action. In other words, semantic artifact are agnostic to processes that use them. Processes over a semantic artifact S = (T, A 0 , R) are (possibly nondeterministic) programs that use the state of S (accessed through T ) to store their (intermediate and final) computation results, and the actions in R as atomic instructions. The state A can be arbitrarily queried through query answering over T , while it can be updated only through the actions in R. There are many ways to specify processes over S. Here we adopt a rule-based specification.
A condition/action rule π for a semantic artifact S is an expression of the form Q → ρ, where ρ is an action in R and Q is an ECQ over T and C A0 , whose free variables are exactly the parameters of ρ. Such a rule expresses that, for each tuple θ for which condition Q holds, the action ρ with actual parameters θ can be executed.
A process is a finite set Π = {π 1 , . . . , π n } of rules. Notice that processes don't force the execution of actions but constrain them: the user of the process will be able to choose any of the actions that the rules forming the process allow. Notice also that our processes inherit entirely their states from the semantic artifact S, see e.g., [1]. Other choices are also possible: the process could maintain its own state besides the one of the semantic artifact. As long as such an additional state is finite, or embeddable into the semantic artifact itself, the results here would easily extend to such a case.
The execution of a process Π over a semantic artifact S is defined as follows: we start from the initial state A 0 of the artifact, and for each rule Q → ρ in Π, evaluate Q, and for each tuple θ returned execute ρθ, obtaining a new state A = do(ρθ, T, A 0 ) if A is consistent wrt T (i.e., ρθ is actually executable), and so on. In this way we build a transition system Υ (Π, S) whose states represent possible artifact states and where each transition represents the execution of an instantiated action that is allowed according to the process. Υ (Π, S) captures the behavior of the process Π over the artifact S. In principle we can model-check such a transition system to verify dynamic properties. This is exactly what we are going to do next. However, one has to consider that in general such a transition system is infinite, so the classical results on model checking [2], which are developed for finite transition systems, do not apply.
Example 2. Referring to the example above, a process Π might include the following rules:
-[Cust(x)] ∧ ¬[∃y.owes(x, y)] → GetLoan(x), i.e., a customer can get a loan if she does not have one already; -∃y.([owes(x, y)] ∧ ¬[closed(x, y)]) → CloseAllLoans(x), i.e., a customer that owes loans that are not closed, can close them all at once; -true → UpdateDebts, i.e., it is always possible to perform UpdateDebts.
We turn to the verification formalism to be used to specify dynamic properties of processes running over semantic artifacts. Several choices are possible. Here we focus on a variant of µ-calculus [7], which is one of the most powerful temporal logics that subsumes both linear time logics, such as LTL and PSL, and branching time logics such as CTL and CTL* [2]. In particular, we introduce a variant of µ-calculus, called µL that conforms with the basic assumption of our formalism, namely the use of ECQs to talk about the semantic information contained in the state of the artifact. Formally, given a semantic artifact S = (T, A 0 , R), formulas of µL over S have the following form:
where Q is an ECQ over T and C A0 (but not labeled nulls), and Z is a predicate variable.
The symbols µ and ν can be considered as quantifiers, and we make use of the notions of scope, bound and free occurrences of variables, closed formulas, etc. The definitions of these notions are the same as in first-order logic, treating µ and ν as quantifiers. In fact, we are interested only in closed formulas as specification of temporal properties to verify. For formulas of the form µZ.Φ and νZ.Φ, we require the syntactic monotonicity of Φ wrt Z: every occurrence of the variable Z in Φ must be within the scope of an even number of negation signs. In µ-calculus, given the requirement of syntactic monotonicity, the least fixpoint µZ.Φ and the greatest fixpoint νZ.Φ always exist. In order to define the meaning of such formulas we resort to transition systems. Let A = Υ (Π, S) be the transition system for a process Π over a semantic artifact S = (T, A 0 , R). We denote by Σ A the states of A. Let V be a predicate and individual variable valuation on A, i.e., a mapping from the predicate variables Z to subsets of the states Σ A , and from individual variables to constants in C A0 . Then, we assign meaning to µ-calculus formulas by associating to Υ (Π, S) and V an extension function (•) A V , which maps µ-calculus formulas to subsets of Σ A . The extension function (•) A
V is defined inductively as follows:
Here A ⇒ A A holds iff there exists a rule Q → ρ in Π such that there exists a θ ∈ ans C A (Q, T, A) and A = do(ρθ, T, A ). That is, there exist a rule in Π that can fire on A and produce an instantiated action ρθ, which applied on A has A as effect.
Intuitively, the extension function (•) A V assigns to the various µ-calculus constructs the following meanings. The boolean connectives have the expected meaning, while quantification is restricted to constants of C A0 , which are the only constants that the ECQs in the formula can retrieve. We also use the usual FOL abbreviations. The extension of 3Φ consists of the states A such that for some state A with A ⇒ A A , we have that Φ holds in A . While the extension of 2Φ consists of the states A such that for all states A with A ⇒ A A , we have that Φ holds in A . The extension of µZ.Φ is the smallest subset E µ of Σ A such that, assigning to Z the extension E µ , the resulting extension of Φ is contained in E µ . That is, the extension of µX.Φ is the least fixpoint of the operator λE.(Φ) A V[Z/E] (here V[Z/E] denotes the predicate valuation obtained from V by forcing the valuation of Z to be E). Similarly, the extension of νX.Φ is the greatest subset E ν of Σ A such that, assigning to X the extension E ν , the resulting extension of Φ contains E ν . That is, the extension of νX.Φ is the greatest fixpoint of the operator λE.
V does not depend on V, and we denote it by Φ A . The reasoning problem we are interested in is model checking, i.e., verify whether a µL closed formula Φ holds for the process Π over the semantic artifact S. Formally, such a problem is defined as checking whether A 0 ∈ Φ A , that is, whether Φ is true in the root of the initial state A 0 of transition system Υ (Π, S).
Example 3. Continuing on our running example, we consider the following simple safety property: It is always true that gold customers in A0 remain so. This property can be written as:
This formula is true, since no action (among the ones above) removes individuals from being Gold.
Next, we consider a simple liveness property: It is possible to reach a state in which a gold customer is also an in-debt customer.
This formula is true, because the ontology implies that if x participates to owes then x is an instance of InDebt; and we can reach a state in which ∃x.Gold(x) ∧ owes(x, y) holds by firing the action GetLoan(john), which is allowed by the process.
We want to understand when two ABoxes A 1 and A 2 over a common DL-Lite R TBox T provide the same answers to all EQL queries. Given two relational structures I 1 and I 2 over the same set of relations, and a set C of constants, a C-homomorphism h from I 1 to I 2 is a mapping from the domain of I 1 to the domain of I 2 that preserves constants in C and relations, i.e., h(c I1 ) = c I2 for each c ∈ C, and if
, where I A1 is the structure whose domain is C A1 , whose constants are interpreted as themselves, and
for each concept name N , similarly for role names. This property can be checked by resorting to query answering over ontologies. For the ABox A 1 , let Q A1 be the boolean conjunctive query obtained as the conjunction of all facts in A 1 , in which the constants not in C are treated as existentially quantified variables.
Lemma 1. Given a DL-Lite R TBox T , two ABoxes A 1 and A 2 over T , and a set C of constants, we have that
Proof (sketch). We remind that a DL-Lite R ontology (T, A) has a unique (up to renaming of domain elements) canonical-model [5], which is the model that has a C Ahomomorphism to each model of (T, A). By composing homomorphisms, we have that A 1 → C T A 2 iff there is a C-homomorphism from I A1 to the canonical model of (T, A 2 ). The claim then follows by considering that there is a C-homomorphism from I A1 to the canonical model of (T, A 2 ) iff ans C (Q A1 , T, A 2 ) = true [11,5].
Theorem 1. Let C be a set of constants, and A 1 , A 2 two ABoxes that are Chomomorphically equivalent wrt a TBox T . Then, for every ECQ Q over T using only constants in C, we have that ans
Next we want to capture when two states of a single transition system or more generally of two transition systems, possibly obtained by applying different processes to different semantic artifacts sharing the same TBox and constants in the initial state, can be considered behaviourally equivalent, in the sense that they satisfy exactly the same µL formulas. To formally capture such an equivalence, we make use of the notion of bisimulation [12], suitably extended to deal with query answering over ontologies.
Given two artifact transition systems
We say that two states A 1 and A 2 are bisimilar, if there exists a bisimulation B such that (A 1 , A 2 ) ∈ B. Two transition systems A 1 with initial state A 10 and A 2 with initial state A 20 are bisimilar if (A 10 , A 20 ) ∈ B.
The following theorem states that the formula evaluation in µL is indeed invariant wrt bisimulation, so we can equivalently check any bisimilar transition systems. Theorem 2. Let A 1 and A 2 be two transition systems obtained from two semantic artifacts sharing the same TBox and constants. Then, for two states A 1 of A 1 and A 2 of A 2 (including the initial ones) are bisimilar iff for all µL closed formulas Φ over the two semantic artifacts, we have that
Proof. The proof is analogous to the standard proof of bisimulation invariance of µcalculus [7], though taking into account our specific definition of bisimulation, using Theorem 1 to guarantee that ECQs are evaluated identically over bisimilar states.
We now show that, not surprisingly, verification in the infinite state setting we considered is undecidable, but that it becomes decidable under some interesting conditions inspired by the recent literature on data exchange [8]. Our results rely on the possibility of building special semantic artifacts that we call "inflationary approximates". For such special artifacts there exists a tight correspondence between the application of an action and a step in the chase of a set of tuple-generating dependencies (TGDs) [13,8] Given a semantic artifact S = (T, A 0 , R), its inflationary approximate is the semantic artifact S + = (T + , A 0 , R + ) defined as follows. T + is obtained from T by dropping all assertions involving negation on the right-hand side, thus obtaining a TBox formed by positive inclusions only. R + is formed by one action specification ρ + for each action specification ρ ∈ R, where ρ + is obtained from ρ by:
removing all input parameters from the signature -note that the variables in q + i that used to be parameters in ρ, become free variables in ρ + ; substituting each effect e i : q + i ∧ Q − i A i with e i : q + i A i -note that we need to preserve the Skolem functions name in the transformation; adding effects to copy all concept and role names, namely adding an effect N (x) N (x) for each concept name N of T , and an effect P (x, y) P (x, y) for each role name P of T . Observe that executing actions in S + can never give rise to an inconsistency, since T + does not contain any negative information [5].
We also consider the generic process Π , in which all condition/action rules have the trivially true condition. Hence, Π allows for executing every action at every step. With these notions in place, it is easy to prove that verification in this setting is undecidable.
Theorem 3. µL model checking of processes over semantic artifacts is undecidable.
Proof (sketch). We show that it is already undecidable to check, given a semantic artifact S + ∅ = (∅, A 0 , R), of the form of an inflationary approximate of an artifact with an empty TBox, and the transition system A = Υ (Π , S + ∅ ), whether A 0 ∈ µZ(q ∨ 3Z) A , where q is a boolean UCQ. We observe that the set of all actions in S + can be seen as a set of TGDs, indeed it suffices to consider one TGD for each disjunct in the UCQ on the left-hand side of an effect specification. So, we can reduce to the above model checking problem the problem of answering boolean UCQs in a relational database under a set of TGDs, which is undecidable [14] Next, we observe a notable property of the transition system Υ (Π , S + ) generated by the generic process Π over the inflationary approximate S + of a semantic artifact S. Namely, each do(ρ + , T, •) is a monotonic operator. This implies that by repeatedly applying such operators starting from the ABox A 0 in S + , we get at the limit (possibly transfinite) a single ABox A max , which is the least fixpoint of such operators taken collectively [15,16]. Such an ABox contains, every fact generated by repeatedly executing actions from the inflationary approximate S + , that is every state A + of Υ (Π , S + ) is such that A + is contained in A max . More interestingly, we show next that A max contains also every A generated by repeatedly executing actions from the original S. Lemma 2. Let S = (T, A 0 , R) be a semantic artifact and Π a process over S. Then every state A of the transition system Υ (Π, S) is a subset of A max defined as above.
Proof (sketch). We can show by induction that, for every sequence of actions ρ 1 θ 1 , ρ 2 θ 2 , . . . , ρ n θ n generated by the process Π starting from A 0 , the resulting state do(ρ n θ n , T, do(
In other words, A max generated by the generic process Π running over the inflationary approximate S + of a semantic artifact S, bounds all states A that any process Π can generate by running on S. Hence if for any reason A max is finite, then the transition system Υ (Π, S) is finite. Hence, being model checking of finite transition system decidable (in fact polynomial in the size of the transition system), we get that also model checking of Υ (Π, S) is decidable.
To get finiteness guarantees on A max , we take advantage of the correspondence between action execution and TGDs chase steps, as in the proof of Theorem 3. We build on this correspondence by further considering that in DL-Lite R , every UCQ q over a TBox can be rewritten as a new UCQ rew (q) over the same alphabet, to be evaluated over the ABox considered as a relational database [5] (that is dropping the TBox).
In the literature for data exchange, several conditions that guarantee the finiteness of the chase of TGDs have been considered [17,18]. Here we focus on the original notion of weakly-acyclic TGDs [17]. Weak-acyclicity is a syntactic notion that involves the so-called dependency graph of the set of TGDs. Informally, a set D of TGDs is weakly-acyclic if there are no cycles in the dependency graph of D involving "existential" relation positions. The key property of weakly-acyclic TGDs is that chasing a relational database with them (i.e., applying them in all possible ways) generates a set of facts (a database) that is finite. See [17] for details.
Given a semantic artifact S = (T, A 0 , R) and its inflationary approximate S + = (T + , A 0 , R + ), we define the set E + ∅ of effect specifications that includes an effect rew (q + i ) A i for each effect q + i A i of an action ρ + ∈ R + . Notice that the set E + ∅ can be seen as a set of TGDs. We say that a semantic artifact S is weakly-acyclic if the set E + ∅ seen as a set of TGDs is weakly-acyclic. (Note that the semantic artifact in our example is trivially weakly-acyclic.) Lemma 3. Let S = (T, A 0 , R) be a weakly-acyclic semantic artifact and S + its inflationary approximate. Then A max computed as above for S + is finite. Proof (sketch). We have to show that starting from A 0 we get to the least fixpoint A max of the do(ρ + , T, •) operator in a finite number of steps. To do so, we follow the line of the proof of finiteness of chase of weakly-acyclic TGDs in [17], and show that the number of Skolem terms generated by the effects of actions is bounded by a polynomial in the size of A 0 . Differently from [17], we cannot rely on the notion of homomorphism to stop firing actions, but have to use membership of the new set of facts in the previous ones.
As a direct consequence of Lemma 2 and Lemma 3, for weakly-acyclic semantic artifacts verification is decidable.
Theorem 4. µL model checking of processes over weakly-acyclic semantic artifacts is decidable.
Proof (sketch). The result follows by observing that every state generated by the execution of any process Π over a weakly-acyclic semantic artifact S is a subset of A max , which by Lemma 3 is finite. Hence, we can apply a model checking procedure for µ-calculus on finite-state systems [7].
Note that the proof of Theorem 4 is giving us a single exponential upper bound (in the size of A 0 ) for µL model checking involving weakly-acyclic semantic artifacts.
This work has been supported by the EU FP7-ICT Project ACSI (257593).
In this paper we have studied verification of processes over semantic artifacts. We obtain an interesting decidability result by relying on the notion of inflationary approximate, which allows for a connection with the theory of chase of TGDs in relational databases. We close by observing that while we fully used the ontology for querying the artifact state, we use it in a limited way when updating the state, namely only to guarantee consistency. Ontology update has its own semantic and computational difficulties, see e.g., [19], which our approach sidesteps. However, if one could introduce a suitable notion of inflationary approximate in that case, the approach presented here could be used to devise decidable cases.