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 α
= 1
= 1 and there exist
α 2 2
∈S
such that ( α 1 2 γ )
R, ( β 2 γ,β 1 )
R , and moreover the following
hold:
a
−→
a
−→
α ,then 2
β for some β such that ( α )
1. if 2
R ;
a
−→
a
−→
β ,then 2
α for some α such that ( α )
2. if 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
we say that the pair ( Eα, Fβ ) is decomposable
if E, F are normed and there is a γ such that
α
γβ and
F if
N
( E )
≤N
( F ) ,
γα
β and E
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
is not de-
composable, then there exists ( ,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