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:
In either case, we have found a
node in G2;H2:
E2
where N1 R;S N2. Thus composition respects bisimulation.
Back