Information Technology Reference
In-Depth Information
Definition 5.
A binary relation
R
⊆S×S
is an expansive-bisimulation if for
all
(
α, β
)
∈
R
it holds that either
α
=
β
,or
α
=
Eα
1
,β
=
Fβ
1
and there exist
α
2
,β
2
,γ
∈S
such that
(
α
1
,α
2
γ
)
∈
R,
(
β
2
γ,β
1
)
∈
R
, and moreover the following
hold:
a
−→
a
−→
α
,then
Fβ
2
β
for some
β
such that
(
α
,β
)
1. if
Eα
2
∈
R
;
a
−→
a
−→
β
,then
Eα
2
α
for some
α
such that
(
α
,β
)
2. if
Fβ
2
∈
R
.
It is not dicult to see that for a finite relation, whether it is an expansive-
bisimulation is decidable.
Proposition 2.
If
R
is an expansive-bisimulation, then
R
⊆∼
.
Proof:
Suppose
R
is an expansive-bisimulation, then it is easy to check that
R
is a self-bisimulation. Thus
R
is included in a
self-bisimulation, and then by Proposition 1
R
∪{
(
α, β
)
|
α, β
∈S
,α
=
β
}
⊆∼
.
Definition 6.
When
Eα
Fβ
we say that the pair
(
Eα, Fβ
)
is decomposable
if
E, F
are normed and there is a
γ
such that
∼
•
α
∼
γβ
and
Eγ
∼
F
if
N
(
E
)
≤N
(
F
)
,
•
γα
∼
β
and
E
∼
Fγ
if
N
(
F
)
≤N
(
E
)
.
Theorem 3.
Let
α, β
β
if and only if there exists a finite
expansive-bisimulation which contains
(
α, β
)
.
∈S
,then
α
∼
Proof:
The soundness part easily follows from Proposition 2.
Now suppose
α
0
β
0
, to show the completeness we will construct a finite
expansive-bisimulation
R
which contains (
α
0
,β
0
). In order to construct such
R
,
we rely on the following fact which was first proved in [CHS92] in the process of
showing the existence of a complete finite self-bisimulation:
∼
There exists a finite relation
R
0
⊆S×S
such that if (
α, β
)
∈
R
0
then
α
∼
β
and moreover if
Eα, Fβ
are standard and
Eα
∼
Fβ
is not de-
composable, then there exists (
Eα
,Fβ
)
α
∈
R
0
such that
α
∼
and
β
.
β
∼
With this fact, our construction of
R
isbasedonsuch
R
0
as follows. Let
S
0
=
{
α
0
,β
0
}∪{
γ
|∃
α.
(
α, γ
)
∈
R
0
or (
γ,α
)
∈
R
0
}
a
−→
a
−→
∪{
γ
|∃
(
α, β
)
∈
R
0
,a
∈
Act.α
γ
or
β
γ
}
.
Since
R
0
is finite and every state is finite branching,
S
0
is a finite set. Choose
n
such that whenever
γ
0
is a normed prefix of some
γ
∈
S
0
then
N
(
γ
0
)
≤
n
,
obviously such
n
exists as
S
0
is finite. Let
S
1
consists of those states
γ
of
which the norm of its maximal normed prefix is less than or equal to
n
,and
itstailisatailofsome
γ
∈S
∈
S
0
. Then it is not dicult to see that
S
0
⊆
S
1
.
Moreover, note that the states in
S
only contain processes from a finite set
P
,
Search WWH ::
Custom Search