Information Technology Reference
In-Depth Information
S
1
must be finite since for each element in it, the norm of the maximum normed
prefix is bounded, and the tail is also from a finite set. Now construct
R
=
{
(
α, β
)
|
α, β
∈
S
1
,α
∼
β
}
,
then
R
is finite. The rest of the proof is to show that
R
is an expansive-
bisimulation, then since
α
0
,β
0
∈
S
1
and
α
0
∼
β
0
,thus(
α
0
,β
0
)
∈
R
so we
can conclude the completeness proof.
To show that
R
is an expansive-bisimulation, take any (
α, β
)
∈
R
, and suppose
α
=
β
, we will show that
α
=
Eα
1
,β
=
Fβ
1
and there exist
α
2
,β
2
,γ
such that
(
α
1
,α
2
γ
)
∈
R
and (
β
2
γ,β
1
)
∈
R
and moreover
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
.
Since
α ∼ β
and
α
=
β
, then it must be the case that neither of
α, β
is
,so
α
=
Eα
1
,β
=
Fβ
1
for some
E, F, α
1
,β
1
, and obviously
Eα
1
,Fβ
1
are standard.
If
Eα
1
∼
Fβ
1
is not decomposable, then according to the property of
R
0
there
exists (
Eα
2
,Fβ
2
)
β
2
, and now take
γ
=
we
can show that
α
2
,β
2
,γ
are just what we want. For that we need to show that
(
α
1
,α
2
γ
)
∈
R
0
such that
α
1
∼
α
2
,
β
1
∼
∈
R
,(
β
2
γ,β
1
)
∈
R
, and moreover requirements 1. and 2. above are
satisfied. To see (
α
1
,α
2
γ
)
∈
R
, just note that
Eα
1
,Eα
2
∈
S
1
which implies
α
1
,α
2
∈
S
1
,andmoreover
α
1
∼
α
2
,so(
α
1
,α
2
γ
)=(
α
1
,α
2
)
∈
R
. For the same
reason (
β
2
γ,β
1
)
∈
R
. To see requirement 1. is satisfied, note that
Eα
2
∼
Fβ
2
,
a
−→
a
−→
α
there must exist
β
β
and
α
β
.
so for
Eα
2
such that
Fβ
2
∼
According to the construction in this case
α
,β
∈
S
1
,so(
α
,β
)
∈
R
.Inthesame
way we can show that 2. is also satisfied. Now if
Eα
1
∼
Fβ
1
is decomposable,
then both
E
and
F
are normed and there exists
δ
such that A:
E
∼
Fδ
and
δα
1
∼
β
1
,orB:
Eδ
∼
F
and
α
1
∼
δβ
1
.IfitiscaseA,thensince
E
∼
Fδ
is not
decomposable, there is (
Eξ, Fη
)
∈
R
0
such that
∼
ξ, δ
∼
η
.Nowwecantake
α
2
=
, β
2
=
η, γ
=
α
1
, and we will show that (
α
1
,α
2
γ
)
∈
R
,(
β
2
γ,β
1
)
∈
R
,and
moreover requirements 1. and 2. above are satisfied. To see (
α
1
,α
2
γ
)
∈
R
,note
that
α
1
∈
S
1
and
α
2
γ
=
α
1
,thus
α
2
γ
∈
S
1
and
α
1
∼
α
2
γ
thus (
α
1
,α
2
γ
)
∈
R
.
To see (
β
2
γ,β
1
)
∈
R
,notethat
β
2
γ
=
ηα
1
∼
δα
1
∼
β
1
,
Fβ
1
∈
S
1
thus
β
1
∈
S
1
,
Eα
1
∈
S
1
,
E
∼
Fδ
∼
Fη
and
E
is normed, so
N
(
E
)=
N
(
Fη
)and
Fηα
1
∈
S
1
thus
ηα
1
∈
S
1
,wehave
β
2
γ
=
ηα
1
∈
S
1
,so(
β
2
γ,β
1
)
∈
R
. To see 1. is satisfied,
note that (
Eα
2
,Fβ
2
)
Fβ
2
, and the reasoning is as in the
previous case for non-decomposable
Eα
1
∼
∈
R
0
,so
Eα
2
∼
Fβ
1
. The case B can be checked in
the same way.
In proving decidability of bisimilarity of context-free processes [CHS92], Chris-
tensen, Huttel, and Stirling proved that two context-free processes are bisimula-
tion equivalent if and only if they can be generated by a finite (full)
self-bisimulation. Based on their work, the last theorem gives a finite char-
acterization of bisimulation equivalence for context-free processes in terms of
expansive-bisimulation. In [BCS95], Burkart, Caucal and Steffen presented an
elementary time algorithm that can compute a (full) self-bisimulation which can
Search WWH ::
Custom Search