In this section we will show that interleaving bisimulation equivalence [Park, Milner] is preserved under safe refinements.
A relation
R⊆![]() ![]() ![]() ![]() ![]() ![]()
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
In [GG a] it has been shown that the configurations of a refined event structure may be deduced compositionally from the configurations of the original event structure and those of the refinements of actions. We will use this result and the following lemmas in the proof of the refinement theorem.
|
Clearly, if
∈
(X) then
X = pr(
) : = {e∈E
| ∃e'∈E
(l(e)) : (e, e')∈
}
and we have
compl (
)⊆pr(
),
pr(
) - max(pr(
))⊆compl (
).
Proof
Immediate from proposition (iii), since
pr(
) - max(pr(
))⊆Y⊆pr(
).
With lemma we have in particular
compl (
)∈
(
).
Proof Immediate from the definitions.
Proof With proposition we have
Xe∈
(
(l
(e))) - {∅}.
If
l(e)∈Crit
than Xe is
complete by proposition
.
However, since
e∈pr() - compl (
), Xe is not complete.
Proof
W.l.o.g. we assume that
e pr(
).
With proposition (i) we prove that
pr(
) enables e.
Suppose
∃d∈pr() with d#e. Since
compl (
)∪{e} is
conflict-free, it follows that
d∈pr(
) - compl (
).
Thus
compl (
) enables d (with lemma
) as well as e, so d ch e.
However, with lemma
we have
l (d )
Crit
, contradicting d ch e.
Now suppose d e and
d
pr(
)⊇compl (
).
Since
compl (
)∪{e}∈
(
) there is an
f∈compl (
)⊆pr(
) with f
e and d#f.
With these lemmas we can prove the theorem.
Proof Let R be a bisimulation between
and
.
Let
= {(
,
)∈
(
(
))×
(
(
)) |
(compl (), compl (
))∈R,
there exist bijections
f : pr()→pr(
)
with
l
(f (e)) = l
(e)
and
:
→
with
(e, e') = (f (e), e')}
We show that is a bisimulation
between
(
) and
(
).
i. Obviously
(∅,∅)∈.
ii. Let
(,
)∈
. Then
(compl (
), compl (
))∈R and there are bijections
f and
as required in the definition of
.
We have to show the bisimulation properties.
It suffices to check one of them, the other follows by symmetry.
Let
a
→
.
Let
-
= {(eo, e*)},
l
(eo) = b.
Then
l
(
)((eo, e*)) = l
(b)(e*) = a.
Now we have to show :
∃∈
(
(
)) with
a
→
and
(
,
)∈
.
For the construction of , we distinguish two cases.
1.
pr() = pr(
).
In this case we can use the bijection f to define , since
its domain is not affected by adding the new event.
Let
: = {(f (e), e') | (e, e')∈
}.
With
= {(f (e), e') | (e, e')∈
} we have
=
∪{(f (eo), e*)}.
First we show that is a configuration with
a
→
.
Then we define the new functions f' and and check their properties.
Finally we prove
(compl (), compl (
))∈R.
With proposition we show
∈
(
(
)):
- |
pr(![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
- |
∀d∈pr(![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
- |
busy(![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Let f' : = f and
: =
∪{((eo, e*),(f (eo), e*))}.
The new function
is bijective, since the events
(eo, e*) and
(f (eo), e*) do not occur in the domain and the range of
, respectively.
By construction f' and
have the required properties.
In order to establish
(,
)∈
we still have to show
(compl (
), compl (
))∈R.
Again we have two cases:
Since
(compl (), compl (
))∈R there is a
Y'∈
(
)
with
compl (
)
b
→ Y' and
(compl (
), Y')∈R.
Using the properties of ,
compl (
) = f'(compl (
)) = f (compl (
)∪{eo}) = compl (
)∪{f (eo)}, hence
compl (
)
b
→compl (
).
Since
eo∈compl ()⊆pr(
) = pr(
),
it follows that
eo∈pr(
) - compl (
) and with lemma
b = l
(eo)
Crit
. Hence
Y' = compl (
) with lemma
.
Thus
(compl (), compl (
))∈R, which had to be proved.
The proof of the second case is similar to that of the first case. However
the construction of is more complicated since we cannot just use
the function f. We need to describe the events by which f is extended.
pr() = pr(
)∪{eo} and
l
(eo) = b.
compl () =
Thus
compl ()⊆compl (
)∪{eo}⊆pr(
)∪{eo} = pr(
).
With lemma it follows that
compl (
)∪{eo}∈
(
).
Hence
compl ()
b
→ compl (
) ∪ {eo}.
Since
(compl (), compl (
))∈R, there is a
do∈E
with
compl (
)
b
→compl (
)∪{do},
l
(do) = b and
(compl (
)∪{eo}, compl (
)∪{do})∈R.
We now extend the bijection f by
(eo, do).
For this we verify that
do is not in the range of f:
Suppose
do∈pr().
Since
do
compl (
),
f-1(do)∈pr(
) - compl (
).
Thus
compl (
)∪{f-1(do)}∈
(
)
with lemma
and
compl (
)
b
→ compl (
)∪{f-1(do)}.
Hence
b Crit
with lemma
and then
eo = f-1(do) with lemma
.
Thus
eo∈pr() which contradicts
pr(
)≠pr(
).
So
do
pr(
).
Now we can define
, f' and
.
Let
f' : = f∪(eo, do) and
: = {(f'(e), e') | (e, e')∈
} =
∪{(do, e*)}.
Using proposition we proof
∈
(
(
)):
The new function f' is bijective, as shown above.
The same for
: =
∪{((eo, e*),(do, d*))}. By construction
f' and
have the required properties.
Now we show
(,
)∈
by proving
(compl (
), compl (
))∈R.
There are again two cases: