Expressiveness of graph conditions with variables


Electronic Communications of the EASST

Volume 30 (2010)

International Colloquium on Graph and Model

Transformation On the occasion of the 65th birthday of

Hartmut Ehrig

(GraMoT 2010)

Expressiveness of graph conditions with variables

Annegret Habel and Hendrik Radke

18 pages

Guest Editors: Claudia Ermel, Hartmut Ehrig, Fernando Orejas, Gabriele Taentzer

Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer

ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122

http://www.easst.org/eceasst/


ECEASST

Expressiveness of graph conditions with variables

Annegret Habel1 and Hendrik Radke2∗

1 habel@informatik.uni-oldenburg.de
2 radke@informatik.uni-oldenburg.de

Carl von Ossietzky Universität Oldenburg, Germany

Abstract: Graph conditions are very important for graph transformation systems

and graph programs in a large variety of application areas. Nevertheless, non-local

graph properties like “there exists a path”, “the graph is connected”, and “the graph

is cycle-free” are not expressible by finite graph conditions. In this paper, we gen-

eralize the notion of finite graph conditions, expressively equivalent to first-order

formulas on graphs, to finite HR+ graph conditions, i.e., finite graph conditions with

variables where the variables are place-holders for graphs generated by a hyperedge

replacement system. We show that graphs with variables and replacement mor-

phisms form a weak adhesive HLR category. We investigate the expressive power

of HR+ graph conditions and show that finite HR+ graph conditions are more ex-

pressive than monadic second-order graph formulas.

Keywords: Graph conditions, graphs with variables, hyperedge replacement sys-

tems, monadic-second order formulas, weak adhesive HLR categories.

1 Introduction

Graph transformation systems have been studied extensively and applied to several areas of com-

puter science [Roz97, EEKR99, EKMR99]. Graph conditions, i.e., graph constraints and appli-

cation conditions, studied, e.g., in [EH86, HHT96, HW95, KMP05, EEHP06, HP09], are very

important for graph transformation systems in a large variety of application areas. Graph con-

ditions are an intuitive, graphical, yet precise formalism, well-suited for describing structural

properties. Moreover, finite graph conditions and first-order graph formulas are expressively

equivalent [HP09]. Unfortunately, non-local graph properties like “there exists a path”, “the

graph is connected”, and “the graph is cycle-free” are not expressible by first-order graph formu-

las [Cou90a, Cou97] and finite graph conditions. They only can be expressed by infinite graph

conditions.

In this paper, we generalize the concept of graph conditions to graph conditions with variables

where the variables are place-holders for graphs generated by a hyperedge replacement (HR)

system. By the HR system, we obtain a finite description of a set of graphs that is infinite in

general, like the set of all paths. We state that graphs with variables and replacement morphisms

form a weak adhesive HLR category. We introduce HR conditions as conditions over graphs with

variables (together with a HR system) and HR+ conditions as extensions of HR conditions by

∗ This work is supported by the German Research Foundation (DFG) under grant GRK 1076/1 (Graduate School on

Trustworthy Software Systems).

1 / 18 Volume 30 (2010)

mailto:habel@informatik.uni-oldenburg.de
mailto:radke@informatik.uni-oldenburg.de


Graph conditions with variables

conditions of the form x◦ ⊑ X , related to monadic second order (MSO) formulas x ∈ X . It turns
out that the validation problem for finite HR+ conditions and graphs is decidable. We show that

MSO graph formulas can be expressed by equivalent HR+ conditions and that HR conditions

can express second-order (SO) graph formulas.

The usefulness of HR conditions is illustrated by an example of a car platooning maneuver

protocol.

Example 1 (Car platooning) We study “a prototypical instance of a dynamic communication

system”, originally taken from the California Path project [HESV91]. It represents a protocol for

cars on a highway that can organize themselves into platoons, by driving close together, with the

aim to conserve space and fuel. A car platoon is modeled as a directed graph where the nodes

represent the cars and the direct edges the direct follower relation. Additionally the leader of

a car platoon is marked by the ”dark grey” color (resp. by a loop) where the color is used in

figures, representing the loop in the formal definition.

A car platooning state graph consists of zero or more car platoons.

Car platooning operations like splitting a car platoon in two, or joining two car platoons into

a single one can be described by graph replacement rules. When performing these operations,

certain car platooning properties have to be satisfied.

(1) Every follower has a unique leader:

∀( 1 ,∃( 1 )∨(∃( 1 + )∧∄( 1
+

+

)))

(2) Leaders are not connected: ∄( + )

(3) The car platooning state is circle-free: ∄(
+

)

where the HR system + ::= 12 | 12
+

generates the set of all non-empty paths from 1 to 2. The car platooning properties are de-

scribed by HR conditions. Bauer [Bau06] and Pennemann [Pen09] model the follower relation

with respect to the leader, but not the order of the followers. HR conditions allow to express path

conditions as in the car platooning example.

The paper is organized as follows: In Section 2, we introduce graphs with variables and state

that graphs with variables and replacement morphisms form a category. In Section 3, we gener-

alize graph conditions to HR and HR+ conditions, i.e., graph conditions with variables equipped

Proc. GraMoT 2010 2 / 18



ECEASST

with a hyperedge replacement (HR) system, and present a number of examples for HR condi-

tions. In Section 4, we show that the validity problem for HR+ graph conditions is decidable. In

Section 5, we investigate the expressiveness of HR+ conditions. In Section 6, we present some

related concepts. A conclusion including further work is given in Section 7. X

2 Graphs with variables

Graphs with variables consist of nodes, edges, and hyperedges. Edges have one source and one

target and are labeled by a symbol of an alphabet; hyperedges have an arbitrary sequence of

attachment nodes and are labeled by variables.

Definition 1 (Graphs with variables) Let C =〈CV,CE,X〉 be a fixed, finite label alphabet where
X is a set of variables with a mapping rank : X →N0 defining the rank of each variable. A graph
with variables, short X-graph, over C is a system G = (VG,EG,YG,sG,tG,attG,lvG,leG,lyG)
consisting of finite sets VG, EG, and YG of nodes (or vertices), edges, and hyperedges, source and

target functions sG,tG : EG →VG, an attachment function attG : YG →V
∗
G, and labeling functions

lvG : VG → CV, leG : EG → CE, ly : YG → X such that, for all y ∈ YG, |attG(y)| = rank(lyG(y)).
GX denotes the set of all X-graphs. For YG = /0, G is a graph; G denotes the set of all graphs.

Remark 1 The definition extends the well-known definition of graphs [Ehr79] by the concept

of hyperedges in the sense of [Hab92]. X-graphs also may be seen as special hypergraphs where

the set of hyperedges is divided into a set of edges labelled with terminal symbols and a set of

hyperedges labelled by nonterminal symbols.

We extend the definition of graph morphisms to the case of graphs with variables.

Definition 2 (Graph morphisms with variables) A morphism over graphs with variables, short

(X-graph) morphism, g : G → H consists of functions gV : VG → VH , gE : EG → EH , and an
injective function gY : YG → YH that preserve sources, targets, attachment nodes, and labels,
that is, sH ◦gE = gV ◦sG, tH ◦gE = gV ◦tG, attH = g

∗
V ◦attG, lvH ◦gV = lvG, leH ◦gE = leG, and

lyH ◦gY = lyG.
1 For YH = /0, g is a (graph) morphism. A morphism g is injective (surjective) if

gV, gE, and gY are injective (surjective), and an isomorphism if it is both injective and surjective.

In the latter case G and H are isomorphic, which is denoted by G ∼= H . The composition h◦g of
g with a morphism h : H → M consists of the composed functions hV ◦gV, hE ◦gE, and hY ◦gY.
For an X-graph G, the identity idG : G → G consists of the identities idGV, idGE, and idGY on GV,
GE, and GY, respectively.

Example 2 Consider the X-graphs G and H over the label alphabet C =〈{A,B},{2},X〉 below
where the symbol 2 stands for the invisible edge label and is not drawn and X ={u,v} is a set of
variables that have rank 4 and 2, respectively. The X-graph G contains five nodes with the labels

A and B, respectively, seven edges with label 2 which is not drawn, and one hyperedge of rank

4 with label u. Additionally, the X-graph H contains a node, an edge, and a hyperedge of rank 2

1 For a mapping g : A → B, the free symbolwise extension g∗ : A∗ → B∗ is defined by g∗(a1 ...ak) = g(a1)...g(ak)
for all k ∈N and ai ∈ A (i = 1,...,k).

3 / 18 Volume 30 (2010)



Graph conditions with variables

with label v.

A 2

B1 B 3

B5 B 4

u
1

2
3

4

G

→֒

A 2

B1 B 3

B5 B
4

B

u
1

2
3

4
v1 2

H

The drawing of X-graphs combines the drawing of graphs in [Ehr79] and the drawing of hyper-

edges in [Hab92, DHK97]: Nodes are drawn by circles carrying the node label inside, edges are

drawn by arrows pointing from the source to the target node and the edge label is placed next

to the arrow, and hyperedges are drawn as boxes containing the label, which are connected by

lines to their attachment nodes v1,...,vk so that the line to vi has the number i written next to it.
For simplicity, binary hyperedges also can be drawn like edges. Arbitrary morphisms are drawn

by usual arrows “→”; the use of “→֒” indicates an injective morphism. The actual mapping of
elements is conveyed by indices, if necessary.

Hyperedges do not only play a static part as building blocks of X-graphs, but also a more

dynamic part as place holders for graphs. Before an X-graph can take the place of a hyperedge,

it needs some preparation. While a hyperedge is attached to a sequence of attachment nodes, an

X-graph has to be equipped with a sequence of nodes.

Definition 3 (Pointed graphs with variables) A pointed X-graph 〈R,pointsR〉 is an X-graph R
together with a sequence pointsR = v1 ... vn of pairwise distinct nodes from R. We write rank(R)
for the number n of nodes. For x ∈ X with rank(x) = n, x• denotes the pointed X-graph with the
nodes v1,...,vn, one hyperedge labeled by x and attached to v1 ... vn, and sequence v1 ... vn. G

•
X

denote the set of all pointed X-graphs.

Variables are replaced by graphs generated by a hyperedge replacement system.

Definition 4 (HR systems) A hyperedge replacement (HR) system R over X is a finite set of

replacement pairs of the form x/R where x is a variable in X and R a pointed X-graph with
rank(x) = rank(R).

x /
•

• •

•1

2 3

4

R

Given an X-graph G, the application of the replacement pair x/R to a hyperedge y with label
x proceeds in two steps: (1) Remove the hyperedge y from G, yielding the X-graph G−{y}.
(2) Construct the disjoint union (G−{y})+R and fuse the i th node in attG(y) with the i

th attach-

ment point of R, for i = 1,...,rank(y), yielding the X-graph H .

Proc. GraMoT 2010 4 / 18



ECEASST

•

• •

•

G−{y} x

1

2

3

4

=⇒
x/R

•

• •

•

G−{y} R

An X-graph G directly derives H by x/R applied to y, denoted by G ⇒x/R,y H or G ⇒R H
provided that x/R ∈ R. A sequence of direct derivations G ⇒R ... ⇒R H is called a derivation
from G to H , denoted by G ⇒∗

R
H . For every variable x in X, R(x) = {G ∈ G | x• ⇒∗

R
G}

denotes the set of all graphs derivable from x◦ by R.

Example 3 The HR system R with the rules + ::=
1 2

|
1 2

+
given in Backus-Naur

form (presented in the introduction) generates the set of all directed paths from node 1 to node 2.

Assumption In the following, let R be a fixed HR system.

Given an X-graph, there are two ways to get rid of variables: (A) Apply a substitution ac-

cording to a mapping from the variables, i.e., labels of the hyperedges, to graphs. Then same-

labelled hyperedges are replaced by the same graph. (B) Apply a base for replacement according

to mapping from the hyperedges to graphs. Then, same-labelled hyperedges may be replaced

differently. In [PH96] and [Pra04], hyperedges are substituted by graphs. In the following,

hyperedges are replaced by graphs. By our opinion, replacement is the more adequate.

HR systems are used to define the set of admissible replacements.

Definition 5 (Replacement) Let G be an X-graph and Y ⊆ YG a set of hyperedges to be re-
placed. A mapping repl : Y → G • is a base for replacement in G if, for all y in Y, repl(y) is
in R(ly(y)). The replacement of Y in G by repl, denoted by repl(G), is obtained from G by
simultaneously replacing all hyperedges y in Y by repl(y). If repl(G) is H , up to isomorphism,

we write G
repl
=⇒H .

G−Y

• •

• •

•

•

•

•

•

•

•

•

x11
2

3

4

x2
1

2
3

x3
1

2

x4
1 2

3

repl
=⇒ G−Y

• •

• •

•

•

•

•

•

•

•

•

R1

R2

R3

R4

Fact 1 (Commutativity)

(1) Given G′
repl
⇐=G

g′

→H′, there exists a pushout G′
g
→H

repl′

⇐=H′.

(2) Given G′
g
→H

repl′

⇐= H′, there exists a pullback G′
repl
⇐= G

g′

→H′.

5 / 18 Volume 30 (2010)



Graph conditions with variables

(3) Given G
g′

→H′
repl′

=⇒H , there exists a pushout complement G
repl
=⇒G′

g
→H .

G H′

G′ H

g′

repl repl′

g

(1)

Construction (1) We make use of the fact that every item in an X-graph G′ is in G−Y or in
repl(Y•)− obtained from repl(Y•) by removing all attachment nodes of hyperedges in Y. Let
repl′ : g′Y(Y) → G

• be a base for replacement in H′ with repl′ = repl◦g′Y
−1

and g : G′ → H be
the morphism with g = g′[G−Y] and g = id[repl(Y•)−]2. (2) Let repl : gY

−1(Y′)→G • be a base
for replacement in G with repl = repl′◦g and g′ : G → H′ be the morphism with g′=g[G−Y] and
g′=id[Y]. (3) Let repl : g′Y

−1
(Y ′) → G • be a base for replacement in G with repl = repl′◦g′ and

g : G′ → H be the morphism with g=g′[G−Y], and g = id[repl(Y )−].

Remark 2 The injectivity of gY guarantees the well-definedness of the bases for replacement.

Replacement morphisms consist of a base for replacement and a graph morphism.

Definition 6 (Replacement morphisms) A replacement morphism 〈repl,g〉: G ։ H consists of
a base for replacement repl in G and a graph morphism g : repl(G) → H . It is injective up to
replacement if the restriction g|G−YG

3 is injective and injective if g is injective.

Definition 7 (Identity and Composition) The replacement morphism 〈/0,idG〉 with empty base
for replacement and identity idG : G →֒ G is called identity. Given replacement morphisms
〈repl1,g1〉: G ։ H and 〈repl2,g2〉: H ։ I, the composition 〈repl,g〉: G ։ I is given by repl =
repl′2 ◦repl1 and g = g2 ◦g

′
1.

G G′ H

H′

I

G′′

repl1

repl′2 repl2
repl

g1

g′1

g2
g

=

=

Fact 2 (Composition) The composition of replacement morphisms is a replacement morphism.

X-graphs and replacement morphisms form a category; this category with the class of all

injective graph morphisms is weak adhesive HLR.

2 For graph morphisms gi : Gi → H with G ⊆ Gi (i = 1,2), g1=g2[G] abbreviates g1|G = g2|G.
3 For a graph morphism g : G → H, g|G−YG denotes the restriction of g to G−YG .

Proc. GraMoT 2010 6 / 18



ECEASST

Theorem 1 (XGraphs is weak adhesive HLR) X-graphs and replacement morphisms form the

category XGraphs. The category 〈XGraphs,M〉 of X-graphs with the class M of all injective
graph morphisms is a weak adhesive HLR and has an M -initial X-graph and epi-M factoriza-

tion.

Proof. By associativity and identity of replacements and graph morphisms and the definition of

weak adhesive HLR.

3 HR and HR+ conditions

Graph conditions are a well-known concept for describing graph properties in a graphical way

by graphs and graph morphisms (see e.g. [EH86, HHT96, HW95, KMP05, EEHP06, HP09]).

In the following, we generalize the concept to HR and HR+ conditions. HR conditions are

conditions in the category of X-graphs where the variables may be replaced by graphs generated

by a hyperedge replacement (HR) system. HR+ conditions are extensions of HR conditions by

conditions of the form x◦ ⊑ X with the meaning “is included in”, a counterpart to the MSO
formulas of the form x ∈ X with the meaning “is element in”.

Definition 8 (HR and HR+ conditions) HR-conditions, short conditions, are inductively de-

fined as follows: For an X-graph P, true is a condition over P. For every morphism a : P → C
and every condition c over C, ∃(a,c) is a condition over P. For conditions c,ci over P with
i ∈ I (for all index sets I), ¬ c and ∧i∈I ci are conditions over P. HR

+ conditions are defined by

adding: For X-graphs x◦, X ⊆ P, the expression x◦ ⊑ X is a condition over P where, for an
item x∈ VP +EP, x

◦ denotes the graph induced by x, i.e., the graph with the single node x and the

edge x together with its source and target, respectively. A condition is finite, if every conjunction

is finite.

Notation The expression false abbreviates the condition ¬true. For an index set I, the ex-
pression ∨i∈I ci abbreviates the condition ¬∧i∈I ¬ci, c1 ⇒ c2 abbreviates ¬c1 ∨c2, ∃a abbre-
viates ∃(a,true), and ∀(a,c) abbreviates ¬∃(a,¬c). For a morphism a : P → C in a condi-
tion, we just depict C, if P can be unambiguously inferred, i.e. for constraints over the empty

graph /0 and for conditions over some left- or right-hand side of a rule. E.g., the condition

∃(/0 →
1

+
1

2
,∄(

1
+

1

2
→

1
+

1

2
)) is abridged ∃(

1
+

1

2
,∄(

1
+

1

2
)).

Remark 3 The definition generalizes the definitions in [HHT96, HW95, KMP05, EEHP06].

HR-conditions are conditions over X-graphs [HP09]. Variables in finite conditions may be re-

placed by graphs generated by a corresponding HR system. In this way, an infinite number of

conditions is expressed by a finite HR condition. IHR+ conditions extend HR-conditions by sub-

conditions the form x◦ ⊑ X . Typical examples are x ⊑ X with X ::= /0 | X and ⊑ X
with X ::= /0 | X . With this extension, there is a transformation of MSO formulas into
equivalent HR+ conditions (see Theorem 3).

Remark 4 For conditions, the underlying HR system R is important: For a condition c, this

may be expressed explicitly by the pair 〈c,R〉 meaning that the variables in c may be replaced

7 / 18 Volume 30 (2010)



Graph conditions with variables

by graphs derived by R.

Let B′ denote the class of all replacement morphisms, injective up to replacement, and A ′ be

the class of all replacement morphisms.

Definition 9 (B′- and A ′-satisfiability) (B′-) satisfiability of conditions are inductively de-

fines as follows: Every replacement morphism satisfies true. A replacement morphism p : P ։ G

satisfies ∃(a,c) if there exists a replacement morphism q in B′ such that q◦a = p and q satis-
fies c.

P

G

C,
a

p q
=

c

|=
∃( )

A replacement morphism p : P ։ G satisfies the condition x◦ ⊑ X if p(x◦)⊆ p( X ). p satisfies
¬c iff p does not satisfy c, and p satisfies ∧i∈I ci iff p satisfies all ci (i∈ I). An X-graph G satisfies
a condition c, if c is a condition over /0 and the morphism /0 → G satisfies c. We write p |= c to
denote that p satisfies c and G |= c to denote that G satisfies c. The notion of A ′-satisfiability is
obtained from B′-satisfiability by replacing all occurrences of B′ by A ′. We write p |=A ′ c to
denote that p A ′-satisfies c and G |=A ′ c to denote that G A

′-satisfies c.

The following monadic second-order graph properties can be expressed by HR conditions.

Example 4 (MSO graph properties) For the HR system with the rules + ::=
1 2

|
1 2

+
,

we have the following.

Simple paths. A nonempty path in G is here a sequence of nodes (v1,v2,...,vn) with n ≥ 2
such that there is an edge with source vi and target vi+1 for all i and vi = v j ⇒{i, j} ={1,n}; if
v1 = vn, this path is a cycle. If in a path each node only appears once, then it is called a simple
path; if each node appears once except that v1 = vn, then it is a simple cycle. The HR condition
path(1,2) =∃(

1 2
→

1 2

+
) requires that there is a simple, nonempty path from the image

of 1 to the image of 2.

Connectedness. The HR condition connected = ∀(
1 2

,path(1,2)) requires that, for each
pair of distinct nodes, there is a simple, nonempty path, i.e., the graph is strongly connected.

Cycle-freeness. The HR condition cyclefree = ∄(
1

+ ) requires that the graph is cycle-
free.

Planarity. By Kuratowski’s Theorem (see e.g. [Eve79]) a graph is planar if and only if it has

no subgraph homeomorphic to K3,3 or K5. For undirected graphs, two graphs are homeomor-

phic if both can be obtained from the same graph by insertion of new nodes of degree 2, in

edges, i.e. an edge is replaced by a path whose intermediate nodes are all new. The HR con-

dition planar = ∄(K∗5 )∧∄(K
∗
3,3) where K

∗
5 and K

∗
3,3 are obtained from the graphs K5 and K3,3

by replacing all edges by hyperedges with label x, respectively, requires that the graph has no

subgraph homeomorphic to K5 or K3,3, i.e. that the graph is planar.

Coloring. A coloring of a graph is an assignment of colors to its nodes so that no two adjacent

nodes have the same color. A k-coloring of a graph G uses k colors. By König’s characterization

Proc. GraMoT 2010 8 / 18



ECEASST

(see e.g. [Har69]), a graph is 2-colorable if and only if it has no odd cycles. For undirected

graphs, i.e., graphs in which each undirected edge stands for two directed edges in opposite

direction, the HR condition 2color = ∄(
1

+2 ) with +2 ::=
1 2

|
1 2

+2
requires

that there are no cycles of odd length, i.e., the graph is 2-colorable.

Hamiltonicity. A graph is Hamiltonian, if there exists a Hamiltonian circuit, i.e. a simple circuit

on which every node of the graph appears exactly once (see e.g. [Eve79]). For undirected graphs,

the HR condition hamiltonian = ∃(
1

+ ,∄(
1

+ )) with + ::=
1 2

|
1 2

+
, re-

quires that there exists a simple circuit in the graph and there is no additional node in the graph,

i.e. every node of the graph lies on the circuit, the graph is Hamiltonian.

The following second-order graph properties can be expressed by HR conditions.

Example 5 (SO graph properties) The following second-order properties (which are not MSO-

expressible) can be expressed by HR graph conditions.

Even number of nodes. The HR condition even = ∃( X ,∄( X )) with X ::= /0 | X
expresses the SO property “the graph has an even number of nodes”.

Equal number of a’s and b’s. The HR condition equal = ∃( X ,∄( X a )∧∄( X b )) with
X ::= /0 | a b X expresses the SO property “the graph has as many nodes labelled a as b”.

Paths of same length. The HR condition 2paths1,2 = ∃( 1 2 → 1 2+
1

3 4

2

) with + ::=
1 2

3 4 |
1

3

2

4
+

1 2

3 4
expresses the SO property “there exist two node-disjoint paths of same

length from the image of 1 to the image of 2”.

Remark 5 (Counting MSO graph properties) Counting MSO [Cou90b] extends MSO with first-

order modulo-counting quantifiers such as “there exists an even number of elements such that

...”. E.g., the SO graph property “even number of nodes” is counting MSO.

4 Decidability of the validity problem

In this section, we show the undecidability of the satisfiability problem for HR conditions and

the decidability of the validity problem for HR+ conditions and graphs. By the undecidability

of the satisfiability problem of first-order graph formulas [Tra50, Cou90a] and the equivalence

of first-order graph formulas and finite graph conditions [HP09], we obtain the undecidability of

the satisfiability problem of HR conditions.

Fact 3 (Undecidability of the satisfiability problem) The satisfiability problem is undecidable,

i.e., there is no algorithm for determining whether or not, given a finite HR condition c, there

exists a replacement morphism p such that p |= c [there exists a graph G such that G |= c].

HR condition c Is c satisfiable ?

∃G. G |= c ?
yes/no

The validity problem for HR+ conditions is decidable.

9 / 18 Volume 30 (2010)



Graph conditions with variables

Theorem 2 (Decidability of the validity problem) The validity problem is decidable, i.e., there

is an algorithm for determining whether or not, given a finite HR+ condition c and a replacement

morphism p, p |= c [given a finite HR+ condition c and a graph G, G |= c].

Does G satisfy c ?

G |= c ?
yes/no

HR+ condition c

graph G

Proof. Let c be a finite HR+ condition with variables and corresponding HR system R. Without

loss of generality, we may assume that R is monotone, i.e., size(x◦) ≤ size(R) for each x/R ∈
R. Otherwise, we transform it into an equivalent monotone one [Hab92]. Let p : P ։ G be a

replacement morphism and size(G) = |VG|+|EG| = n for some n ≥ 0. Let G
n denote the set of

all graphs of size ≤ n. By induction, it can be shown that, for all x ∈ X, n ∈N0, and C ∈ GX, the
sets

R
n(x) = {G ∈ G n | x◦ ⇒∗

R
G}

Repln(C) = {repl ∈ Repl | repl(y) ∈ Rn(ly(y)) for all y ∈ YC}
R

n(C) = {repl ∈ Repln(C) | repl(C)≤ n}

can be constructed effectively. For HR conditions of the form c =∃(a,d), we have p |= c ⇔ p |=
∨

repl′∈Rn c. Since R
n(C) is finite, the condition

∨

repl∈Rn(C) repl(d) is finite. In this way, for exis-
tential subconditions, satisfiability can be tested and, for non-existential conditions, satisfiability

can be checked. For a HR condition c over /0 and a graph G, G |= c ⇔ /0 → G |= c.

Remark 6 Theorem 2 can be extended to monotonic replacement systems, i.e., replacement

systems consisting of a set of rules of the form 〈L ←֓ K →֒ R〉 in the double-pushout approach
[Ehr79] with size(L) ≤ size(R).

5 Expressiveness of HR+ conditions

For investigating the expressiveness of HR+ conditions, we compare HR+ conditions and monadic

second-order (MSO) formulas on graphs [Cou90a, Cou97]. We show that there is a transfor-

mation from MSO formulas into “equivalent” HR+ conditions. Vice versa, there is no such a

transformation: HR+ conditions can express counting MSO graph properties [Cou90b].

Let Rel be a finite set of relation symbols. Let Var contain individual variables and relation

variables of arity one. Since a relation with one argument is nothing but a set, we call these

variables set variables. A monadic second-order formula over Rel is a second-order formula

written with Rel and Var: the quantified and free variables are individual or set variables; there

is no restriction on the arity of symbols in Rel. In order to get more readable formulas, we shall

write x
.
= y instead of

.
= (x,y) and x ∈ X instead of X(x) where X is a set variable. For simplicity,

we consider graphs G with common label alphabet C and common labeling function lG for nodes

and edges.

Definition 10 (MSO graph formulas) Let Var be a countable set of individual and set variables.

The set of all monadic second-order (MSO) formulas (over Var and C) is inductively defined as

Proc. GraMoT 2010 10 / 18



ECEASST

follow: For b ∈ C and x,y,z,X ∈ Var, labb(x), inc(x,y,z), x
.
= y, and x ∈ X are formulas. For

formulas F , Fi (i ∈ I) and variables x,X ∈ Var, ¬F , ∧i∈I Fi, ∃xF , and ∃X F are formulas. For
a formula F , Free(F) denotes the set of all free variables of F .4A MSO formula is closed, if
Free(F) is empty.

Notation For a (finite) index set I, the expression ∨i∈I Fi abbreviates the formula ¬∧i∈I ¬Fi,
F ⇒ G abbreviates ¬F ∨G, ∀xF abbreviates ¬∃x¬F, and ∀X F abbreviates ¬∃X¬F. Moreover,
the expression edg(y,z) abbreviates the formula ∃x.inc(x,y,z).

Definition 11 (Satisfiability) The semantic GJFK(σ) of a formula F in a non-empty graph
G with DG = VG+EG+P(VG)+P(EG)

5 under assignment σ : Var → DG is inductively de-
fined as follows: GJlabb(x)K(σ) = true iff σ(x) = lG(b), GJinc(x,y,z)K(σ) = true iff σ(x)∈ EG,
sG(σ(x)) = σ(y), and tG(σ(x)) = σ(z), GJx

.
= yK(σ) = true iff σ(x) = σ(y), GJx∈X K(σ) = true

iff σ(x) ∈ σ(X), GJ∃x FK(σ) = true iff GJFK(σ{x/d}) = true for some d ∈ DG where, for
some x ∈ Var and some d ∈ DG, σ{x/d} is the modified assignment with σ{x/d}(x) = d and
σ{x/d}(y) = σ(y) otherwise. The semantics is extended to the operators in the usual way:
GJtrueK(σ) = true, GJ¬FK(σ) = ¬GJFK(σ), and GJ∧i∈I FiK(σ) = ∧i∈I GJFiK(σ). A graph G
satisfies a formula F , denoted by G |= F , iff, for all assignments σ : Var → DG, GJFK(σ) = true.

Example 6 The MSO formula F0(x1,x2) =∀X((∀y∀z(y∈X∧edg(y,z)⇒z∈X)∧∀y(edg(x1,y)
⇒ y ∈ X))⇒ x2 ∈ X) with free variables x1 and x2 expresses the property “There is a nonempty
path from x1 to x2” [Cou97]. The formula F1(x1,x2) = x1

.
= x2∨F0(x1,x2) expresses the property

“x1 = x2 or there is a nonempty path from x1 to x2” and the formula F2 = ∀x1 ∀y2 F1(x1,x2)
expresses the property “the graph is strongly connected”.

MSO formulas and HR+ conditions are closely related. More precisely, MSO formulas can

be transformed into A ′-satisfiable HR+ conditions.

Theorem 3 (From MSO formulas to A ′-satisfiable HR+ conditions) There is a transformation

Cond from MSO formulas to HR+ conditions such that for all MSO formulas F and all graphs G,

G |= F ⇐⇒ G |=A ′ Cond(F).

Proof. Let F be a MSO formula. Without loss of generality, we may assume that F is closed

and rectified, i.e. distinct quantifiers bind occurrences of distinct variables; otherwise, we build

the universal closure of F and rename the variables. Since F is rectified, the variables of F

can be represented by isolated nodes, edges, and hyperedges in the graphs of a constructed

condition. Let P be an X-graph, IsoP the set of all isolated nodes in P, D
′
P = IsoP + EP + YP.

If D′P ⊆ Var, then every replacement morphism p : P ։ G into a non-empty graph G induces an
assignment σ : Var → DG such that p = σ[D

′
P], i.e., p(x) = σ(x) for each x ∈ D

′
P. Vice versa,

every assignment σ : Var → DG induces a replacement morphism p : P ։ G with p = σ[D
′
P].

4 For a MSO formulas, the set of free variables is defined inductively as for first-order formulas.
5 For a set A, P(A) denotes the power set of A.

11 / 18 Volume 30 (2010)



Graph conditions with variables

PDPD
′
PFree(F)

GDGVar

⊆ ⊆

⊇ p
σ

=

Construction For a MSO formula F , the HR+ condition is given by Cond(F) = Cond(/0,F).
For an X-graph P and a MSO formula F with Free(F)⊆D′P ⊆Var, the HR

+ condition Cond(P,F)
is constructed as follows:

Cond(P,labb(x)) = true if lP(x) = b; false otherwise.

Cond(P,inc(x,y,z)) = ∃(P → PsP(x)=y,tP(x)=z) if x ∈ EP, y,z ∈ VP where Px1=y1,x2=y2 is obtained
from P by identifying the pairs (x1,y1),(x2,y2); false otherwise.

Cond(P,x
.
= y) = ∃(P → Px=y) if x and y are identifiable in P, i.e., x,y ∈ VP and lP(x) = lP(y)

or x,y ∈ EP, sP(x) = sP(y), tP(x) = tP(y), and lP(x) = lP(y) or x,y ∈ P(VP)+P(EP) and
there exist morphisms a : x◦ → P and b : y◦ → P from the graphs induced by x and y,
respectively, such that a(x) = a(y).

Cond(P,x ∈ X) =
∨2

i=1〈x
◦ ⊑ X ,Ri〉; false otherwise.

Cond(P,∃xF) =
∨

b∈C∃(P → Pb,Cond(Pb,F))∨
∨

b,d,d′∈C∃(P → Pbdd′,Cond(Pbdd′,F))∨
∨2

i=1〈∃(P → P+ X ,Cond(P+ X ,F)),Ri〉 where Pb is obtained from P by adding a node
x with label b, Pbdd′ by adding an edge x with label b together with a d-labeled source

and a d′-labeled target, R1 : X ::= /0 | x b for b ∈ C, and R2 : x ::= /0 | x d d
′b for

b,d,d′ ∈ C.

For Boolean formulas over formulas, the transformation is extended as usual: Cond(P,true) =
true, Cond(P,¬F) =¬Cond(P,F), and Cond(P,∧i∈I Fi) =∧i∈I Cond(X,Fi). For Boolean formu-
las over HR+ conditions with variables 〈c,R〉 and 〈ci,Ri〉 (i ∈ I) with pairwise distinct sets free
variables6 , Cond(P,true) = 〈true, /0〉, ¬〈c,R〉 = 〈¬c,R〉 and ∧i∈I〈ci,Ri〉= 〈∧i∈I ci,∪i∈I Ri〉.

There is a nice relationship between the satisfiability of MSO formulas and the A ′-satisfiability

of the corresponding HR+ conditions.

Claim 1 For all rectified MSO formulas F , all graphs G, all assignments σ : Var → DG, and all
replacement morphisms p : P ։ G with σ = p[D′P], GJFK(σ) = true ⇐⇒ p |=A ′ Cond(P,F).

Proof (of the claim) The proof makes use of the proof of the corresponding statement for

rectified first-order formulas given in [HP09] and is done by structural induction.

Basis. For the atomic formulas labb(x), inc(x,y,z), and x
.
= y, the proof is as in [HP09]. For

atomic formulas of the form x ∈ X , the statement follows by the semantics of x ∈ X , p = σ[D′P],
x,X ∈ Free(x ∈ X)⊆ D′P, the semantics of x

◦ ⊑ X , and the definition of Cond:

6 Without loss of generality, we may assume that, for a collection of HR+ conditions 〈ci,Ri〉 (i ∈ I), the sets of free
variables are pairwise disjoint. Otherwise, we rename the free variables in the conditions.

Proc. GraMoT 2010 12 / 18



ECEASST

GJx ∈ X K(σ) = true
⇔ σ(x) ∈ σ(X)
⇔ p(x◦)⊆ p( X )

⇔ p |=A ′
∨2

i=1〈x
◦ ⊑ X ,Ri〉

⇔ p |=A ′ Cond(P,x ∈ X)

Hypothesis. Assume that the statement holds for rectified MSO formulas F .

Step. For rectified MSO formulas of the form ¬F and ∧i∈I Fi, the proof is as in [HP09]. For for-
mulas of the form ∃xF , graphs G, and assignments σ , the statement follows from the semantics
of ∃xF , the induction hypothesis, q = σ{x/d}[D′P], and the definitions of |=A ′ and Cond:

GJ∃xFK(σ) = true
⇔ ∃d ∈ DG.GJFK(σ{x/d}) = true
⇔ ∃b ∈ C.∃q : Pb → G ∈ A

′.p = q◦(P→Pb)∧q |=A ′ Cond(Pb,F)
∨∃b,d,d′ ∈ C.∃q : Pbdd′ → G ∈ A

′.p = q◦(P→Pbdd′)∧q |=A ′ Cond(Pbdd′,F)
∨∃q : P+ x →G ∈ A ′.p = q◦(P → P+ x )∧q |=A ′ Cond(P+ x ,F)

⇔ p |=A ′
∨

b∈C∃(P→Pb,Cond(Pb,F))∨
∨

b,d,d′∈C∃(P→Pbdd′,Cond(Pbdd′,F))

∨
∨2

i=1〈∃(P→P+ X ,Cond(P+ X ,F),Ri〉
⇔ p |=A ′ Cond(P,∃xF)

This completes the inductive proof of the claim.

By the claim above and the definitions |=, |=A ′, and Cond, for all graphs G and all closed,
rectified MSO formulas F , we have G |= F ⇔∀σ : Var → DG.GJFK(σ) = true ⇔ /0 → G |=A ′

Cond(/0,F)⇔ G |=A ′ Cond(F), i.e., the HR
+ condition Cond(F) has the wanted property.

Example 7 The closure of the MSO formula

F(x1,x2) =∀X((∀y∀z(y ∈ X ∧edg(y,z) ⇒ z ∈ X)
︸ ︷︷ ︸

G1

∧∀y′(edg(x1,y
′) ⇒ y′ ∈ X)

︸ ︷︷ ︸

G2

)⇒ x2 ∈ X
︸ ︷︷ ︸

G3

)

is transformed into the HR+ condition

Cond(∀x1∀x2F(x1,x2))
= Cond(/0,∀x1∀x2F(x1,x2))
≡ ∀(

x1 x2
,Cond(/0,∀X(G1∧G2 ⇒ G3))))

≡ ∀(
x1 x2

X ,(Cond( X ,G1 ∧G2 ⇒ G3))
= ∀(

x1 x2
X ,(Cond( X ,G1)∧Cond( X ,G2) ⇒ Cond( X ,G3)))

≡ ∀(
x1 x2

X ,( ∀(x1 x2 X y z ,( y ⊑ X ∧∃(x1 x2 X y z ) ⇒ z ⊑ X )∧
∀(

x1 x2
X

y′
,∃(

x1 y′ x2
X

y′
) ⇒

y′
⊑ X ) ⇒ x2 ⊑ X ))

with X ::= /0 | X using the equivalence ∀(x(∀(y,c)) ≡∀(y◦x,c)) in [HP05].

A
′-satisfiable HR+ conditions can be transformed into B′-satisfiable HR+ conditions.

Lemma 1 (From A ′- to B′-satisfiability) There is a transformation Bsat such that, for every

HR+ condition c over /0 and every graph G, G |=A ′ c ⇐⇒ G |= Bsat(c).

13 / 18 Volume 30 (2010)



Graph conditions with variables

Construction For a HR condition c over /0, Bsat(c) = Shift(/0→ /0,c), and, for a HR+ condition
of the form x◦ ⊑ X , Bsat(x◦ ⊑ X ) = x◦ ⊑ X .

P

C

P′

C′

a a′(1)

b

b′

c

For a morphism b : P → P′, Shift(b, ) is inductively defined as follows:
Shift(b,true) = true.
Shift(b,∃(a,c)) =

∨

(a′,b′)∈F ∃(a
′,Shift(b′,c)) if F = {(a′,b′) | (a′,b′)

jointly epimorphic, (1) commutes} 6= /0 and false, otherwise.
Shift(b,x◦ ⊑ X ) = x◦ ⊑ X .

For Boolean formulas over HR+ conditions, Bsat( ) and Shift(b, ) are extended as usual.

Proof. For HR conditions c over /0, the statement follows directly from the corresponding state-

ment in [HP09]. For HR+ conditions of the form x◦ ⊑ X , we have p |=A ′ x
◦ ⊑ X ⇔ p |=

x◦ ⊑ X . Consequently, for all graphs G, we have G |=A ′ x
◦ ⊑ X )⇔ iG |=A ′ x

◦ ⊑ X ⇔ iG |=
x◦ ⊑ X ⇔ G |= x◦ ⊑ X where iG denotes the injective morphism /0 → G. This completes the
proof.

Example 8 The HR condition c =∃(/0→
1

+

2
) with HR system R : + ::=

1 2
|

1 2

+

meaning “There exists some simple, nonempty path” is transformed into the HR condition

Bsat(c) = ∃(/0 →
1

+

2
)∨∃(/0 →

1=2

+
) with the HR system R meaning “There exists some

simple, nonempty path or cycle”. The HR condition c = ∃(/0 → X x y ) is transformed into the
HR condition Bsat(c) =∃(/0 → X x y )∨∃(/0 → X x=y ).

The standard semantics for HR+ conditions is B′-satisfiability. By Theorem 3 and Lemma 1,

MSO formulas also can be transformed into B′-satisfiable HR+ conditions.

Corollary 1 (From MSO formulas to HR+ conditions) There is a transformation CondB′ from

MSO formulas to HR+ conditions, such that, for all MSO formulas F and all graphs G,

G |= F ⇐⇒ G |= CondB′(F).

Proof. Let CondB′ = Bsat◦Cond. By Theorem 3 and Lemma 1, we have G |= F ⇐⇒ G |=A ′

Cond(F) ⇐⇒ G |= CondB′(F).

Remark 7 For finite MSO formulas c, the corresponding HR+ conditions CondB′(c) are finite.

6 Related concepts

In [Hab92, DHK97], hypergraphs and hyperedge replacement are introduced. In [PH96], the

concept of graphs with variables is introduced using hyperedges as graph variables and hyper-

edge replacement as substitution mechanism. In [Hof01, HJG08], graph transformation — using

graph variables in rules without/with application conditions — are considered and, in [HM10],

an extension of hyperedge replacement grammars by context nodes and HR application condi-

tions is introduced. In [KMP05], graphs with ∗-labelled edges are considered; the ∗-labelled
edge stands for paths of arbitrary length. In [KK08], the authors describe regular expressions

Proc. GraMoT 2010 14 / 18



ECEASST

for forbidden paths which should not occur in any reachable graph. In [BKK03], the authors

introduce a monadic second-order logic over graphs expressively enough to characterize typical

graph properties. They propose to describe state predicates, i.e. the graph properties of inter-

est, by means of a monadic second-order logic on graphs, where quantification is allowed over

(sets of) edges. In [CE95], a logical characterization of the sets of hypergraphs defined by HR

grammars is given saying that a set of hypergraphs L can be generated by an HR grammar if

and only if the set of structures |L|2 is the image of a recognizable set of finite trees under a
MSO-definable transduction. The comparison diagram in [Cou90a] shows that the families of

HR- and MSO-definable sets of graphs are not comparable: In MSO, one cannot express whether

the number of elements of a set is even; in HR, this is expressible. In HR, one cannot express

that a graph is a square grid; in MSO, this is expressible. In [Pra04], it is sketched that graphs

with variables and substitution morphisms (consisting of a graph morphism and a substitution)

form an adhesive HLR category.

7 Conclusion

In this paper, we have investigated graph conditions with variables where the variables may be

replaced by graphs generated by some assigned hyperedge replacement system. We have shown

the following.

Graphs with variables. Graphs with variables and replacement morphisms form a category.

Distinguishing the class of all injective graph morphisms, we obtain a weak adhesive HLR cat-

egory 〈XGraphs,M〉. All results — known for weak adhesive HLR categories — hold for
rules with variables: Local Church-Rosser, Parallelism, Concurrency, Amalgamation, Embed-

ding/Extension, Restriction, and the Local Confluence Theorem.

HR and HR+ conditions. HR conditions are conditions in 〈XGraphs,M〉. HR+ conditions
extend HR conditions by subconditions of the form x◦ ⊑ X , a counterpart to MSO subformulas
of the form x ∈ X .

Validity for HR+ conditions. By the monotony property of HR systems the validity problem

for HR+ conditions is decidable, i.e., there is an algorithm for determining whether or not, given

a finite HR+ condition and a graph, the graph satisfies the condition.

Expressiveness of HR+ conditions. There is a transformation from MSO formulas to HR+

conditions, but HR+ conditions are more powerful: HR+ can express certain counting MSO

formulas. It remains the question whether or not there is a transformation from HR+ conditions

to SO formulas, and vice versa.

15 / 18 Volume 30 (2010)



Graph conditions with variables

FO formulas

MSO formulas

SO formulas

conditions

HR conditions

HR+ conditions

[HP09]

/
this paper

?

Expressiveness of OCL constraints. The concept of OCL constraints is well-known and there

are translations from restricted OCL constraints into first-order graph formulas [BKS02] and

graph constraints [EKT09], respectively. What about a translation of a larger class of OCL

constraints into HR constraints?

Acknowledgements: We thank the reviewers for their constructive criticism that helped to im-

prove our paper.

Bibliography

[Bau06] J. Bauer. Analysis of Communication Topologies by Partner Abstraction. PhD thesis,

Universität Saarbrücken, 2006.

[BKK03] P. Baldan, B. König, B. König. A Logic for Analyzing Abstractions of graph transfor-

mation systems. In Int. Static Analysis Symposium (SAS ’03). LNCS 2694, pp. 255–

272. 2003.

[BKS02] B. Beckert, U. Keller, P. H. Schmitt. Translating the Object Constraint Language into

First-order Predicate Logic. In Proc. VERIFY, Workshop at Federated Logic Confer-

ences (FLoC). 2002.

[CE95] B. Courcelle, J. Engelfriet. A Logical Characterization of the Sets of Hypergraphs De-

fined by Hyperedge Replacement Grammars. Mathematical Systems Theory 28:515–

552, 1995.

[Cou90a] B. Courcelle. Graph Rewriting: An Algebraic and Logical Approach. In Handbook of

Theoretical Computer Science. Volume B, pp. 193–242. Elsevier, 1990.

[Cou90b] B. Courcelle. The Monadic Second-Order Logic of Graphs I: Recognizable Sets of

Finite Graphs. Information and Computation 85:12–75, 1990.

[Cou97] B. Courcelle. The Expression of Graph Properties and Graph Transformations in

Monadic Second- Order Logic. In Handbook of Graph Grammars and Computing

by Graph Transformation. Volume 1, pp. 313–400. World Scientific, 1997.

Proc. GraMoT 2010 16 / 18



ECEASST

[DHK97] F. Drewes, A. Habel, H.-J. Kreowski. Hyperedge Replacement Graph Grammars. In

Handbook of Graph Grammars and Computing by Graph Transformation. Volume 1,

pp. 95–162. World Scientific, 1997.

[EEHP06] H. Ehrig, K. Ehrig, A. Habel, K.-H. Pennemann. Theory of Constraints and Appli-

cation Conditions: From Graphs to High-Level Structures. Fundamenta Informaticae

74(1):135–166, 2006.

[EEKR99] H. Ehrig, G. Engels, H.-J. Kreowski, G. Rozenberg (eds.). Handbook of Graph

Grammars and Computing by Graph Transformation. Volume 2: Applications, Lan-

guages and Tools. World Scientific, 1999.

[EH86] H. Ehrig, A. Habel. Graph Grammars with Application Conditions. In Rozenberg and

Salomaa (eds.), The Book of L. Pp. 87–100. Springer, 1986.

[Ehr79] H. Ehrig. Introduction to the Algebraic Theory of Graph Grammars. In Graph-

Grammars and Their Application to Computer Science and Biology. LNCS 73, pp. 1–

69. 1979.

[EKMR99] H. Ehrig, H.-J. Kreowski, U. Montanari, G. Rozenberg (eds.). Handbook of Graph

Grammars and Computing by Graph Transformation. Volume 3: Concurrency, Paral-

lelism, and Distribution. World Scientific, 1999.

[EKT09] K. Ehrig, J. M. Küster, G. Taentzer. Generating instance models from meta models.

Software and System Modeling 8(4):479–500, 2009.

[Eve79] S. Even. Graph Algorithms. Computer Science Press, Rockville, Maryland, 1979.

[Hab92] A. Habel. Hyperedge Replacement: Grammars and Languages. LNCS 643. Springer,

1992.

[Har69] F. Harary. Graph Theory. Addison-Wesley, Reading, Mass., 1969.

[HESV91] A. Hsu, F. Eskafi, S. Sachs, P. Varaiya. The Design of Platoon Maneuver Protocols

for IVHS. Technical report, Institute of Transportation Studies, University of Califor-

nia at Berkeley, 1991.

[HHT96] A. Habel, R. Heckel, G. Taentzer. Graph Grammars with Negative Application Con-

ditions. Fundamenta Informaticae 26:287–313, 1996.

[HJG08] B. Hoffmann, E. Jakumeit, R. Geiß. Graph Rewrite Rules with Structural Recursion.

In Mosbah and Habel (eds.), Int. Workshop on Graph Computational Models (GCM

2008). Pp. 5–16. 2008.

[HM10] B. Hoffmann, M. Minas. Defining Models - Meta Models versus Graph Grammars. In

Graph Transformation and Visual Modeling Techniques (GT-VMT 2010). Electronic

Communications of the EASST. 2010.

17 / 18 Volume 30 (2010)



Graph conditions with variables

[Hof01] B. Hoffmann. Shapely Hierarchical Graph Transformation. In Proc. IEEE Symposia

on Human-Centric Computing Languages and Environments. IEEE Computer Press,

pp. 30–37. 2001.

[HP05] A. Habel, K.-H. Pennemann. Nested Constraints and Application Conditions for

High-Level Structures. In Formal Methods in Software and System Modeling.

LNCS 3393, pp. 293–308. 2005.

[HP09] A. Habel, K.-H. Pennemann. Correctness of High-Level Transformation Systems Rel-

ative to Nested Conditions. Mathematical Structures in Computer Science 19:245–

296, 2009.

[HW95] R. Heckel, A. Wagner. Ensuring Consistency of Conditional Graph Grammars —

A Constructive Approach. In SEGRAGRA ’95. ENTCS 2, pp. 95–104. 1995.

[KK08] B. König, V. Kozioura. Augur 2—A New Version of a Tool for the Analysis of Graph

Transformation Systems. In Proc. Workshop on Graph Transformation and Visual

Modeling Techniques (GT- VMT ’06). ENTCS 211, pp. 201–210. 2008.

[KMP05] M. Koch, L. V. Mancini, F. Parisi-Presicce. Graph-based Specification of Access Con-

trol Policies. Journal of Computer and System Sciences 71:1–33, 2005.

[Pen09] K.-H. Pennemann. Development of Correct Graph Transformation Systems. PhD the-

sis, Universität Oldenburg, 2009.

[PH96] D. Plump, A. Habel. Graph Unification and Matching. In Graph Grammars and Their

Application to Computer Science. LNCS 1073, pp. 75–89. 1996.

[Pra04] U. Prange. Graphs with Variables as an Adhesive HLR Category. 2004. Private Com-

munication.

[Roz97] G. Rozenberg (ed.). Handbook of Graph Grammars and Computing by Graph Trans-

formation. Volume 1: Foundations. World Scientific, 1997.

[Tra50] B. A. Trakhtenbrot. The impossibility of an algorithm for the decision problem on

finite classes (In Russian). Doklady Akademii Nauk SSSR 70:569–572, 1950. English

translation in: Nine Papers on Logic and Quantum Electrodynamics, AMS Transl. Ser.

2, 23:1–5, 1963.

Proc. GraMoT 2010 18 / 18


	Introduction
	Graphs with variables
	HR and HR+ conditions
	Decidability of the validity problem
	Expressiveness of HR+ conditions
	Related concepts
	Conclusion