In the setting of graph-structured data, description logics are well suited to impose constraints that capture the semantics of the domain of interest. When the data evolves as a result of operations carried out by users or applications, it is important to ensure that the satisfaction of the constraints is preserved, analogously to the consistency requirement for transactions in relational databases. In this paper we introduce a simple action language in which actions are nite sequences of insertions and deletions performed on concept/roles, and we study static veri cation in this setting. Speci cally, we address the problem of verifying whether the constraints are still satis ed in the state resulting from the execution of a given action, for every possible initial state satisfying them. We are able to provide a tight coNExpTime bound for a very expressive DL, and show that the complexity drops to coNP-complete for the case of DL-Lite.
Graph databases are gaining increasing importance due to the adoption of data
formats like RDF, and are fundamental for storing, for example, web data in the
form of RDF triplestores, and other forms of semi-structured data. Given the
very large amounts of data currently available in these stores, the development of
automated management tools for them is becoming a pressing problem. Indeed,
many of the crucial aspects of managing classical relational databases are also
relevant for graph databases. For instance, as in traditional databases, integrity
constraints on graph databases are important to capture the semantics of the
domain of interest. Databases may evolve as a result of operations carried out
by users or applications, and it is important to ensure that this does not result
in the constraints being violated. This is essentially the consistency property
of database transactions. A transaction encapsulates a sequence of modi
cations to the data, which are executed and committed as a unit. A transaction
is consistent if its execution over a legal database state never leads to an
illegal one. Verifying the consistency of transactions is a crucial problem that
has been studied extensively, for di erent kinds of transactions and constraints,
over traditional relational databases [
In contrast, the setting we consider here is that of graph databases where
integrity constraints are expressed in Description Logics (DLs) [
We now de ne the description logic that we use as a constraint language for graph databases. We call it ALCHOIQbr, which is the standard ALCHOIQ extended with Boolean combinations of axioms and a constructor for a singleton role. We assume countably in nite sets NR of role names, NC of concept names, NI of individual names, and NV of variables.
Roles are de ned inductively: (i) if r 2 NR, then r and r (the inverse of r) are roles; (ii) if ft; t0g NI [ NV, then f(t1; t2)g is also a role; (iii) if r1; r2 are roles, then r1 [ r2, and r1 n r2 are also roles.
Concepts are de ned inductively as well: (i) if A 2 NC, then A is a concept; (ii) if t 2 NI [ NV, then ftg is a concept (called nominal ); (iii) if C1, C2 are concepts, then C1 u C2, C1 t C2, and :C1 are also concepts; (iv) if r is a role, C is a concept, and n is a non-negative integer, then 9r:C, 8r:C, 6n r:C, and >n r:C are also concepts.
A concept (resp., role) inclusion is an expression of the form 1 v 2, where 1; 2 are concepts (resp., roles). Expressions of the form t : C and (t; t0) : r, where ft; t0g NI [ NV, C is a concept, and r is a role, are called concept assertions and role assertions, respectively. Concepts, roles, inclusions and assertions that have no variables are called ordinary. The role of variables will become apparent in Section 3. We de ne (ALCHOIQbr-)formulae inductively: (i) every inclusion and assertion is a formula; (ii) if K1; K2 are formulas, then so are K1 ^K2, K1 _K2 and :_K1. If a formula K has no variables, it is called a knowledge base (KB).
An interpretation is a pair I = h I ; I i where I 6= ; is the domain, AI
I for each A 2 NC, rI I I for each r 2 NR, and oI 2 I for each o 2 NI.
For the ordinary roles of the form f(o1; o2)g, we let f(o1; o2)gI = f(o1I ; o2I )g. The
function I is extended to the remaining ordinary concepts and roles in the
usual way. Assume an interpretation I. For an ordinary inclusion 1 v 2, I
satis es 1 v 2 (in symbols, I j= 1 v 2) if 1I 2I . For an ordinary assertion
= o : C (resp., = (o1; o2) : r), I satis es (in symbols, I j= ) if oI 2 CI
(resp., (o1I ; oI ) 2 rI ). The notion of satisfaction is extended to knowledge bases
2
as follows: (i) I j= K1 ^ K2 if I j= K1 and I j= K2; (ii) I j= K1 _ K2 if I j= K1
or I j= K2; (iii) I j= :_K if I 6j= K. If I j= K, then I is a model of K. The nite
satis ability (resp., unsatis ability ) problem is to decide given a KB K if there
exists (resp., doesn't exist) a model I of K with I nite. The nite satis ability
problem for ALCHOIQbr KBs has the same computational complexity as for
the standard ALCHOIQ:
Theorem 1. Finite satis ability of ALCHOIQbr KBs is NExpTime-complete.
Proof (sketch). The lower bound comes from [
We now de ne an action language that allows us to express nite sequences of operations on interpretations (i.e., graph databases).
De nition 1 (Action language). A basic action grammar: is given by the following ! (A
C) j (A
C) j (r p) j (r p); where A is a concept name, r is a role name, C is an arbitrary concept, and p is an arbitrary role. Then, (complex) actions are given by the following grammar: ! j K ? : j ; where is a basic action and K is an arbitrary ALCHOIQbr{formula. The special symbol denotes the empty action.
An action is ground if it has no variables. An action 0 is called a ground instance of an action if 0 is ground and it can be obtained from by replacing each variable by an individual name from NI. For an action , we will sometimes write (x), where x is a tuple containing exactly the variables of .
Intuitively, an application of an action (A C) on an interpretation I stands for the addition of the content of CI to AI . In turn, removing CI from AI can be done by applying (A C) on I. The two operations can also be performed on extensions of roles. In addition, complex actions allow for composing basic actions and for conditional action execution. In order to formally de ne the semantics of actions, we rst introduce the notion of interpretation updates. De nition 2 (Interpretation updates). Assume an interpretation I and let be a concept or role name. If is a concept, let W I be a unary relation, otherwise, if is a role, let W I I be a binary relation. Then we let I W (resp., I W ) denote the interpretation I0 such that
I0 = 1I0 = I0 =
I , 1I for all symbols 1 6= , and
I [ W (resp., I0 = I n W ).
Now we can de ne the semantics of ground actions inductively as follows. De nition 3. Given a ground action , we de ne a mapping S from interpretations to interpretations as follows:
S(A C) (I) = S (I S(A C) (I) = S (I
A CI )
A CI ) S (I) = I
SK? 1: 2 (I) = S(r p) (I) = S (I r pI ) S(r p) (I) = S (I r pI ) (S 1 (I); if I j= K;
S 2 (I); if I 6j= K: Example 1. The following interpretation I1 represents (part of) the project database of some research institute. There are two active projects, and there are four employees of which three work in the active projects.
ActiveProjectI1 = fP20840 ; P24090 g;
ProjectI1 = fP20840 ; P24090 g; ConcludedProjectI1 = fg;
EmployeeI1 = fE01 ; E03 ; E04 ; E07 g;
ProjectEmployeeI1 = fE01 ; E03 ; E07 g; PermanentEmployeeI1 = fE04 g; worksForI1 = f(E01 ; P20840 ); (E03 ; P20840 ); (E07 ; P24090 )g; The following action captures the termination of project P20840, which is removed from the active projects and added to the concluded ones. The employees working for this project are removed from the project employees.
1 = ActiveProject fP20840g
ConcludedProject fP20840g
ProjectEmployee 9worksFor:fP20840g The interpretation S 1 (I1) that re ects the status of the database after action 1 looks as follows:
ActiveProjectS 1 (I1) = fP24090 g;
ProjectS 1 (I1) = fP20840 ; P24090 g; ConcludedProjectS 1 (I1) = fP20840 g;
EmployeeS 1 (I1) = fE01 ; E03 ; E04 ; E07 g; ProjectEmployeeS 1 (I1) = fE07 g; PermanentEmployeeI1 = fE04 g;
worksForI1 = f(E01 ; P20840 ); (E03 ; P20840 ); (E07 ; P24090 )g; P20840S 1 (I1) = P20840 ;
P24090S 1 (I1) = P24090 :
In our approach, all the individual variables of an action are seen as parameters, whose values are given before executing an action.
Example 2. The following action 2 with variables x; y; z transfers the employee x from project y to project z: 2 = (x : Employee ^ y : Project ^ z : Project ^ (x; y) : worksFor) ?
worksFor f(x; y)g worksFor f(x; z)g : The action 2 rst checks whether x is an employee, y and z are projects, and x works for y. If yes, it removes the worksFor link between x and y and creates a worksFor link between x and z. If any of the checks fails, it does nothing.
In this paper we focus on static veri cation: we want to know whether, given an action and a collection of constraints expressed as a KB, the execution of on I preserves the satisfaction of the constraints, for any possible nite interpretation I.
De nition 4 (The static veri cation problem). Let K be a knowledge base. We say that an action is K-preserving if for every ground instance 0 of and every nite interpretation I, we have that I j= K implies S 0 (I) j= K. The static veri cation problem is to decide, given as input an action and a KB K, whether is K-preserving. Example 3. The following KB K1 expresses constraints on the project database of our running example:
(Project v ActiveProject t ConcludedProject) ^ (Employee v ProjectEmployee t PermanentEmployee) ^ (9worksFor:Project v ProjectEmployee) The action 1 from Example 1 is not K1-preserving: I1 j= K1, but S 1 (I1) 6j= K1 since the concept inclusion 9worksFor:Project v ProjectEmployee is violated. 4
To obtain an algorithm for the static veri cation problem we employ a reduction to nite (un)satis ability of ALCHOIQbr KBs. In particular, given a knowledge base K and an action , we build a KB K0 such that K0 is nitely satis able i is not K-preserving. We start by de ning a transformation TR (K) that incorporates an action into a KB K: De nition 5. Given a KB K, we use KL L0 to denote the KB that is obtained from K by replacing every name L by a possibly more complex expression L0. Given a KB K and an action , we de ne TR (K) as follows: (a) TR (K) = K, (b) TR(A C) (K) = (TR (K))A AtC , (c) TR(A C) (K) = (TR (K))A Au:C , (d) TR(r p) (K) = (TR (K))r r[p, (e) TR(r p) (K) = (TR (K))r rnp, (f ) TR(K1? 1: 2)(K) = (:K1 _ TR 1 (K)) ^ (K1 _ TR 2 (K)) Example 4. By applying the transformation above to K1 and following KB TR 1 (K1): 1, we obtain the (Project v (ActiveProject u :fP20840g) t (ConcludedProject t fP20840g)) ^ (Employee v (ProjectEmployee u :9worksFor:fP20840g) t PermanentEmployee) ^ (9worksFor:Project v (ProjectEmployee u :9worksFor:fP20840g)) Note that I1 6j= TR 1 (K1), since (9worksFor:Project)I1 = fE01 ; E03 ; E07 g and (ProjectEmployee u :9worksFor:fP20840g)I1 = fE07 g, hence the inclusion 9worksFor:Project v (ProjectEmployee u :9worksFor:fP20840g is violated.
We now show that this transformation correctly captures the meaning of ground actions.
Lemma 1. Assume a ground action we have S (I) j= K i I j= TR (K).
and a KB K. For any interpretation I, Proof. We prove the claim by induction on the structure of . In the base case where = , we have S (I) = I and TR (K) = K by de nition, and thus the claim holds.
Assume
= (A C) 0. Let I0 = S(A C)(I), i.e., I0 coincides with I except that AI0 = AI [ CI . We know that for any KB K0, I0 j= K0 i I j= KA AtC . In 0 particular, I0 j= TR 0 (K) i I j= (TR 0 (K))A AtC . Since, (TR 0 (K))A AtC = TR (K), we get I0 j= TR 0 (K) i I j= TR (K). By the induction hypothesis, I0 j= TR 0 (K) i S 0 (I0) j= K. Thus, I j= TR (K) i S 0 (I0) j= K. Since S 0 (I0) = S 0 (S(A C)(I)) = S (I), we have I j= TR (K) i S (I) j= K.
For the cases = (A C) 0, = (r p) 0, and = (r p) 0, the argument is analogous.
Finally, we consider = (K1? 1: 2), and assume an arbitrary I. We distinguish two cases: (i) I j= K1. Then S (I) = S 1 (I) by de nition. By the induction hypothesis, S 1 (I) j= K i I j= TR 1 (K), hence we have S (I) j= K i I j= TR 1 (K). Since TR (K) = (:K1 _ TR 1 (K)) ^ (K1 _ TR 2 (K)), it trivially follows that S (I) j= K i I j= TR (K). (ii) I 6j= K1, that is, I j= :K1. The proof is analogous. We have S (I) = S 2 (I) by de nition. By the induction hypothesis, S 2 (I) j= K i I j= TR 2 (K), hence we have S (I) j= K i I j= TR 2 (K). Since TR (K) = (:K1 _ TR 1 (K)) ^ (K1 _ TR 2 (K)), it trivially follows that S (I) j= K i I j= TR (K). tu This lemma is the key to our reduction. An action is not K-preserving i some model of K does not model TR (K), where is a `canonical' grounding of obtained by replacing each variable with a fresh individual. This allows us to decide the static veri cation problem by deciding the satis ability of K ^ :TR (K). Formally, we have: Theorem 2. Assume a (complex) action are equivalent: and a KB K. Then the following (i) The action is not K-preserving. (ii) K ^ :TR (K) is nitely satis able, where is obtained from ing each variable with a fresh individual name not occurring in by replacand K.
Proof. (i) to (ii). Assume there exist a ground instance 0 of and a nite interpretation I such that I j= K and S 0 (I) 6j= K. Then by Lemma 1, I 6j= TR 0 (K). Thus I j= :TR 0 (K). Suppose o1 ! x1; : : : ; on ! xn is the substitution that transforms into 0. Suppose also o01 ! x1; : : : ; o0n ! xn is the substitution that transforms into . Take the interpretation I that coincides with I except for (o0i)I = (oi)I . Then I j= K ^ :TR (K).
(ii) to (i). Assume K ^ :TR (K) is nitely satis able, i.e., there is an interpretation I such that I j= K and I 6j= TR (K). Then by Lemma 1, S (I) 6j= K. tu
The above reduction leads to the main complexity result of this paper. Theorem 3. The static veri cation problem is coNExpTime-complete in the presence of ALCHOIQbr KBs.
Proof. The coNExpTime upper bound follows from Theorem 2 and the fact that nite satis ability of ALCHOIQbr KBs is NExpTime-complete (c.f. Theorem 1).
For hardness, we note that nite unsatis ability of ALCHOIQbr KBs can be reduced in polynomial time to static veri cation in the presence of ALCHOIQbr KBs. Indeed, a KB K is nitely satis able i (A0 fog) is not (K^(Av:A0)^(o : A))-preserving, where A, A0 are fresh concept names and o is a fresh individual. tu 5
In this section we consider a restricted setting for which the computational
complexity of the static veri cation problem is lower. We use a variant of
DLLiteR [
De nition 6. A DL-Lite+R KB K is a KB satisfying the following conditions: - The operator :_ may occur only in front of assertions. - All concept inclusions have the form C1 v C2 or C1 v :C2 of K, with C1; C2 2
NC [ f9r:> j r 2 NRg [ f9r :> j r 2 NRg. - All role inclusions have the form r1 v r2 or r1 v :r2, with r1; r2 2 NR [ fr j r 2 NRg. - For all concept assertions3 o : C of K, C 2 B+, where B+ is the smallest set of concepts such that: (a) NC B+, (b) fo0g 2 B+ for all o0 2 NI, (c) 9r:> 2 B+ for all roles r, (d) fB1 u B2; B1 t B2; :B1g B+ for all B1; B2 2 B+.
A DL-LiteR KB K is a DL-Lite+ KB that satis es the following restrictions:
R - K is a conjunction of inclusions and assertions, - all assertions in K are basic assertions of the forms o : C with C 2 NC, and (o; o0) : r with r 2 NR.
We also restrict slightly the action language, by allowing only Boolean combinations of (possibly negated) assertions to be used to express the condition K in actions of the form K ? 1: 2. This is captured by the notion of localized actions. 3 Note that there is no restriction on role assertion (o; o0) : r of K. De nition 7. If no inclusions occur in an action , then is called localized.
DL-Lite+R is expressive enough to allow us to reduce the static veri cation problem for localized actions to nite unsatis ability testing.
Theorem 4. The static veri cation problem for DL-Lite+ KBs and localized R actions can be reduced in linear time to nite unsatis ability testing for DLLite+ KBs.
R Proof. Assume a DL-Lite+R KB K and a localized action . Let be the action obtained from by replacing each variable with a fresh individual name not occurring in and K. Construct K0 = K ^ :_TR (K). From Theorem 2 we know that K0 is not nitely satis able i is K-preserving. The KB K0 is not a DLLite+R KB, but it can be transformed into an equisatis able DL-Lite+R KB in linear time. To this end, turn K0 into negation normal form, i.e., push :_ inside so that :_ occurs in front of inclusions and assertions only. Then replace every occurrence of :_(B1 v B2) and :_(r1 v r2) in the resulting K0 by o : B1 u :B2 and (o; o0) : r1 n r2, respectively, where o; o0 are fresh individuals. Clearly, the above transformations preserve satis ability. Moreover, since in K the operator :_ may occur only in front of assertions, and is localized, every inclusion in the resulting K0 already appears in K. This implies that K0 is a DL-Lite+R KB as desired. tu
We next characterize the complexity of nite satis ability in DL-Lite+R. Theorem 5. Finite satis ability of DL-Lite+ KBs is NP-complete. R Proof. NP-hardness is immediate (e.g., by a reduction from propositional satisability). For membership in NP, we de ne a non-deterministic rewriting procedure that transforms in polynomial time a DL-Lite+R KB into a DL-LiteR KB. In particular, we ensure that a DL-Lite+R KB K is nitely satis able i there exists a rewriting of K into a nitely satis able DL-LiteR KB. Since satis ability testing in DL-LiteR is feasible in polynomial time, this yields an NP upper bound for DL-Lite+R.
Assume a DL-Lite+ KB K. The rewriting of K has two steps: rst, we get
R rid of the possible occurrences of _, and then of the complex concepts and roles in assertions.
For the rst step, let P be the set of inclusions and assertions appearing in K. Non-deterministically pick a set M P such that M is a model of K, when K is seen as a propositional formula over P . Let KM = V 2M ^V 062M :_ 0. Clearly, K is nitely satis able i we can choose an M with KM nitely satis able.
In the next step, we show how to obtain from KM a DL-LiteR KB. Let T be the set of inclusions that occur in KM and let A be the set of assertions and their negations occurring in KM . Recall that the inclusions of T are inclusions of the standard DL-LiteR, but the assertions in A may contain complex concepts. We non-deterministically complete A with further assertions to explicate complex concepts and roles. A completion of A is a -minimal set A+ of assertions such that: - A A+; - for every assertion , 62 A+ or :_ 62 A+; - if o is an individual from KM and C1 v C2 2 T , then :_(o : C1) 2 A+ or o : C2 2 A+; - if (o; o0) are individuals from KM and r1 v r2 2 T , then :_((o; o0) : r1) 2 A+ or (o; o0) : r2 2 A+; - if o : C1 u C2 2 A+, then o : C1 2 A+ and o : C2 2 A+; - if o : C1 t C2 2 A+, then o : C1 2 A+ or o : C2 2 A+; - if o : 9r:> 2 A+, then (o; o0) : r 2 A+ for some fresh o0; - if o : :C 2 A+, then :_(o : C) 2 A+; - if :_(o : C) 2 A+, then o : :C 2 A+; - if o : ::C 2 A+, then o : C 2 A+; - if o : :(C1 u C2) 2 A+, then :_(o : C1) 2 A+ or :_(o : C2) 2 A+; - if o : :(C1 t C2) 2 A+, then :_(o : C1) 2 A+ and :_(o : C2) 2 A+; - if o : :(9r:>) 2 A+, then :_((o; o0) : r 2 A+) for all individuals o0 of A+; - if (o; o0) : r 2 A+, then (o0; o) : r 2 A+; - if (o; o0) : r1 [ r2 2 A+, then (o; o0) : r1 2 A+ or (o; o0) : r2 2 A+; - if (o; o0) : r1 n r2 2 A+, then (o; o0) : r1 2 A+ and :_((o; o0) : r2) 2 A+; - if :_((o; o0) : r1 [ r2) 2 A+, then :_((o; o0) : r1) 2 A+ and :_((o; o0) : r2) 2 A+; - if :_((o; o0) : r1 n r2) 2 A+, then :_((o; o0) : r1) 2 A+ or (o; o0) : r2 2 A+; - if o : fo0g 2 A+, then o = o0; - if (o1; o2) : f(o01; o02)g 2 A+, then o1 = o01 and o2 = o02; Let Ab+ be the restriction of A+ to basic assertions. Clearly, V T ^ V Ab+ is a DL-LiteR KB. It is not di cult to see that KM is nitely satis able i there exists a completion A+ such that V T ^ V Ab+ is nitely satis able. tu
Now we can give a tight bound on the complexity of static veri cation. Theorem 6. The static veri cation problem for DL-Lite+ KBs and localized R actions is coNP-complete.
Proof. The upper bound follows directly from Theorems 4 and 5. The lower bound can be obtained by a reduction from nite unsatis ability in DL-Lite+R. To this end, we can employ exactly the same reduction in the proof of Theorem 3. tu
It is important to note that coNP-hardness is not only due to the fact that we are using an intractable extension of DL-LiteR to specify the constraints. Indeed, the given coNP bound is tight even if the constraints are in a very restricted fragment of the core DL-Lite: they are a conjunction of disjointness assertions between concept names. The actions needed to show coNP-hardness are also quite restricted: plain sequences of basic concept actions. Theorem 7. The static veri cation problem is coNP-hard already for KBs of the form (A0 v :A00) ^ : : : (An v :A0n), where each Ai; A0i is a concept name, and actions are localized, ground sequences of basic actions of the forms (A C) and (A C). Proof. We employ the 3-Coloring problem for graphs. Assume a graph G = (V; E) with V = f1; : : : ; ng. We construct in polynomial time a KB K and an action such that G is 3-colorable i is not K- preserving. For every v 2 V , we use 3 concept names A0v; A1v; A2v for the 3 possible colors of the vertex v. In addition, we employ a concept name D. Let K be the following KB: K = (D v :D) ^
^ fAogi0))((BBi1
Assume I is a model of K such that S (I) 6j= K. We argue that then G is 3-colorable. Indeed, since does not modify the extensions of concepts Acv, S (I) 6j= K may only hold if fogI is in the extension of D after applying on I. Due to 3, fogI is not in the extensions of B1; : : : ; Bn after applying 1 21 2n on I. Due to 1 and 2n, for any i 2 f1; : : : ; ng, it must be the case that fogI is in the extension of some Ai0; Ai1 or Ai2 in I. For every v 2 V , let col(v) 2 f0; 1; 2g by any value such that fogI is in the extension of Aicol(v) in I. Since I satis es the disjointness axioms in K, the function col is a proper 3-coloring of G.
Suppose G is 3-colorable and a proper coloring of G is given by a function col : V ! f0; 1; 2g. Take any interpretation I with I = feg and such that (i) fogI = e, (ii) DI = ;, (iii) e 2 (Acv)I i col(v) = c. Since col is a proper coloring of G, I is a model of K. As easily seen, S (I) 6j= K. tu 6
In this paper we have studied the static veri cation problem for evolving graph
databases, when the integrity constraints are expressed in DLs and the updates
in a simple action language. We have shows that the problem can be reduced
to a better known reasoning task: nite satis ability of knowledge bases. We
obtained a tight coNExpTime bound for the problem when the constraints are
expressed in a very expressive DL, and a coNP bound if a dialect of DL-Lite
is considered. This paper is intended to be only a starting point in the study of
evolving graph databases under DL constraints, and many challenges remain for
future work. For example, the action language we have considered here is rather
weak, and a more expressive action language seems desirable. However, many
natural extensions, such as `while' loops in actions, would easily yield an
undecidable formalism. Given that the static veri cation problem is intractable even
for weak fragments of the core DL-Lite and very restricted forms of actions, it
remains to explore how feasible static veri cation is in practice, and whether there
are meaningful restrictions that make the problem tractable. Also other data
management reasoning services remain to be considered, including planning, for
which we may draw from existing work on DL-based action languages [