Graph Algebras for BigraphsWork funded by MIUR PRIN project ``SisteR'', prot. 20088HXMYN. Dedicated to the memory of Robin Milner (13 January 1934 -- 20 March 2010).


Electronic Communications of the EASST
Volume 29 (2010)

Proceedings of the
Ninth International Workshop on

Graph Transformation and
Visual Modeling Techniques

(GT-VMT 2010)

Graph Algebras for Bigraphs

Davide Grohmann, Marino Miculan

17 pages

Guest Editors: Jochen Küster, Emilio Tuosto
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

Graph Algebras for Bigraphs∗

Davide Grohmann1, Marino Miculan2

1 grohmann@dimi.uniud.it, 2 miculan@dimi.uniud.it
Department of Mathematics and Computer Science, University of Udine, Italy

Abstract: Binding bigraphs are a graphical formalism intended to be a meta-model
for mobile, concurrent and communicating systems. In this paper we present an
algebra of typed graph terms which correspond precisely to binding bigraphs over a
given signature. As particular cases, pure bigraphs and local bigraphs are described
by two sublanguages which can be given a simple syntactic characterization.

Moreover, we give a formal connection between these languages and Synchronized
Hyperedge Replacement algebras and the hierarchical graphs used in Architectural
Design Rewriting. This allows to transfer results and constructions among for-
malisms which have been developed independently, e.g., the systematic definition
of congruent bisimulations for SHR graphs via the IPO construction.

Keywords: Bigraphs, graph grammars, types.

1 Introduction

Bigraphical Reactive Systems (BRSs) [Mil01] have been proposed as a promising meta-model
for ubiquitous, mobile systems. The key feature of BRSs is that their states are bigraphs, semi-
structured data which can represent at once both the (physical, logical) location and the connec-
tions of the components of a system. The dynamics of the system is given by a set of rewrite
rules on this semi-structured data.

Bigraphs have been successfully used for representing many domain-specific calculi and mod-
els, from traditional programming languages, to process calculi for concurrency and mobility,
from context-aware systems to web-service orchestration languages—see e.g. [JM03, LM06,
BDE+06, GM07, BGH+08]. In fact, many variants of bigraphs have been proposed: the original
pure bigraphs have been later generalized into binding bigraphs, allowing also for name scoping;
other variants have been proposed, such as local bigraphs used for studying the λ -calculus.

In this paper, we propose a general typed language for binding bigraphs, which we recall in
Section 2. More precisely, in Section 3 we define an algebra of typed graph terms, so that well-
typed terms correspond to binding bigraphs, and congruence captures bigraphic equality; this
interpretation and corresponding properties are exposed in Section 4. Moreover, as we will show
in Section 5, the important subcategories of pure, local and prime bigraphs can be described by
suitable sublanguages which can be given a simple and effective syntactic characterization.

Finally, we show how this language can be tailored to formalisms introduced in literature (for
quite different purposes). In Section 6 we consider hypergraphs used in Synchronized Hyperedge
Rewriting [FHL+05] and the “designs” of Architectural Design Rewriting [BLMT07].
∗ Work funded by MIUR PRIN project “SisteR”, prot. 20088HXMYN.
Dedicated to the memory of Robin Milner (13 January 1934 – 20 March 2010).

1 / 17 Volume 29 (2010)

mailto:grohmann@dimi.uniud.it
mailto:miculan@dimi.uniud.it


Graph Algebras for Bigraphs

We have implemented the resulting algorithm in our BPL Tool, which we briefly describe in Section 6. We also
present an example of a bigraphical reactive system, an encoding of the polyadic π calculus, and show how it can be
used to simulate a simple model of a mobile phone system.

Bigraphical reactive systems are related to general graph transformation systems; Ehrig et al. [10] provide a recent
comprehensive overview of graph transformation systems. In particular, bigraph matching is related to the general
graph pattern matching (GPM) problem, so general GPM algorithms might also be applicable to bigraphs [11, 14, 20,
21]. As an alternative to implementing matching for bigraphs, one could try to formalize bigraphical reactive systems
as graph transformation systems and then use an existing implementation of graph transformation systems. Some
promising steps in this direction have been taken [19], but they have so far fallen short of capturing precisely all the
aspects of binding bigraphs. For a more detailed account of related work, in particular on relations between BRSs,
graph transformations, term rewriting and term graph rewriting, see the Thesis of Damgaard [8, Section 6].

The remainder of this paper is organized as follows. In Section 2 we give an informal presentation of bigraphical
reactive systems and in Section 3 we present our matching algorithm: we first recall the graph-based inductive char-
acterization, then we develop a term-based inductive characterization, which forms the basis for our implementation
of matching. In Section 4 we describe how our implementation deals with the remaining nondeterminism and in Sec-
tion 5 we discuss a couple of auxiliary technologies needed for the implementation of the term-based matching rules.
In Section 6 we finally describe the BPL Tool and present an example use of it. We conclude and discuss future work
in Section 7.

2. Bigraphs and Reactive Systems

In the following, we present bigraphs informally; for a formal definition, see the work by Jensen and Milner [13]
and Damgaard and Birkedal [9].

2.1. Concrete Bigraphs

A concrete binding bigraph G consists of a place graph GP and a link graph GL. The place graph is an ordered
list of trees indicating location, with roots r0, . . . , rn, nodes v0, . . . , vk, and a number of special leaves s0, . . . , sm called
sites, while the link graph is a general graph over the node set v0, . . . , vk extended with inner names x0, . . . , xl , and
equipped with hyper edges, indicating connectivity.

We usually illustrate the place graph by nesting nodes, as shown in the upper part of Figure 1 (ignore for now the
interfaces denoted by “ : · →· ”). A link is a hyper edge of the link graph, either an internal edge e or a name y. Links

Bigraph G : �3, [{},{},{x0, x2}], X� → �2, [{y0},{}],Y �

0

1

2

y0 y1 y2

x0 x2

x1

e2

v0

v1
v2 v3

e1

X ={x0, x1, x2}
Y ={y0, y1, y2}

Place graph GP : 3 → 2
roots:

sites:

r0

v0

v1

s0

v2

r1

v3

s2 s1

Link graph GL : X → Y
names:

inner names:

y0 y1 y2

v0

v1

v2

v3

x0 x2 x1

e1

e2

Fig. 1. Example bigraph illustrated by nesting and as place and link graph.

2

Figure 1: A binding bigraph (picture taken from [BDGM07]).

These results are useful for several reasons. First, the typed algebra we propose can be used
as a language for binding, pure, local and prime bigraphs, alternative to the bigraph algebra
[JM03]. Moreover, we confirm once more that bigraphs are a quite expressive general framework
of ubiquitous systems. These connections pave the way for transferring results and constructions
from bigraphs to the SHR and ADR frameworks, and vice versa, as suggested in Section 7.

2 Binding Bigraphs

In this section we recall Milner’s binding bigraphs [JM03, JM04]. Intuitively, a binding bigraph
represents an open system, so it has an inner and an outer interface to “interact” with subsystems
and the surrounding environment (Figure 1). The width of the outer interface describes the roots,
that is, the various locations containing the system components; the width of the inner interface
describes the sites, that is, the holes where other bigraphs can be inserted. On the other hand, the
names in the interfaces describe free links, that is end points where links from the outside world
can be pasted, creating new links among nodes. In particular, we consider binding bigraphs with
(possibly) multiply localized names, as in [Mil04] and slightly generalizing [JM03, JM04].

More formally, let K be a binding signature of controls (i.e., node types), and ar : K →
N×N be the arity function. The arity pair (h, k) (written h → k) consists of the binding arity h
and the free arity k, indexing respectively the binding and the free ports of a control.

Definition 1 (Interfaces) An interface is a pair 〈m, X〉 where m is a finite ordinal (called width),
X is a finite set of names. A binding interface is a triple 〈m, loc, X〉, where 〈m, X〉 is an interface
and loc ⊆ m×X is a locality map associating a subset of the names in X with sites in m. If
(s, x) ∈ loc then x is located at s, or local to s; x is global if, ∀s, (s, x) /∈ loc.

Proc. GT-VMT 2010 2 / 17



ECEASST

Sometime, we shall represent the locality map as a vector ~X = (X0, . . . , Xm−1) of subsets, where
Xs is the set of names local to s; thus X \~X = X \(X0 ∪···∪Xm−1) are the global names. We
call an interface local (resp. global) if all its names are local (resp. global). We denote by ] the
union of already disjoint sets, i.e., S]T , S∪T if S∩T = /0, otherwise it is undefined.

Definition 2 (Pure and binding bigraphs) A (pure) bigraph G : 〈m, X〉→〈n,Y〉 is composed by
a place graph GP and a link graph GL describing node nesting and (hyper-)links among nodes:

G = (V, E, ctrl, GP, GL) : 〈m, X〉→〈n,Y〉 (pure bigraph)
GP = (V, ctrl, prnt) : m → n (place graph)
GL = (V, E, ctrl, link) : X →Y (link graph)

where V, E are the sets of nodes and edges respectively; ctrl : V → K is the control map, which
assigns a control to each node; prnt : m]V → V ]n is the (acyclic) parent map (often written
also as <); link : X ]P → E ]B]Y is the link map, where P = ∑v∈V π1(ar(ctrl(v))) is the set
of ports and B = ∑v∈V π2(ar(ctrl(v))) is the set of bindings (associated to all nodes). A link
l ∈ X ]P is bound if link(l) ∈ B; it is free if link(l) ∈Y ]E.

A binding bigraph G : 〈m, loc, X〉→〈n, loc′,Y〉 is a (pure) bigraph Gu : 〈m, X〉→〈n,Y〉 satis-
fying the following locality conditions:

1. if a link is bound, then the names and ports linked to it must lie within the node that binds it;

2. if a link is free, with outer name x, then x must be located in every region that contains any
inner name or port of the link.

Definition 3 (Binding bigraph category) The category of binding bigraphs over a signature K
(written Bbg(K )) has local interfaces as objects, and binding bigraphs as morphisms.

Given two binding bigraphs G : 〈m, loc, X〉→ 〈n, loc′,Y〉, H : 〈n, loc′,Y〉→ 〈k, loc′′, Z〉, the
composition H◦G : 〈m, loc, X〉→〈k, loc′′, Z〉 is defined by composing their place and link graphs,
whenever they have disjoint node and edge sets:

1. the composition of GP : m → n and H P : n → k is defined as
H P ◦GP = (VG ]VH , ctrlG ]ctrlH , (idVG ] prntH )◦(prntG ]idVH )) : n → k;

2. the composition of GL : X →Y and H L : Y → Z is defined as
H L ◦GL = (VG ]VH , EG ]EH , ctrlG ]ctrlH , (idEG ]linkH )◦(linkG ]idPH )) : X → Z.

Definition 4 (Pure, local and prime bigraphs) The category of pure bigraphs (Big) is the full
subcategory of Bbg whose objects are of the form 〈n, ( /0), X〉 (often shorten as 〈n, X〉).

The category of local bigraphs (Lbg) is the full subcategory of binding bigraphs whose objects
are of the form 〈n, (~X ),⋃~X〉 (often shorten as (~X )).

The category of prime bigraphs (Pbg) is the full subcategory of local bigraphs whose objects
are of the form 〈n, (~X ),⋃~X〉, with n ∈{0, 1}, (often shorten as before: (~X )).

Intuitively, in pure bigraphs all names are global, whilst in local bigraphs all names are local,
finally prime bigraphs are all the local bigraphs with one root, and one or zero holes.

3 / 17 Volume 29 (2010)



Graph Algebras for Bigraphs

An important operation about (bi)graphs, is the tensor product. Intuitively, the tensor prod-
uct puts “side by side” two bigraphs, given G : 〈m, (~X ), X〉→〈n, (~Y ),Y〉 and H : 〈m′, (~X′), X′〉→
〈n′, (~Y ′),Y ′〉, their tensor product is a bigraph G⊗H : 〈m+m′, (~X~X′), X∪X′〉→〈n+n′, (~Y~Y ′),Y ∪
Y ′〉 defined when global names in X , X′ and Y,Y ′ are disjoint. Two useful variants of tensor prod-
uct can be defined using tensor and composition: the parallel product ‖, which merges shared
names between two bigraphs, and the prime product |, that also merges all roots in a single one.
As shown in [Mil04, DB06], all bigraphs can be constructed by composition and tensor product
from a set of elementary bigraphs:

• 1 : 〈0, ( /0), /0〉→〈1, ( /0), /0〉 is the barren (i.e., empty) root;
• mergen : 〈n, ( /0), /0〉→〈1, ( /0), /0〉 merges n roots into a single one;
• γm,n,(~X ,~Y ) : 〈m + n, (~X~Y ), (

⋃
~X )∪(⋃~Y )〉→〈m + n, (~Y ~X ), (⋃~X )∪(⋃~Y )〉 permutes the first m

roots having local names in ~X with the following n roots with local names in ~Y .
• /x : 〈0, ( /0),{x}〉→〈0, ( /0), /0〉 is a closure, that is it maps x to an edge;
• y/X : 〈0, ( /0), X〉→〈0, ( /0),{y}〉 substitutes the names in X with y, i.e., it maps the whole set

X to y; as a shortcuts, we write ~y/~X to mean y0/X0 ⊗. . .⊗yn−1/Xn−1;
• pX q : 〈1, (X ), X〉→〈1, ( /0), X〉 means that names in X are switched from local to global
• conversely, (X ) : 〈1, ( /0), X〉→〈1, (X ), X〉 localizes the global names of X .
• Finally, K

~x(~X ) : 〈1, (X ), /0〉→〈1, ( /0),~x〉 is a control which may contain other graphs, and it has
free ports linked to the name in ~x, whilst the names ~X are connected to its binding ports.

We use the convention that local names are enclosed in parenthesises.
Bigraphs can be given always in discrete normal form: the idea of this normal form is to

separate wirings (i.e., linkings) from discrete bigraphs (i.e., nesting of nodes). The following is
an easy generalization of [DB06, Theorem 1] to the case of bigraphs with multiply located names.

Theorem 1 (Discrete Normal Form (DNF)) 1. Any binding bigraph
G : I →〈n,~YB, (

⋃
~YB)]YF〉 can be expressed as

G =
(⊗

i<n(~yi)/(~Xi)⊗
⊗

i<|YF| wi/Wi ⊗
⊗

i<|Z|(/zi ◦zi/Zi)
)
◦D

where D : I →〈m,~X , (⋃~X )]W ]Z〉 is a name discrete.
2. Any name discrete D : I →〈m,~X , (⋃~X )]W ]Z〉 can be expressed as

D = α ⊗((P0 ⊗. . .⊗Pn−1)◦π)
where α is a renaming, and π a permutation.

3. Any name-discrete prime P : J →〈1, (UB),U〉 can be expressed as
(UB)◦(mergen+k ⊗idU )◦(pα0q⊗. . .⊗pαn−1q⊗M0 ⊗. . .⊗Mk−1)◦π

where every Mi : Ji →〈1, ( /0),U Mi 〉 is a free discrete molecule, and for renamings αi : Vi →UCi ,
we have U = (

⊎
i∈n U

C
i )]

⊎
i∈k U

M
i .

4. Any free discrete molecule M : K →〈1, ( /0),~x]V〉 can be expressed as M = (K
~x(~S) ⊗ idV )◦P

where P : H →〈1, (⊎~S), (⊎~S)]V is a name discrete.
Proc. GT-VMT 2010 4 / 17



ECEASST

(a) l

x0 x1 xn. . .
. . .

(b) L
A

y0
y1

ym

. . .

x0 x1 xn. . .

. . . . . .

. . .

Figure 2: Example of an atomic label (a) and a non-atomic one (b).

3 Graph Grammar for Bigraphs

In this section we introduce a language for binding bigraphs. It is parametric over a ranked
alphabet of labels L = (La, Ln, exit : La ∪Ln → N, in : Ln → N), where La are the atomic
labels, ranged over by l, and Ln are the non-atomic labels, ranged over by L. Each label is given
an exit-rank, exit(l)∈ N, enumerating the “exiting tentacles”. Non-atomic labels have an in-rank
in(L)∈N, enumerating the label’s “incoming tentacles”. We often denote by L the set La∪Ln.

One may think of a node with an atomic label l as an hyperedge with exit(l) tentacles, as in
Figure 2(a). A node labelled with L has exit(L) tentacles, and may contain a subsystem whose
exiting tentacles are either linked to the in(L) ports of the node, or go “outside” the node, see
Figure 2(b). More formally, the language of graphs is as follows.

Definition 5 (Agent graphs) Let N be an infinite set of names, V be an infinite set of variables,
and L be a ranked alphabet of labels. An agent-graph A is a term generated as follows:

A ::= ε | 0 | l(~x) | L(~x)[A\~y] | X | A|A | A ‖ A | ν z.A | A[w 7→ z] | A |• z | A |• z
where ~x,~y ⊆N ∗; l ∈La, L ∈Ln with exit(l) = exit(L) = |~x|, in(L) = |~y|; X ∈V ; and w, z ∈N .
Moreover, in a term A, each X is used at most once.

Intuitively, ε represents the absence of any system, that is, no agents at all, while 0 represents
an empty agent (i.e., an agent with no nodes). We denote by l(~x) atomic hyperedges whose
tentacles are linked to the names in ~x, whilst by L(~x)[A\~y] non-atomic hyperedges having exiting
tentacles linked to the names in ~x, containing a subgraph A whose names ~y are linked on the edge
itself. Graph variables X are needed for representing open systems, i.e., graphs with holes.

Two agent graphs A, B can be composed in parallel in two different ways: A | B “merges” two
graphs into a unique one (i.e., in the same location), while A ‖ B puts the two systems side by
side, i.e., they keep living in different locations.

As usual, ν y.A limits the scope of y to A, while A[w 7→ z] is the explicit substitution of name w
with z. Notice that the agent-graph A[w 7→ z] exhibits the name z also when w does not appear in
A; in this case, the operator [w 7→ z] “creates” unused (or idle) names.

Finally, A |• z localizes z to (the location of) A. This means that z can only be accessed by/linked
to nodes lying in the location of A, that is, they must be inside or in parallel (|) to A. Dually, A |• z
globalizes z, allowing a localized name to be used also by nodes in different locations.

From the above intuition, it is clear that not all terms generated by this grammar are meaning-
ful. For instance, what is the meaning of A|B or A |• z when A is a system with more than one
location? In order to rule out meaningless terms, we introduce a typing system for agent graphs.

5 / 17 Volume 29 (2010)



Graph Algebras for Bigraphs

〈〉; τ ` ε : (〈〉, τ) 〈〉; τ ` 0 : ( /0, τ) 〈〉; τ ` l(~x) : ( /0,~x∪τ)
Γ ; τ ` A : (σ ∪~y, ρ) ~y∩σ = /0

Γ ; τ ` L(~x)[A\~y] : (σ , ρ ∪~x)
Γ ; τ ` A : (σ , ρ) Γ′ ; τ′ ` A′ : (σ ′, ρ′) τ ∩τ′ = /0

Γ, Γ′ ; τ ∪τ′ ` A | A′ : (σ ∪σ ′, ρ ∪ρ′)
Γ ; τ ` A : (~σ , ρ) Γ′ ; τ′ ` A′ : (~σ ′, ρ′) τ ∩τ′ = /0

Γ, Γ′ ; τ ∪τ′ ` A ‖ A′ : (~σ~σ ′, ρ ∪ρ′)

X : σ ; τ ` X : (σ , τ)
Γ ; τ ` A : (~σ , ρ)

Γ ; τ ` ν x.A : (~σ \{x}, ρ \{x})
Γ ; τ ` A : (~σ , ρ) π permutation

π(Γ) ; τ ` A : (~σ , ρ)
Γ ; τ ` A : (~σ , ρ) x ∈~σ

Γ ; τ ` A[x 7→ y] : (~σ{y/x}, ρ)
Γ ; τ ` A : (~σ , ρ) x /∈~σ

Γ ; τ ` A[x 7→ y] : (~σ , (ρ \{x})∪{y})
Γ ; τ ` A : (σ , ρ ∪{x}) x /∈ ρ

Γ ; τ ` A |• x : (σ ∪{x}, ρ)
Γ ; τ ` A : (~σ , ρ) x ∈~σ

Γ ; τ ` A |• x : (~σ \{x}, ρ ∪{x})

Figure 3: Type inference rules for agent-graphs.

Definition 6 (Type system for agent graphs) Simple types τ, σ , ρ are finite sets of names.
An agent-type (~τ, τ) is a pair formed by a list ~τ = τ0 . . . τn−1 of simple types (where 〈〉 is the

empty list), and a simple-type τ , such that τ ∩(τ0 ∪. . .∪τn−1) = /0.
An environment is a pair Γ ; τ formed by a list of typed variables (Γ = ~X :~τ = X0 : τ0, . . . , Xn−1 :

τn−1) and a simple-type (τ ), such that (~τ, τ) is an agent-type.
A typing judgement is of the form Γ ; τ ` A : (~σ , ρ), whose inference rules are in Figure 3.

Agent-types (~τ, τ) = (τ0 . . . τn−1, τ) describe both the locations of a graph, and the names that
the graph exposes to the environment. Names in τ are “global”, and can be used from every
location; instead, names in τi can be used only inside the i-th location of the system.

We are interested in open systems, that is systems with “holes”. An environment Γ ; τ = X0 :
τ0, . . . , Xn−1 : τn−1 ; τ declares the “inner interface” of an agent: the names of the variables (Xi for
i ∈ n), with their sets of local names (τi are the names local to Xi), and the set of incoming global
names (τ ), i.e., names that can be used from within any variable.
Notation. List concatenation is denoted simply by juxtaposition. We extend the operators ∈,
∪ and \ over set lists as follows: x ∈~τ iff there exists τ̄ ∈~τ such that x ∈ τ̄ ; let S be a set,
then τ0 . . . τn−1∪S , (τ0∪S) . . . (τn−1∪S) and τ0 . . . τn−1\S , (τ0\S) . . . (τn−1\S). Γ1, Γ2 is the
concatenation of Γ1 and Γ2, defined when dom(Γ1)∩dom(Γ2) = /0. We introduce some useful
shortcuts: ν~x.A = ν x|~x−1|. . . . ν x0.A; A[~x 7→~y] = A[x0 7→ y0] . . . [xn−1 7→ yn−1] when |~x| = |~y| = n;
A[X 7→ x] = A[x0 7→ x] . . . [x|X| 7→ x] if X 6= /0, A[ /0 7→ x] = A[z 7→ x] for some z fresh (i.e., z is not
used by A); finally A[~X 7→~x] = A[X0 7→ x0] . . . [Xn−1 7→ xn−1] when |~X| = |~x| = n.

Some intuitive explanation of the typing rules may be useful. Empty agents have only global
names, as defined by the environment. Notice that 0 is the null process, which is an agent, while
ε is no agent at all. An atomic hyperedge whose exit-tentacles are linked to the names ~x exposes
those (global) names to a context, plus the ones added by the environment. As before, a non-
atomic hyperedge shows names ~x that are linked to its exit-tentacles, plus the global ones defined
in the environment. The difference is that it contains a graph term having ~y local names, that are
linked to the hyperedge’s input tentacles, and hence they are not visible from the context.

Proc. GT-VMT 2010 6 / 17



ECEASST

lX
x

z

x w

u
l′ Y

x

L

y

y

Y : {x}, X : {x, z};{y}` ν u.((l(x, u) | X ) |• z[z 7→ w] ‖ L(y, u)[(Y | l′(w, x))\x] |• w) : ({w}{w},{x, y})
Figure 4: An example of an agent-graph.

The names exposed by a composition (|) of two subgraphs are the union of the names exposed
by the two subgraphs. The rule for ‖ is quite similar, but in this case the two graphs keep their
different locations, and hence the names can be treated in a different way, so global names are the
union of agents’ global names, whilst local names remains unchanged, i.e, the two lists of local
names are concatenated. If a variable has type σ in an environment Γ, then it exposes σ local
names and the global names τ defined by the environment. The restriction deletes a name from
the set of global or local exposed names. The next rule describes the possibility to reorder the
variables in the environment; it will be important in the definition of a category for agent-graphs.

For the substitution A[w 7→ z] there are two cases: (1) if w is localized, it will be substituted
by z; (2) if it is global the substitution (possibly) deletes w and adds z to the set of global names.
Notice that if w, z are not used in A, then it effectively adds the name z to its interface.

An example of an agent-graph is given in Figure 4, where white nodes are closed (that is,
nodes not accessible from the context); the other are the external nodes (which can be visible by
a context): the grey nodes are global and the black ones are local.

Now, we can prove the following properties on our language.

Proposition 1 If Γ ; τ ` A : (~σ , τ) and Γ ; τ ` A : (~σ ′, τ′) then ~σ = ~σ ′ and τ = τ′.

Lemma 1 (substitution lemma) The following rule is admissible.

Γi ; τi ` Ai : (σi, ρi) 0 ≤ i < n ∀i 6= j. τi ∩τ j = /0 X0 : σ0, . . . , Xn−1 : σn−1 ;
⋃n−1

i=0 ρi ` A : (~η, ζ )
Γ0, . . . , Γn−1 ;

⋃n−1
i=0 τi ` A{A0/X0, . . . , An−1/Xn−1} : (~η ; ζ )

As happens often with graph grammars, the same system may be denoted by many terms.
Therefore, it is convenient to introduce a structural congruence over terms, capturing graph iso-
morphisms up-to free nodes. Congruence judgments are of the form Γ ; τ ` A ≡ B, for A, B terms
of the language. This turns our language into a graph algebra, whose axioms are in Appendix A.

Proposition 2 Let Γ ; τ ` A ≡ A′, Γ ; τ ` A : (~σ , ρ) if and only if Γ ; τ ` A′ : (~σ , ρ).

4 Interpreting Agent Graphs as Binding Bigraphs

In this section we give an interpretation of agent graphs as binding bigraphs, showing that the
language is sound and complete, and that the axiomatization captures bigraphical equivalence.
In order to simplify the interpretations, we first introduce a category for agent-graphs.

7 / 17 Volume 29 (2010)



Graph Algebras for Bigraphs

Definition 7 The category A(L ) of agent-graphs, over a ranked alphabet L , has graph types
(~σ , ρ) as objects, and judgments on agent-graphs as morphisms, that is, if X0 : η0, . . . , Xn−1 :
ηn−1 ; τ ` A : (~σ , ρ) then (X0, . . . , Xn−1, A) : (~η, τ) → (~σ , ρ) is a morphism. Composition is
defined in virtue of Lemma 1.

Proposition 3 (A(L ),‖,〈〉; /0 ` ε : (〈〉, /0)) is a strict symmetric monoidal category.

4.1 Interpretation of agent-graphs as binding bigraphs

Let L be a ranked alphabet of labels; we define a functor from the agent-graph category A(L )
to the binding bigraph category BBg(KL ), for a suitable bigraphical signature KL . The idea
is to map agent-graph hyperedges into nodes, and nodes (or names) into links (i.e., outer names
and edges); hence, the bigraphical signature corresponds to the alphabet of labels. Formally:

KL , {l : 0 → exit(l) | l ∈ La}∪{L : in(L) → exit(L) | L ∈ Ln}.
We can now define the functor J−K : A(L ) → BBg(KL ) by induction on the typing judgments:

Objects: J(~σ , τ)K = 〈|~σ|,~σ , τ〉
Morphisms: J〈〉; τ ` ε : (〈〉, τ)K = idτ

J〈〉; τ ` 0 : ( /0, τ)K = 1 ‖ idτ
J〈〉; τ ` l(~x) : ( /0,~x∪τ)K = l~x ‖ idτ

JΓ ; τ ` L(~x)[A\~y] : (σ , ρ ∪~x)K = L~x,(~y)◦JΓ ; τ ` A : (σ ∪~y, ρ)K
JX : σ ; τ ` X : (σ , τ)K = id(σ ) ‖ idτ

JΓ, Γ′ ; τ ∪τ′ ` A | A′ : (σ ∪σ ′, ρ ∪ρ′)K = JΓ ; τ ` A : (σ , ρ)K | JΓ′ ; τ′ ` A′ : (σ ′, ρ′)K
JΓ, Γ′ ; τ ∪τ′ ` A ‖ A′ : (~σ~σ ′, ρ ∪ρ′)K = JΓ ; τ ` A : (~σ , ρ)K ‖ JΓ′ ; τ′ ` A′ : (~σ ′, ρ′)K

JΓ ; τ ` ν x.A : (~σ \{x}, ρ)K = /(x)◦JΓ ; τ ` A : (~σ , ρ)K (if x ∈~σ )
JΓ ; τ ` ν x.A : (~σ , ρ \{x})K = /x◦(JΓ ; τ ` A : (~σ , ρ)K ‖{x}) (if x /∈~σ )

JΓ ; τ ` A[x 7→ y] : (~σ{y/x}, ρ)K = (y)/(x)◦JΓ ; τ ` A : (~σ , ρ)K (if x ∈~σ )
JΓ ; τ ` A[x 7→ y] : (~σ , (ρ \{x})∪{y})K = y/x◦(JΓ ; τ ` A : (~σ , ρ)K ‖{x}) (if x /∈~σ )

JΓ ; τ ` A |• x : (σ ∪{x}, ρ)K = (x)◦JΓ ; τ ` A : (σ , ρ ∪{x})K
JΓ ; τ ` A |• x : (~σ \{x}, ρ ∪{x})K = pxq◦JΓ ; τ ` A : (~σ , ρ)K (if x ∈~σ )

Jπ(Γ) ; τ ` A : (~σ , ρ)K = JΓ ; τ ` A : (~σ , ρ)K◦π .
Basically, each variable of type σ is encoded as a site having σ local names; therefore, variable
permutation is site permutation. Restricted names are represented by bigraph edges, not accessi-
ble from the context. The graph 0 is represented by the empty root 1. An example is in Figure 5.

Now we can prove that J−K respects the structure of the two categories:
Proposition 4 J−K : (A(L ),‖,〈〉; /0 ` ε : (〈〉, /0)) → (Bbg(K ),‖, id(0, /0, /0)) is strict monoidal.

Moreover, the axiomatization of the graph algebra given in Appendix A is sound and complete
with respect to bigraph equivalence.

Proposition 5 Let A, A′ be two agent-graphs; then, for every environment Γ ; τ : Γ ; τ ` A ≡ A′
if and only if JΓ ; τ ` A : (~σ , ρ)K = JΓ ; τ ` A′ : (~σ , ρ)K.

Proc. GT-VMT 2010 8 / 17



ECEASST

Y : {x}, X : {x, z};{y}` ν u.((l(x, u) | X ) |• z[z 7→ w] ‖ L(y, u)[(Y | l′(w, x))\x] |• w) : ({w}{w},{x, y})

1
z x

l

0
w x

0
x

l′L

1
w

y

y

G :〈2, ({z, x},{x}),{z, x, y}〉→
〈2, ({w},{w}),{x, y, w}〉

J−K

Figure 5: An example of encoding an agent-graph into a binding bigraph.

4.2 Representing binding bigraphs with agent-graphs

In this section we show that our language is expressive enough to cover all binding bigraphs, over
a given signature K . To this end, we define a translation from binding bigraphs to agent-graphs
of a language whose ranked labels are defined by means of the bigraphical signature.

LK , ({k | k : 0 → n ∈ K , atomic},{k | k : m → n ∈ K , non atomic}, exit, in)
exit(k) , n for k : m → n ∈ K in(k) , m for k : m → n ∈ K non atomic

The representation function L−M maps objects of the category Bbg(K ) to agent-types, as
L〈n, (~X ), (⋃~X )] X〉M , (~X , X ). In order to simplify the translation of bigraphs, in virtue of
Theorem 1 we can suppose w.l.o.g. that all binding bigraphs are in discrete normal form. Let
G : 〈m,~XB, (

⋃
~XB)]XF〉→〈n,~YB, (

⋃
~YB)]YF〉, be in discrete normal form as follows

G =
(⊗

i<n(~yi)/(~Xi)⊗
⊗

i<|YF| wi/Wi ⊗
⊗

i<|Z|(/zi ◦zi/Zi)
)
◦(~a/~b⊗((P0⊗. . .⊗Pn−1)◦π))

then, for ~Q = Q0, . . . , Qm−1 a list of m variables, we define

LGM~Q = ν z|Z|−1. . . . ν z0.
(
(Lp0M~Q ‖ . . . ‖ Lpn−1M~Q)

[~b 7→~a][W0 7→ w0] . . . [W|YF|−1 7→ w|YF|−1][~X0 7→~y0] . . . [~Xn−1 7→~yn−1]
)

where p0 ⊗. . .⊗ pn−1 = (P0 ⊗. . .⊗Pn−1)◦π ◦(v0(X0)⊗. . .⊗v
m−1
(Xm−1)

).

Given p = (UB)◦(mergeh+k ⊗idU )◦(p~a0/~b0q⊗. . .⊗p~ah−1/~bh−1q⊗m0 ⊗. . .⊗mk−1), then
LpM~Q =

(
LK0

~x0,(~S0)
◦ p0M~Q | . . . | LK

ki−1
~xki−1 ,(~Ski−1 )

◦ pki−1 M~Q |

Lv j0(X j0 )
M~Q[

~b0 7→~a0] |• ~a0 | . . . | Lv
jhi−1
(X jhi−1

)M~Q[
~bhi−1 7→~ahi−1 ] |• ~ahi−1

)
|• UB

Lvi(Xi)M~Q = Qi
LK~x,( /0)◦1M~Q = K(~x) where K atomic
LK

~x,(~S)◦ pM~Q = K(~x)[LpM~Q[~S 7→~s]\~s] where K non-atomic, and ~s fresh
where the nodes v0, . . . , vm−1 have special controls not present in K , and they are used only
to simplify the translation. In practice, these special nodes give a “name” to each hole of the
bigraphs, i.e., the node vi represents the i-hole of the bigraphs. Notice that, the hole sequence
may not follow necessarily the numeration of holes, as shown in the bigraph in Figure 6.

The following result, states the expressivity of our language.

9 / 17 Volume 29 (2010)



Graph Algebras for Bigraphs

1
z x

l

0
w x

0
x

l′L

1
w

y

y

G :〈2, ({z, x},{x}),{z, x, y}〉→
〈2, ({w},{w}),{x, y, w}〉

0

v1

x
1

v0

z x

y

L−M

Q0 : {x}, Q1 : {x, z};{y}`
ν z.((((l(x, z) | Q1) ‖ ε) |• z ‖ (L(y, z)[(Q0 | l′(w, x))[x 7→ s]\s] ‖ ε) |• w)[z 7→ w]) : ({w}{w},{x, y})

Figure 6: An example of encoding a binding bigraph into an agent-graph.

Proposition 6 Let G : 〈m,~XB, (
⋃

~XB)]XF〉→〈n,~YB, (
⋃

~YB)]YF〉 be a binding bigraph. Then,
LGM~Q is an agent-graph s.t.

~Q : ~XB; XF ` LGM~Q : (~YB,YF ), and J~Q : ~XB; XF ` LGM~Q : (~YB,YF )K = G.

We can also establish nice connections between the axiomatizations of the two categories.

Proposition 7 Let G, G′ : 〈m,~XB, (
⋃

~XB)]XF〉→〈n,~YB, (
⋃

~YB)]YF〉 be two binding bigraphs
over a given signature. Then, G = G′ if and only if ~Q : ~XB; XF ` LGM~Q ≡ LG′M~Q.

Proposition 8 For Γ ; τ ` A : (~σ , ρ) a typing judgment: Γ ; τ ` LJΓ ; τ ` A : (~σ , ρ)KMdom(Γ) ≡ A.

These results induces a normal form for agent-graphs inspired to the discrete normal form of
binding bigraphs. This normal form tries to separate the notions of nesting and linking:

A ≡ ν~z.
(
(Ā0 ‖ . . . ‖ Ān−1)[~X 7→~x]

)
Ā ≡

(
L0(~x0)[Ā

0[~Y0 7→~y0]\~y0] | . . . | Lm−1(~xm−1)[Ām−1[~Ym−1 7→~ym−1]\~ym−1] |
l0(~z0) | . . . | lk−1(~zk−1) | X0[~Z0 7→~z0] |• ~z0 | ··· | Xh−1[~Zh−1 7→~zh−1] |•~zh−1

)
|• W .

Proposition 9 Every agent-graph is structural equivalent to an agent-graph in normal form.

Finally, notice that the mapping L−M : Bbg(K ) → A(LK ) is not a functor, because the com-
position of wirings in binding bigraphs is not respected by the graph composition defined in
virtue of Lemma 1. Therefore, Bbg(K ) and A(LK ) are not isomorphic. However, as we will
see next, composition is respected in the important subcategories of pure and local bigraphs.

5 Characterizing pure, local and prime bigraphs

In this section we show that pure, local and prime bigraphs can be captured by simple syntactic
conditions on the language and types of the typed language presented in Section 3. Indeed, these

Proc. GT-VMT 2010 10 / 17



ECEASST

(A,‖,〈〉; /0 ` ε : (〈〉, /0))(P,‖,〈〉; /0 ` ε : /0) (L,‖,〈〉` ε : 〈〉) (H,|,` ε : /0)

(Bbg,‖, id〈0, /0, /0〉)(Big,‖, id〈0, /0〉) (Lbg,‖, id()) (Pbg,|, id /0)

J−K L−MJ−K L−M J−K L−M J−K L−M
Π

U

Figure 7: Relations among the categories under investigation.

〈〉; τ ` ε : (0, τ) 〈〉; τ ` 0 : (1, τ) 〈〉; τ ` l(~x) : (1,~x∪τ)
Γ ; τ ` A : (1, ρ)

Γ ; τ ` L(~x)[A\〈〉] : (1, ρ ∪~x) X ; τ ` X : (1, τ)
Γ ; τ ` A : (1, ρ) Γ′ ; τ′ ` A′ : (1, ρ′) τ ∩τ′ = /0

Γ, Γ′ ; τ ∪τ′ ` A | A′ : (1, ρ ∪ρ′)
Γ ; τ ` A : (n, ρ) Γ′ ; τ′ ` A′ : (n′, ρ′) τ ∩τ′ = /0

Γ, Γ′ ; τ ∪τ′ ` A ‖ A′ : (n + n′, ρ ∪ρ′)
Γ ; τ ` A : (n, ρ)

Γ ; τ ` ν x.A : (n, ρ \{x})
Γ ; τ ` A : (n, ρ) π permutation

π(Γ) ; τ ` A : (n, ρ)
Γ ; τ ` A : (n, ρ)

Γ ; τ ` A[x 7→ y] : (n, (ρ \{x})∪{y})

Figure 8: Typing rules for restricted agent-graphs where all names are global.

subcategories are covered by the same sublanguage, obtained by removing |• and |•:
A ::= ε | 0 | l(~x) | L(~x)[A\~y] | X | A|A | A ‖ A | ν z.A | A[w 7→ z] . (1)

Despite we use the same (sub)language, and essentially the same typing rules of Figure 3, we are
able to describe both pure and local bigraphs, just by restricting the form of types and typing en-
vironment. Figure 7 summarizes the correspondences among the categories under investigation.

5.1 Pure bigraphs

In pure bigraphs all names are global, hence, variables and agents cannot have localized names.
Therefore, a typing system for pure bigraphs is derivable from the system in Figure 3 by simply
restricting to types of the form (~/0, τ), while the variables in the environment can have only /0 as
type. The only function of ~/0 is to count the locations of the system. Therefore, taking n = |~/0|,
a typing judgement is simply of the form Γ ; τ ` A : (n, ρ) where A is a term as per (1). We can
hence define global type (n, ρ) is a pair where n ∈ N and ρ is a simple types; an environment
Γ ; τ is a list of variables Γ = ~X = X0, . . . , Xn−1, together with a simple-type τ .

Notice that for L non-atomic, it must be in(L) = 0, because there are no local names which can
be linked to an in-tentacle. This is enforced by the typing system, which is given Figure 8. These
rules are essentially the same of Figure 3, just with the restricted form of types and environments.

Definition 8 The category P(L ) of agent-graphs, over a ranked alphabet L , has types (m, ρ)
as objects, and judgments as morphisms, i.e., if X0, . . . , Xn−1 ; τ `A : (m, ρ) then (X0, . . . , Xn−1, A) :
(n, τ) → (m, ρ) is a morphism. Composition is defined in virtue of Lemma 1.

Proposition 10 (P(L ),‖,〈〉; /0 ` ε : /0) is a strict symmetric monoidal category.

11 / 17 Volume 29 (2010)



Graph Algebras for Bigraphs

〈〉` ε : 〈〉 〈〉` 0 : /0 〈〉` l(~x) : ~x
Γ ` A : σ ∪~y ~y∩σ = /0

Γ ` L(~x)[A\~y] : σ ∪~x

X : σ ` X : σ
Γ ` A : σ Γ′ ` A′ : σ ′
Γ, Γ′ ` A | A′ : σ ∪σ ′

Γ ` A : ~σ Γ′ ` A′ : ~σ ′
Γ, Γ′ ` A ‖ A′ : ~σ~σ ′

Γ ` A : ~σ
Γ ` ν x.A : ~σ \{x}

Γ ` A : ~σ π permutation
π(Γ) ` A : ~σ

Γ ` A : ~σ
Γ ` A[x 7→ y] : (~σ \{x})∪{y}

Figure 9: Typing rules for restricted agent-graphs where all names are local.

The encoding functor J−K : Big(K )→L(PK ) and the representation function L−M : P(K )→
Big(KL ) are particular cases of the ones for binding bigraphs. Again the two maps establish a
bijection between the two categories.

5.2 Local bigraphs
In local bigraphs all names are localized, hence there are no global names, and variables can have
only their own names. So, the typing is obtained again from the system in Figure 3 by simply
restricting to types of the form (~σ , /0), while in the environment the set of the global names is
always /0. More formally, a typing judgement is of the form Γ ` A : ~σ where A is a term generated
by the grammar (1), a local type ~τ = τ0 . . . τn−1 is a list of simple types, and an environment Γ
is a list of typed variables (Γ = ~X : ~τ = X0 : τ0, . . . , Xn−1 : τn−1). The type inference rules are in
Figure 9. Notice that, in local bigraphs, non-atomic hyperedges can have non-zero in-rank.

Definition 9 The category L(L ) of agent-graphs, over a ranked alphabet L , has local types
~σ as objects, and judgments as morphisms, that is, if X0 : τ0, . . . , Xn−1 : τn−1 ` A : ~σ then
(X0, . . . , Xn−1, A) : ~τ →~σ is a morphism. Composition is defined in virtue of Lemma 1.

Proposition 11 (L(L ),‖,〈〉` ε : 〈〉) is a strict symmetric monoidal category.

The two encoding functors J−K : Lbg(K )→ L(LK ), and L−M : L(K )→ Lbg(KL ) are par-
ticular cases of the ones for binding bigraphs. Notice that, in this particular case, L−M is actually
a functor; and, as before, the two functors establish a bijection between the two categories.

5.3 Prime bigraphs
Following the idea of the functor J−K from agent-graph to bigraphs, we can identify a subcate-
gory of A, where all agents have zero or one variable. These are prime bigraph, that is bigraphs
with at most one hole. One may think of these bigraphs as single-located (open) systems.

We can characterize pure prime bigraphs by a restriction on agent types. A typing judgement
is of the form Γ`A : σ where A is a one-variable term generated by A ::= 0 | l(~x) |X |A|A |ν z.A |
A[w 7→ z]. A prime type σ is a simple type, and an environment Γ is a list of typed variables of
at most length one, i.e., Γ ::= 〈〉 | X : ρ . The induced type inference rules are in Figure 10.

Definition 10 The category H has simple types (τ ) as objects, and judgments as morphisms,

Proc. GT-VMT 2010 12 / 17



ECEASST

〈〉` 0 : /0 〈〉` l(~x) : ~x
Γ ` A : σ Γ′ ` A′ : σ ′ |Γ, Γ′| < 2

Γ, Γ′ ` A | A′ : σ ∪σ ′

X : σ ` X : σ
Γ ` A : σ

Γ ` ν x.A : σ \{x}
Γ ` A : σ

Γ ` A[x 7→ y] : (σ \{x})∪{y}

Figure 10: Typing rules for restricted agent-graphs with one locality.

i.e., if X : τ ` A : ρ then (X , A) : τ → ρ is a morphism or if 〈〉` A : ρ then (〈〉, A) : /0 → ρ is a
morphism. Composition is defined as follows:

Γ ` A : τ X : ρ ` A′ : ρ
Γ ` A′{A/X} : ρ

Proposition 12 (H,|,〈〉` 0 : /0) is a strict symmetric monoidal category.

The two encoding functors J−K : Pbg(K ) → H(LK ) and L−M : H(L ) → Pbg(LK ) can be
defined as a “simplification” of the ones for local bigraphs.

Proposition 13 Let A, A′ be terms; then, for every environment X : τ : X : τ ` A ≡ A′ if and only
if JX : τ ` A : τ′K = JX : τ ` A′ : τ′K.

Proposition 14 Let H, H′ : (〈〉) → (Y ) be two prime graphs; then, H = H′ iff 〈〉 ` LHM〈〉 ≡
LH′M〈〉. Instead, if H, H′ : (X ) → (Y ), then H = H′ iff Q : X ` LHMQ ≡ LH′MQ.

Forgetting localities. Let us consider only atomic signatures Ka, that is, where all controls
are atomic, and hence there is no nesting of nodes. In this case, we can define a functor U :
Lbg(Ka) → Pbg(Ka) which “forgets” the localities of a local bigraph, merging all roots into a
single one and all sites (holes) into a single one. Formally:
Objects: U ((X0 . . . Xn−1)) = X0 +···+ Xn−1.
Morphisms: U ((V, E, ctrl, prnt, link)) = (V, E, ctrl, prnt′, link) where prnt′(v) = 0, for all v.

The previous functors J−K, L−M and the forgetful functor U induce a forgetful functor Π :
L(LKa ) → H(LKa ), defined as follows:
Objects: Π(σ0 . . . σn−1) = σ0 +···+ σn−1.
Morphisms: given a graph in normal form A ≡ ν~z.

(
(Ā0 ‖ . . . ‖ Ān−1)[~X 7→~x]

)
, where every

subgraph Āi ≡
(
li0(~z

i
0) | . . . | liki−1(~ziki−1) | X i0[~Zi0 7→~zi0] | ··· | X ihi−1[~Zihi−1 7→~zihi−1]

)
, then

Π(A) = ν~z.
(
(l00 (~z

0
0) | . . . | l0k0−1(~z

0
k0−1)) | . . . | (l

n−1
0 (~z

n−1
0 ) | . . . | ln−1kn−1−1(~z

n−1
kn−1−1)) |

X [~Z00 7→~z00] . . . [~Z0h0−1 7→~z
0
h0−1] . . . [

~Zn−10 7→~zn−10 ] . . . [~Zn−1hn−1−1 7→~z
n−1
hn−1−1]

)
In practice the above functor merges all the separate agent-graphs into a single-located graph. It
translates a ‖ operator with the | one and unifies all variables into a single one.

As a consequence of the definitions of the functors defined above, we can prove the following
results. Notice that the lists ~X , ~Q and ~τ are either empty or just singletons.

13 / 17 Volume 29 (2010)



Graph Algebras for Bigraphs

Proposition 15 Let ~X : ~τ ` A : ρ = Π(Γ ` B : ~σ ); then, ~X : ~τ ` LU (JΓ ` B : ~σ K)M~X ≡ A.

Proposition 16 1. Let P : (~X ) → (Y ) be a prime bigraph, then J~Q : ~X ` LPM~QK = P.

2. Let ~X : ~τ ` A : σ be a term, then ~X : ~τ ` LJ~X : ~τ ` A : σ KM~X ≡ A.

6 Comparing with SHR hypergraphs and ADR designs

Our language for binding bigraphs can be used for capturing formalisms introduced in literature,
often for quite different purposes. Here we consider the hypergraphs used in Synchronized Hy-
peredge Rewriting (SHR) [FHL+05] and the “designs” of Architectural Design Rewriting (ADR)
[BLMT07]. Both are derived from the algebra of graphs introduced first in [CMR94].
SHR hypergraphs. SHR is a framework that allows hypergraph transformations by means of
local productions replacing a single hyperedge by a generic hypergraph, possibly with constraints
given by the surrounding nodes. The global rewriting is obtained by combining different local
production whose conditions are compatible (with respect to some synchronization model).

In this paper, we are interested only in SHR hypergraphs, which are inductively defined as:

G ::= 0 | l(~x) | G|G | ν x.G
where 0 is the empty graph, the hyperedge l is linked to the nodes in ~x, and ν binds x in G.

Clearly, the SHR grammar is a particular case of the one for prime bigraphs (Section 5.3), and
specifically when the variable and substitutions are dropped.
ADR designs. ADR graphs (called designs) resemble SHR graphs, but they have a notion of
graph nesting, as some hyperedges can contain other graphs. Such nesting is used for incremental
modelling, that is, edges can be refined into graphs or vice versa graphs collapse into edges. The
ADR designs are inductively defined as:

D ::= L[λ~x.G] G ::= 0 | x | l(~x) | G|G | ν x.G | D(~x)
where 0 is the empty graph, the hyperedge l is linked to the nodes in ~x, ν binds x in G, D(~x) is
a design generated by attaching design D to nodes ~x, and finally L[λ~x.G] represent a design L,
with “body graph” G and exposing the names ~x in its interface.

The grammar of designs recalls the one defined for local bigraphs, when the ‖ composition is
omitted. In such a case, we deal with graphs residing in only one location. A formal translation
of the ADR design grammar into the grammar in (1) can be defined as follow:

T (0) = 0 T (x) = 0[z 7→ x] (z fresh) T (G1 | G2) = T (G1) | T (G2)
T (l(~x)) = l(~x) T (ν x.G) = ν x.T (G) T (L[λ~x.G](~y)) = L(~y)[G\~x]

By means of these translations of SHR hypergraphs as prime bigraphs, and ADR designs as
local bigraphs, we can transfer results and constructions among formalisms developed indepen-
dently. As examples, it is possible to extend the SHR semantics allowing for not only replacing
single hyperedges, but more complex graphs; moreover, we can also define congruent bisimula-
tions for SHR systems via the so-called IPO construction over bigraphical reactive systems.

Proc. GT-VMT 2010 14 / 17



ECEASST

7 Conclusion

In this paper we have first defined an algebra of typed term graphs which corresponds precisely to
binding bigraphs, on a given signature. Secondly, we have shown that particular sublanguages of
our main language properly characterize interesting subclasses of bigraphs, more precisely: pure
and local bigraphs. Moreover, on this last kind of bigraphs we also give a reduced language for
dealing with one-location (bi)graphs, named prime bigraphs. So, those languages can be used in
place of the more complex bigraph algebra already present in literature. A family of bigraphical
calculi has been introduced in [DK08]; however, these calculi has been suitably restricted for
modelling biological systems and do not cover all possible bigraphs over a given signature.

Finally, it turns out that these languages are strictly connected with two well-know formalisms:
Synchronized Hyperedge Replacement hypergraphs, which can be represented as a sublanguage
of the algebra for prime bigraphs (over atomic signatures), and Architectural Design Rewriting
designs, which are a sub-case of the local bigraphs’ language.

A possible future work is to take advantage of the rich theory provided by bigraphical reactive
systems [JM03], in order to obtain interesting results about SHR and ADR. In particular, we hope
to generalize the transitions allowed in SHR graphs, which only rewrites a single hyperedge, to
more general ones dealing with (sub)graphs. Moreover, bigraphs allow to synthesise labelled
transition systems out of rewriting rules, via the so-called idem-pushout construction [LM00];
it is important to notice that the bisimilarity induced by this labelled transitions system (LTS)
is always a congruence. Therefore, given a reactive system over SHR (ADR) graphs, we can
derive the labelled transition system in bigraphs, and remap it on SHR (ADR) graphs. Then, the
inductive definition of SHR (ADR) agents can be useful for defining an SOS-like presentation of
the LTS derived in this way.

Acknowledgments. We thank Emilio Tuosto and Ivan Lanese for useful discussions about SHR.

Bibliography

[BDE+06] L. Birkedal, S. Debois, E. Elsborg, T. Hildebrandt, H. Niss. Bigraphical Models of
Context-Aware Systems. In Aceto and Ingólfsdóttir (eds.), Proc. FoSSaCS. Lecture
Notes in Computer Science 3921, pp. 187–201. Springer, 2006.

[BDGM07] L. Birkedal, T. C. Damgaard, A. J. Glenstrup, R. Milner. Matching of Bigraphs.
Electr. Notes Theor. Comput. Sci. 175(4):3–19, 2007.

[BGH+08] M. Bundgaard, A. J. Glenstrup, T. T. Hildebrandt, E. Højsgaard, H. Niss. Formal-
izing Higher-Order Mobile Embedded Business Processes with Binding Bigraphs.
In Lea and Zavattaro (eds.), COORDINATION. Lecture Notes in Computer Sci-
ence 5052, pp. 83–99. Springer, 2008.

[BLMT07] R. Bruni, A. Lluch-Lafuente, U. Montanari, E. Tuosto. Service Oriented Architec-
tural Design. In Barthe and Fournet (eds.), Proc. TGC. Lecture Notes in Computer
Science 4912, pp. 186–203. Springer, 2007.

15 / 17 Volume 29 (2010)



Graph Algebras for Bigraphs

[CMR94] A. Corradini, U. Montanari, F. Rossi. An Abstract Machine for Concurrent Modular
Systems: CHARM. Theor. Comput. Sci. 122(1&2):165–200, 1994.

[DB06] T. C. Damgaard, L. Birkedal. Axiomatizing Binding Bigraphs. Nord. J. Comput.
13(1-2):58–77, 2006.

[DK08] T. C. Damgaard, J. Krivine. A Generic Language for Biological Systems based on
Bigraphs. Technical report TR-2008-115, IT University of Copenhagen, Dec. 2008.

[FHL+05] G. L. Ferrari, D. Hirsch, I. Lanese, U. Montanari, E. Tuosto. Synchronised Hyper-
edge Replacement as a Model for Service Oriented Computing. In Boer et al. (eds.),
Proc. FMCO. Lecture Notes in Computer Science 4111, pp. 22–43. Springer, 2005.

[GM07] D. Grohmann, M. Miculan. Reactive Systems over Directed Bigraphs. In Caires
and Vasconcelos (eds.), Proc. CONCUR 2007. Lecture Notes in Computer Sci-
ence 4703, pp. 380–394. Springer, 2007.

[JM03] O. H. Jensen, R. Milner. Bigraphs and transitions. In Proc. POPL. Pp. 38–49. 2003.

[JM04] O. H. Jensen, R. Milner. Bigraphs and mobile processes (revised). Technical re-
port UCAM-CL-TR-580, Computer Laboratory, University of Cambridge, 2004.

[LM00] J. J. Leifer, R. Milner. Deriving Bisimulation Congruences for Reactive Systems.
In Palamidessi (ed.), Proc. CONCUR. Lecture Notes in Computer Science 1877,
pp. 243–258. Springer, 2000.

[LM06] J. J. Leifer, R. Milner. Transition systems, link graphs and Petri nets. Mathematical
Structures in Computer Science 16(6):989–1047, 2006.

[Mil01] R. Milner. Bigraphical Reactive Systems. In Larsen and Nielsen (eds.), Proc. 12th
CONCUR. Lecture Notes in Computer Science 2154, pp. 16–35. Springer, 2001.

[Mil04] R. Milner. Bigraphs whose names have multiple locality. Technical report 603, Uni-
versity of Cambridge, CL, Sept. 2004.

A Structural congruence

The free name function f n is defined as follows with respect to an environment (Γ, τ).

f nΓ ; τ (ε) = τ f nΓ ; τ (L(~x)[A\~y]) = ( f nΓ ; τ (A)\~y)∪~x∪τ
f nΓ ; τ (0) = τ f nΓ ; τ (A1 | A2) = f nΓ ; τ (A1)∪ f nΓ ; τ (A2)

f nΓ ; τ (l(~x)) =~x∪τ f nΓ ; τ (A1 ‖ A2) = f nΓ ; τ (A1)∪ f nΓ ; τ (A2)
f nΓ ; τ (ν y.A) = f nΓ ; τ (A)\{y} f nΓ ; τ (A[w 7→ z]) = ( f nΓ ; τ (A)\{w})∪{z}
f nΓ ; τ (A |• x) = f nΓ ; τ (A) f nΓ ; τ (A |• x) = f nΓ ; τ (A)

f nΓ ; τ (Xi) = τi ∪τ if Xi:τi ∈ Γ

Proc. GT-VMT 2010 16 / 17



ECEASST

In the following table, the structural congruence for agent-graph is defined with respect to
some environment Γ ; τ .

Γ
;τ
`

A
|0
≡

A

Γ
;τ
`

A
1
|A

2
≡

A
2
|A

1

Γ
;τ
`

(A
1
|A

2
)
|A

3
≡

A
1
|(

A
2
|A

3
)

Γ
;τ
`

A
‖ε
≡

A

Γ
;τ
`

ε
‖A
≡

A

Γ
;τ
`

(A
1
‖A

2
)
‖A

3
≡

A
1
‖(

A
2
‖A

3
)

Γ
;τ
`

ν
x.

0
≡

0
if

x
/∈

fn
Γ

;τ
(0

)
Γ

;τ
`

ν
x.

ε
≡

ε
if

x
/∈

fn
Γ

;τ
(ε

)
Γ

;τ
`

ν
x.

ν
y.

A
≡

ν
y.

ν
x.

A

Γ
;τ
`

ν
x.

A
≡

ν
y.

(A
{y

/
x}

)
if

y
/∈

fn
Γ

;τ
(A

)
Γ

;τ
`

A
[x
7→

y]
≡

(A
{z

/
x}

)[
z
7→

y]
if

z
/∈

fn
Γ

;τ
(A

)
Γ

;τ
`

A
[x
7→

x]
≡

A
if

x
∈

fn
Γ

;τ
(A

)
Γ

;τ
`

A
[x
7→

y]
≡

A
if

x
/∈

fn
Γ

;τ
(A

)∧
y
∈

fn
Γ

;τ
(A

)
Γ

;τ
`

A
[x
7→

y]
[w
7→

z]
≡

A
[w
7→

z]
[x
7→

y]
if

x
6=

z,
y
6=

w

Γ
;τ
`

A
[x
7→

y]
[y
7→

z]
≡

A
[x
7→

z]
if

y
/∈

fn
Γ

;τ
(A

)
Γ

;τ
`

ν
y.

(A
[x
7→

y]
)
≡

ν
x.

A
if

y
/∈

fn
Γ

;τ
(A

)
Γ

;τ
`

ν
z.

(A
[x
7→

y]
)
≡

(ν
z.

A
)[

x
7→

y]
if

z
/∈
{x

,y
}

Γ
;τ
`

A
| •x
|• x
≡

A
if

x
∈

fn
Γ

;τ
(A

)
Γ

;τ
`

A
|• x
| •x
≡

A
if

x
∈

fn
Γ

;τ
(A

)
Γ

;τ
`

A
| •x

[x
7→

y]
≡

A
[x
7→

y]
| •y

Γ
;τ
`

A
| •x

[y
7→

z]
≡

A
[y
7→

z]
| •x

if
y
6=

x
∧

z
6=

x

Γ
;τ
`

A
|• x

[x
7→

y]
≡

A
[x
7→

y]
|• y

Γ
;τ
`

A
|• x

[y
7→

z]
≡

A
[y
7→

z]
|• x

if
y
6=

x
∧

z
6=

x

Γ
;τ
`

ν
x.

(A
| •x

)
≡

ν
x.

A
if

x
∈

fn
Γ

;τ
(A

)
Γ

;τ
`

ν
y.

(A
| •x

)
≡

(ν
y.

A
)
|• x

if
x
6=

y

Γ
;τ
`

ν
x.

(A
|• x

)
≡

ν
x.

A
if

x
∈

fn
Γ

;τ
(A

)
Γ

;τ
`

ν
y.

(A
|• x

)
≡

(ν
y.

A
)
|• x

if
x
6=

y

Γ
;τ
`

ν
x.

(A
1
|A

2
)
≡

ν
x.

A
1
|A

2
if

x
/∈

fn
Γ

;τ
(A

2
)

Γ
;τ
`

ν
x.

(A
1
‖A

2
)
≡

ν
x.

A
1
‖A

2
if

x
/∈

fn
Γ

;τ
(A

2
)

Γ
;τ
`

ν
x.

(A
1
‖A

2
)
≡

A
1
‖ν

x.
A

2
if

x
/∈

fn
Γ

;τ
(A

1
)

Γ
;τ
`

(A
1
|A

2
)[

x
7→

y]
≡

A
1
[x
7→

y]
|A

2
if

x
/∈

fn
Γ

;τ
(A

2
)

Γ
;τ
`

(A
1
|A

2
)[

x
7→

y]
≡

A
1
[x
7→

y]
|A

2
[x
7→

y]
Γ

;τ
`

(A
1
‖A

2
)[

x
7→

y]
≡

A
1
[x
7→

y]
‖A

2
if

x
/∈

fn
Γ

;τ
(A

2
)∧

x
∈

fn
Γ

;τ
(A

1
)

Γ
;τ
`

(A
1
‖A

2
)[

x
7→

y]
≡

A
1
‖A

2
[x
7→

y]
if

x
/∈

fn
Γ

;τ
(A

1
)∧

x
∈

fn
Γ

;τ
(A

2
)

Γ
;τ
`

(A
1
‖A

2
)[

x
7→

y]
≡

A
1
[x
7→

y]
‖A

2
[x
7→

y]
if

x
∈

fn
Γ

;τ
(A

1
)∩

fn
Γ

;τ
(A

2
)

Γ
;τ
`

(A
1
‖A

2
)[

x
7→

y]
≡

A
1
[x
7→

y]
‖A

2
[x
7→

y]
if

x
/∈

fn
Γ

;τ
(A

1
)∪

fn
Γ

;τ
(A

2
)

Γ
;τ
`

(A
1
|A

2
)
| •x
≡

A
1
| •x
|A

2
if

x
∈

fn
Γ

;τ
(A

1
)∧

x
/∈

fn
Γ

;τ
(A

2
)

Γ
;τ
`

(A
1
|A

2
)
| •x
≡

A
1
| •x
|A

2
| •x

if
x
∈

fn
Γ

;τ
(A

1
)∩

fn
Γ

;τ
(A

2
)

Γ
;τ
`

(A
1
|A

2
)
|• x
≡

A
1
|• x
|A

2
if

x
∈

fn
Γ

;τ
(A

1
)∧

x
/∈

fn
Γ

;τ
(A

2
)

Γ
;τ
`

(A
1
|A

2
)
|• x
≡

A
1
|• x
|A

2
|• x

if
x
∈

fn
Γ

;τ
(A

1
)∩

fn
Γ

;τ
(A

2
)

Γ
;τ
`

(A
1
‖A

2
)
|• x
≡

A
1
|• x
‖A

2
if

x
∈

fn
Γ

;τ
(A

1
)∧

x
/∈

fn
Γ

;τ
(A

2
)

Γ
;τ
`

(A
1
‖A

2
)
|• x
≡

A
1
‖A

2
|• x

if
x

/∈
fn

Γ
;τ

(A
1
)∧

x
∈

fn
Γ

;τ
(A

2
)

Γ
;τ
`

(A
1
‖A

2
)
|• x
≡

A
1
|• x
‖A

2
|• x

if
x
∈

fn
Γ

;τ
(A

1
)∩

fn
Γ

;τ
(A

2
)

Γ
;τ
`

l(
~x
)[

x
7→

z]
≡

l(
~x
){

z/
x}

if
x
∈~

x

Γ
;τ
`

L
(~x

)[
A
\~y

]≡
L
(~x

)[
(A
{z

/
y}

)\
(~y
{z

/
y}

)]
if

x
∈~

y
∧

z
/∈~

y
∪

fn
Γ
(A

)
Γ

;τ
`

ν
z.

L
(~x

)[
A
\~y

]≡
L
(~x

)[
(ν

z.
A
)\~

y]
if

z
/∈~

x
∪~

y

Γ
;τ
`

L
(~x

)[
A
\~ Y

][
x
7→

w
]≡

L
(~x
{w

/
x}

)[
A
\~y

]i
f

x
∈~

x
∧

w
/∈

(f
n Γ

(A
)\

~y
)

Γ
;τ
`

L
(~x

)[
A
\~y

][
w
7→

z]
≡

L
(~x

)[
(A

[w
7→

z]
)\~

y]
if

w
/∈~

x
∪~

y
∧

z
/∈~

y

Γ
;τ
`

L
(~x

)[
A
[w
7→

y]
\~y

]≡
L
(~x

)[
A
\(~

y{
w

/
y}

]i
f

y
∈~

y
∧

w
/∈

fn
Γ

;τ
(A

)
Γ

;τ
`

L
(~x

)[
A
\~y

]| •
z
≡

L
(~x

)[
(A
| •z

)\~
y]

if
z

/∈~
x
∪~

y

Γ
;τ
`

L
(~x

)[
A
\~y

]|•
z
≡

L
(~x

)[
(A
|• z

)\~
y]

if
z

/∈~
x
∪~

y

17 / 17 Volume 29 (2010)


	Introduction
	Binding Bigraphs
	Graph Grammar for Bigraphs
	Interpreting Agent Graphs as Binding Bigraphs
	Interpretation of agent-graphs as binding bigraphs
	Representing binding bigraphs with agent-graphs

	Characterizing pure, local and prime bigraphs
	Pure bigraphs
	Local bigraphs
	Prime bigraphs

	Comparing with SHR hypergraphs and ADR designs
	Conclusion
	Structural congruence