# Proof that bisimulation is a congruence

Proposition (Bisimulation is a congruence). Bisimulation is a congruence wrt the graph operations.

Proof. It is routine to show that bisimulation is an equivalence.

To show that it is a congruence, we have to show it is respected by composition and tensor. Of these, tensor is simpler, so we shall show the case for composition.

If we have bisimulations R and S with:

R
S
we would like to find a bisimulation R;S with:
R;S
Wlog, we shall assume the graphs have disjoint node and edge sets. Define union on graphs with overlapping edge sets as G G with:

- Nodes and edges taken as the union of G and Gs.

- Incoming edges from G.

- Outgoing edges from G.

Given graph G including vector of edges E, let G[F/E] be the graph given by renaming edges E to F.

We have graphs:

G1 : E1 E1
G2 : E2 E2
H1 : F1 F1
H2 : F2 F2

and:
G1;H1 = G1 H1[E1/F1]
G2;H2 = G2 H2[E2/F2]

Then define relation:

R;S R S[E1/F1]

It is routine to show that this relation respects incoming and outgoing edges, labelling, and is an isomorphism between incoming edges. To show that R;S is a bisimulation, consider any node in G1;H1:

E1
where E1 R;S E2. Then either:

- E1 G1, so N1 G1 and E1 R E2. Since R is a bisimulation, we can find a N2 G2 with N1 R N2.

- E1 H1, so E1 is not an incoming edge of H1, so E2 is not an incoming edge of H2, so N1 H1 and E1 S E2. Since S is a bisimulation, we can find a N2 H2 with N1 S N2.

In either case, we have found a node in G2;H2:
E2
where N1 R;S N2. Thus composition respects bisimulation.

Back