Graph databases are directed graphs in which the edges are labeled with symbols from a finite alphabet. In this paper we introduce a logic for such graphs in which the domain is the set of edges. We compare its expressiveness with the standard logic in which the domain the set of vertices. Furthermore, we introduce a robust model of computation for such logic, the so called graph pebble automata.
The study of graph structured data has received much attention lately, due to numerous
applications in areas such as biological networks [
For querying graph structured data, one normally wishes to specify certain types of
paths between nodes. Most common examples of these queries are conjunctive
regular path queries [
Our intention is to study formalisms for such graph databases which is capable of expressing these integrity constraints, while at the same time still feature manageable model checking properties. Obviously such formalisms depend on how the underlying directed graph of the databases are represented in the first place.
The standard representation of directed graphs is simply a set of nodes, together with a binary relation on these nodes to represent the edge among them. The labeling of the edges is represented as a function from the edges to the finite alphabet of symbols. We call such representation the vertex representation.
Another less common way to represent directed graphs is to take the edges as the domain, together with some well defined binary relations on these edges to indicate how two edges intersect. The labeling of the edges is represented as a set of unary predicates on the domain. We call such representation the edge representation.
In the first part of our paper we propose a vocabulary for the edge representation, which we call E-vocabulary. We call V-vocabulary the vocabulary for the vertex representation. We study the expressive power of E and compare it to V-vocabulary. In this respect our contributions are the following.
– The logic that we propose for edge representation is robust, in the sense that for each graph database in the vertex representation, there exists a unique (up to isomorphism) graph database in the edge representation that have the same underlying directed graph. Vice versa, for each graph database in the edge representation, there exists a unique (up to isomorphism) graph database in the vertex representation that have the same underlying directed graph. – Next, we turn our attention to expressivity of E-vocabulary. For first-order logic (FO) we show that it is equivalent to V-vocabulary. On the other hand, for the existential monadic second-order logic (9MSO), as well as monadic second-order logic (MSO), the E-vocabulary is more expressive than the V-vocabulary. That is, there are 9MSO and MSO sentences in E-vocabulary that cannot be expressed in sentences in V-vocabulary in 9MSO and MSO logics, respectively.
In the second part of our paper we introduce a notion of automata for graph databases.
We follows the direction in [
Pebble automata was initially introduced for words over finite alphabet in [
Later in [
In this paper we extend this connection to the case of graph databases, i.e., directed
graphs in which edges are labeled with symbols from a finite alphabet . Some of the
results in this paper are the following.
1. We define the notion of k pebble graph automata, or in short k-PA, for graph
databases.
2. Every first-order sentences of quantifier rank k over graph databases can be
simulated by k-PA.
3. We demonstrate the robustness of pebble automata by showing the equivalence
between two-way alternating k-PA and one-way deterministic k-PA. This result
settles a question raised in [
This robustness immediately implies that the class of families of directed graphs captured by k-PA is closed under boolean operations.
We also note that almost all results in [
Related work. Closely related to our work is Courcelles work [
Later on in the paper [
Another work related to ours is the work in [
These models, the V - and E-automata, are incomparable to our graph pebble automata. On one side, E-automata are capable of simulating -calculus on directed graphs, but they are not closed under negation. On the other side, our graph pebble automata are capable of simulating the whole first-order logic on directed graphs, closed under all boolean operations.
Organization. This paper is organized as follows. In Section 2 we define the vocabularies V and E. Then in Section 3 we define the notion of structural equivalent, the notion to compare two structures from V and E logics. In Section 4 we compare the expressive power between V and E logics. We introduce graph pebble automata in Section 5. We then extend all previous definitions to the labeled edges graphs in Section 6. Finally we conclude with a future direction for our work in Section 7. 2
Graph databases are usually defined as finite edge-labeled directed graphs [
In what follows, we state two representations for graph databases. The first is the standard one, where a directed graph is just a set of vertices equipped with a binary relation on the vertices. We will denote its vocabulary by V.
The second one is our proposed representation for directed graphs where the edges are the domain. We will denote its vocabulary by E.
The vocabulary V. The vocabulary V simply consists of one binary predicate E. We denote by STRUCT[V] the set of structures of V, which are simply directed graphs. A V-structure is a structure in STRUCT[V].
We will usually write G = (V (G); E(G)) for structures in STRUCT[V], where V (G) = Dom(G) is the domain and E(G) is the binary relation on the elements in V (G).
The atomic formula in the logic V is either x = y or E(x; y). The meaning of
atomic formulas under the Boolean connectives and first-order quantification over V . The logic MSO[V], which stands for monadic second-order, is obtained by adding quantification over unary predicates on the domain. If the unary predicates quantifications are all existential, then we denote it by 9MSO[V]. A V-sentence is a sentence using the vocabulary V. A sentence ' defines a set of directed graphs via G(') := fG j G j= 'g.
there is no isolated vertices and there is no self loop.
The vocabulary E. Intuitively, rather than viewing a directed graph G = (V; E) as a set V of vertices and E a binary relation on V , we take E as the domain and define some relations among the elements in E.
Let u and v be two vertices and e be an edge from u to v. What we mean by the head of e is the vertex v, while the tail of e is the vertex u. Now the vocabulary E consists of the binary relations HeadHead, HeadTail and TailTail on the directed edges, where the intentions of each predicate are as follows.
– TailTail(e1; e2) means that the tails of e1 and e2 are the same. – HeadHead(e1; e2) means that the heads of e1 and e2 are the same. – HeadTail(e1; e2) means that the head of e1 is the tail of e2.
As above, STRUCT[E] denotes the set of all structures of E and an E-structure is a structure in STRUCT[E]. We assume that the structures in STRUCT[E] satisfy the following axioms.
E1: Both HeadHead and TailTail are equivalence relations.
E2: If HeadHead(e1; e2) and HeadTail(e1; e3), then HeadTail(e2; e3). E3: If TailTail(e1; e2) and HeadTail(e3; e1), then HeadTail(e3; e2).
E4: If HeadTail(e1; e3) and HeadTail(e2; e3), then HeadHead(e1; e2). E5: If HeadTail(e3; e1) and HeadTail(e3; e2), then TailTail(e1; e2).
E6: If HeadHead(e1; e2) and TailTail(e1; e2), then e1 = e2.
The purpose of axioms E1–E5 are for consistency, that is, the structures in STRUCT[E] are really graphs in the ordinary sense of graphs as structures in STRUCT[V]. (See Proposition 2 below.) Axiom E6 does not allow multiple edges, whereas Axiom E7 does not allow self-loop. Axioms E6 and E7 are not essential, but they will be useful for our convenience in the presentation.
second-order and existential monadic second-order sentences in the logic E. An Esentence is a sentence using the vocabulary E.
G(') := fE j E j= 'g: 3
In this section we will show that both the edge and the vertex representations essentially denote the same class of objects.
Definition 1. Let G 2 STRUCT[V] and G 2 STRUCT[E]. We say that G and E are structurally equivalent if there exists a 1-1 mapping : E(G) ! Dom(E ) such that for all (v1; v2); (v2; v3); (v1; v3) 2 E(G) and e1; e2 2 Dom(E ), 1. (v1; v2) = e1 and (v2; v3) = e2 if and only if HeadTail(e1; e2); 2. (v1; v2) = e1 and (v1; v3) = e2 if and only if TailTail(e1; e2); and 3. (v1; v3) = e1 and (v2; v3) = e2 if and only if HeadHead(e1; e2). The 1-1 mapping is called a (V; E)-isomorphism.
same underlying directed graph. The following proposition states that this notion is robust.
Proposition 1. (a) Let G be a V-structure and E 1, E 2 be E-structures. If both E 1 and E 2 are structurally equivalent to G, then E 1 and E 2 are isomorphic. (b) Let G1, G2 be V-structures and E be a E-structure. If both G1 and G2 are equivalent to E , then G1 and G2 are isomorphic.
Moreover, the following proposition shows that both edge and vertex representations are equivalent, in the sense that each graph stored using the standard vertex representation can be coded as a graph under the edge representation, and vice versa. Proposition 2. 1. For every V-structure G, there exists a unique (up to isomorphism)
E-structure E which is structurally equivalent to G. 2. For every E-structure E , there exists a unique (up to isomorphism) V-structure G structurally equivalent to E .
We do not state the full proof, but rather give an example of how the edge to vertex translation works.
– Dom(E ) = fe1; e2; e3g; – HeadHead = f(e1; e1); (e2; e2); (e3; e3); (e1; e3); (e3; e1)g; – TailTail = f(e1; e1); (e2; e2); (e3; e3)g; – HeadTail = f(e1; e2); (e2; e3); (e3; e2)g.
e1
I
R e2 e3 We can get a V-structure G = (V (G); E(G)) equivalent to E as follows. Let H be the equivalent classes of HeadHead and T the equivalent classes of TailTail, i.e. H = ffe1; e3g; fe2gg and T = ffe1g; fe2g; fe3gg. Then we define G = (V (G); E(G)) as follows. The set of vertices is V (G) = H T , and ((H1; T1); (H2; T2)) 2 E(G) if and only if T1 \ H2 6= ;. It is depicted as follows.
(;; fe1g)
(fe1; e3g; fe2gI)
R (fe2g; fe3g) 4
In this section we will study the relation between the expressive power of logics using vertex or edge vocabularies. We need the following definition. For a set A STRUCT[V], we define EquivE(A) as the set of E-structures which are equivalent to the structures in A. Formally,
EquivE(A) = fE 2 STRUCT[E] j E is structurally equivalent to some G 2 Ag:
STRUCT[E], we define EquivV(B) = fG 2 STRUCT[V] j G is structurally equivalent to some E 2 Bg:
STRUCT[E],
A = EquivV(EquivE(A)) and B = EquivE(EquivV(B)) From this we immediately get that A = EquivV(B) if and only if B = EquivE(A).
Now we introduce the notion of (V; E)-equivalent, the logical version of Defintion 1.
Definition 2. A V-sentence ' and an E-sentence are (V; E)-equivalent if G(') = EquivV(G( )), or equivalently, G( ) = EquivE(G(')).
Using the notion of (V; E)-equivalent, we can now compare the expressive power between vertex and edge representations. Our first proposition shows that the edge representation is as least as expressive as the vertex representation: Proposition 3. Let L in fFO; 9MSO; MSOg. Then, for every sentence ' 2 L[V], there exists a sentence 2 L[E] such that ' and are (V; E)-equivalent The proof is pretty straightforward, thus omitted.
The natural question is whether the converse holds, that is, whether for every sentence using the edge representation we can find an equivalent sentence using the vertex representation. As we show below, it turns out that this is not true even for 9MSO sentences, nor if the full power of MSO is allowed.
Theorem 1. 1. There exists a sentence 2 9MSO[E] such that for all sentence ' 2 9MSO[V], and ' are not (V; E)-equivalent. 2. There exists a sentence 2 MSO[E] such that for all sentence ' 2 MSO[V], and ' are not (V; E)-equivalent.
in directed graph is not expressible in 9MSO[V] (see, for example, [13, Theorem 7.16]).
For this we need to add two constants s and t to both V- and E-vocabularies, denoting the source and target vertices respectively. The interpretation of the constants s and t in V-structures are the source and the target vertices, while their interpretation in E-structures are two edges: one whose tail is the source vertex, and the other whose head is the target vertex.
We define the following class of V-structures consists of directed graphs in which there is a path from s to t.
RV =
G 2 STRUCT[V] tfhoerreeaacrheiv=1; :1:;::;:v:k; ks.t. v11; (=vis;vain+d1)vk2=E(tGan)d
It can be readily seen that the class EquivE(RV) is expressible in 9MSO[E] in the following sentence. There exists a set P such that – there is an edge y in P such that TailTail(y; s) holds; – there is an edge y in P such that HeadHead(y; t) holds; – for every edge y in P where :HeadHead(y; t), there is an edge z in P such that HeadTail(y; z) holds.
This proves the first case of the theorem.
The proof for the second case goes along the same lines, this time using the fact that directed graph hamiltonicity (i.e., whether a graph is hamiltonian) is not expressible in MSO[V] (see, for example, [13, Corollary 7.24]). On the other hand, directed graph hamiltonicity can be expressed in the following MSO[E] sentence. There exists a set U such that – every two edges in U are connected (can be expressed as in the proof above); and – for every edge x, x is adjacent to some edge y in U (either HeadHead(x; y), TailTail(x; y), or HeadTail(x; y) holds); 2
Next, we compare the two representations for the case of first-order logic. It turns out that the edge and vertex representations are equivalent if one disallows second-order quantification. Moreover, we also show that this transformation involves only a slight increase in quantifier rank.
Proposition 4. For every sentence 2 FO[E], there exists a sentence ' 2 FO[V] such that they are (V; E)-equivalent and qr(') = 2qr( ).
With respect to the vertex to edge transformation, the following is immediate from the proof of proposition 3 Corollary 1. For every sentence ' 2 FO[V], there exists a sentence that ' and are (V; E)-equivalent and qr( ) = qr(') + 1. 2 FO[E] such 5
In this section we define pebble automata for directed graphs. It is based on the idea of
pebble automata (PA) for words over infinite alphabet [
Briefly the way graph PA with k pebbles works as follows. If G is a directed graph, and (a1; b1); : : : ; (an; bn) are the edges in E(G), then we feed a sequence w = ab11 abnn into graph k-PA. The pebbles are numbered from 1 to k. The automaton starts the computation with only pebble k on the sequence w. The pebbles are placed on/lifted from w in the stack discipline according to the strict order of the pebbles: Pebble i can be placed only when pebbles i + 1; : : : ; k are above the sequence w. Each pebble is intended to mark one position in w and the smallest numbered pebble on w, or, equivalently the most recently placed pebble, serves as the head of the automaton. The automaton moves from one state to another depending on whether the edges read by the pebbles satisfy the HeadHead; TailTail; HeadTail relations.
Definition 3. A two-way alternating graph k-pebble automaton, (in short graph k-PA) is a system A = hQ; q0; F; i, where – Q, q0 2 Q, U Q and F Q are a finite set of states, the initial state, the set of universal states and the set of final states, respectively; and – is a finite set of transitions of the form such that ! is of the form
(i; P; V00; V10; V01; V11; q) , where i 2 f1; : : : ; kg, P; V00; V10; V01; V11 is of the form (q; act), where q 2 Q and fi + 1; : : : ; kg, and act 2 fleft; right; place-pebble; lift-pebbleg:
Given a sequence of edges w = ab11 abnn , a configuration of A on /w. is a triple [i; q; ], where i 2 f1; : : : ; kg, q 2 Q and : fi; i + 1; : : : ; kg ! f0; 1; : : : ; n; n + 1g. The function defines the position of the pebbles and is called the pebble assignment. The symbols in the positions 0 and n + 1 are / and ., respectively.
The initial configuration is 0 = [k; q0; 0], where 0(k) = 0 is the initial pebble assignment. A configuration [i; q; ] with q 2 F is called an accepting configuration.
A transition (i; P; V00; V01; V10; V11; p) ! applies to a configuration [j; q; ], if (1) i = j and p = q, (2) P = fl > i : (l) = (i)g, (3:a) V00 = fl > i : a (l) = a (i)g, (3:b) V10 = fl > i : b (l) = a (i)g, (3:c) V10 = fl > i : a (l) = b (i)g, and (3:d) V11 = fl > i : b (l) = b (i)g.
A transition (i; P; V00; V01; V10; V11; p) ! applies to a configuration [j; q; ], if conditions (1)–(3) above hold.
We define the transition relation `A as follows: [i; q; ] `A [i0; q0; 0], if there is a transition ! (p; act) 2 that applies to [i; q; ] such that q0 = p, for all j > i, 0(j) = (j), and - if act = left, then i0 = i and 0(i) = (i) 1, - if act = right, then i0 = i and 0(i) = (i) + 1, - if act = lift-pebble, then i0 = i + 1, - if act = place-pebble, then i0 = i 1, 0(i 1) = 0 and 0(i) = (i).
The acceptance criteria is based on the notion of leads to acceptance below. For every configuration = [i; q; ], – if q 2 F , then leads to acceptance; – if q 2 U , then leads to acceptance if and only if for all configurations 0 such that ` 0, 0 leads to acceptance; – if q 2= F [ U , then leads to acceptance if and only if there is at least one configuration 0 such that ` 0, and 0 leads to acceptance.
A sequence of edges ab11 abnn is accepted by A, if the initial configuration 0 leads to acceptance. The language L(A) consists of all sequence of edges accepted by A. Obviously, the sequence w induces a set of directed edges Gw as explain in the beginning of this section.
We have presented here the notion of alternating graph PA, since it is easier to work with for our purposes. However, it is not difficult to define instead the notion of deterministic graph PA. The next theorem shows that this choice is without loss of generality, as both models are equivalent.
Theorem 2. 1. For each k 1, two-way non-deterministic graph k-PA and one-way deterministic graph k-PA have the same recognition power. 2. For each k 1, graph k-PA languages are closed under boolean operation.
Next, we introduce the relationship between graph PA and First Order logic.
Theorem 3. For every FO E-sentence , there exists a graph k-PA A
qr( ) and L(A) = G( )).
such that k =
Proof. The proof is an adaptation of similar result in [
The proof is by straightforward induction on k. A k-PA A iterates pebble k through all possible positions in the input. On each iteration, the automaton A recursively calls a (k 1)-PA A0 that accepts the language L( (xk)), treating the position of pebble k as the assignment value for xk.
- If Q = 8, then A accepts w if and only if A0 accepts on all iterations. - If Q = 9, then A accepts w if and only if A0 accepts on at least one iteration. 2
Notice that Theorem 3 is optimal in the sense that all k pebbles are needed. More
precisely, it is possible to adapt the proof of [
In the usual graph databases setting the edges are labeled with symbols from a fixed finite alphabet. Each symbol can be viewed as a unary predicate on the edges.
In this section we extend the vocabularies V and E with unary predicates on the edges, which we called extended V and E vocabularies. We also extend the definition of graph pebble automata for edges labeled with symbols from a fixed alphabet.
In the following we let be a fixed finite alphabet.
Extended V logic. The vocabulary for the extended V logic consists of for each
V logic.
An extended V-structure is a tuple G = (V; f g 2 ) such that V is the domain of nodes and the sets f g 2 are disjoints. Intuitively, each relation denotes the set of edges which are labeled with the symbol 2 . Since no edge can be labeled with two different symbols, the sets f g 2 are disjoint.
Extended E logic. The vocabulary consists of HeadHead; HeadTail; TailTail; f g 2 , where each 2 is unary predicate on the domain. We denote by E the extended E logic.
An extended E-structure is a tuple E = (U; HeadHead; HeadTail; TailTail; f g 2 ), where U is the domain of edges, the relations HeadHead; HeadTail; TailTail on U are defined as before, and each 2 is a unary predicate on U .
It is straightforward to show that all results on the vocabularies V and E still hold for the extended logics V and E . In the following we will elaborate this point more precisely.
Definition 4. Let G be an V structure and E an E structure. We say that G and E are structurally equivalent if there exists a 1-1 mapping : E(G) ! Dom(E ) such that for all (v1; v2); (v2; v3); (v1; v3) 2 S 2 and e1; e2 2 Dom(E ), 1. for each 2 , (v1; v2) 2 if and only if (v1; v2) 2 ; 2. (v1; v2) = e1 and (v2; v3) = e2 if and only if HeadTail(e1; e2); 3. (v1; v2) = e1 and (v1; v3) = e2 if and only if TailTail(e1; e2); and 4. (v1; v3) = e1 and (v2; v3) = e2 if and only if HeadHead(e1; e2).
The 1-1 mapping is called a (V ; E )-isomorphism.
Theorem 4. 1. Let L in fFO; 9MSO; MSOg. Then, for every sentence ' 2 L[V ], there exists a sentence 2 L[E ] such that ' and are (V ; E )-equivalent 2. There exists a sentence 2 9MSO[E ] such that for all sentence ' 2 9MSO[V ], and ' are not (V ; E )-equivalent. 3. There exists a sentence 2 MSO[E ] such that for all sentence ' 2 MSO[V ], and ' are not (V ; E )-equivalent.
Next we define a graph pebble automata with unary predicates on the edges. It is also pretty much straightforward extension of Definition 3. In this case the input is of 0 1 1 0 n 1 the form: @ a1 A @ an A 2 D D, where i 2 is the label of the edge b1 bn (ai; bi).
The transitions are of the form: (i; ; P; V00; V10; V01; V11; p) ! (q; act). It is straightforward to show that all the results in the previous section can be adapted for such graph pebble automata. More precisely, Theorem 5. 1. For PA with unary predicates, for each k 1, two-way non-deterministic graph k-PA and one-way deterministic graph k-PA have the same recognition power. 2. For each k 1, graph k-PA (with unary predicates) languages are closed under boolean operation. 3. For every FO E -sentence , there exists a graph k-PA A with unary predicates such that k = qr( ) and L(A) = G( )).
We would like to apply our logics and graph pebble automata in a more application oriented settings. Also, it is well known that the emptiness problem for graph pebble automata is undecidable. One direction that we would like to pursue is to charaterize a subclass of pebble automata, for which the emptiness problem is decidable. We also would like to define and study similar logics for matroid and extend the graph pebble automata for abstract matroid.
Acknowledgments: We thank the anonymous referees for many helpful comments. Partial support provided by EPSRC grant G049165 and FET-Open Project FoX, grant agreement 233599.