Information Technology Reference
In-Depth Information
Let
E
be an expression and
F
1
,F
2
be two subexpressions occuring in
E
.
We say that the occurrence of
F
1
is before the occurrence of
F
2
if there is a
subexpression of the form
E
1
;
E
2
in
E
such that the occurrence of
F
1
is in
E
1
and the occurrence of
F
2
is in
E
2
. We say that the occurrence of
F
1
is unguarded
if there is no subexpression which occurs before
F
1
, otherwise the occurrence
of
F
1
is called guarded. If
F
occurs unguarded in
E
, the nesting depth of the
occurrence is the number of subexpressions of the form
E
1
;
E
2
where
E
1
contains
the occurrence.
a
−→
Lemma 5.
If
E
α
, then there is an unguarded occurrence of
a
in
E
such
that the length of
α
equals to the nesting depth of the occurrence.
Proof:
Induction on the rules in Table 2.
Theorem 2.
Every
α
∈S
is finite branching.
a
−→
Proof:
We need to show that the set
B
(
α
)=
is finite.
If
α
=
then it holds trivially. If
α
=
Eα
, then by the rules of Table 2
B
(
α
)
has the same number of elements as
B
(
E
)=
{
β
|
a
∈
Act, α
β
}
a
−→
{
γ
|
a
∈
Act, E
γ
}
.Nowby
a
−→
Theorem 1 if
E
γ
then the processes which can occur in
γ
is from a finite
set. Moreover by the previous lemma the length of
γ
is bounded, thus
B
(
E
)
must be finite.
3
Expansive-Bisimulation
This section contains the main result of the paper, where we study expansive-
bisimulation which gives a finite characterization of bisimilar BPA processes.
Definition 4.
A state
α
is said to be
normed
if there exists a finite sequence
of transitions from
α
to
. The norm of a process
α
is the length of the shortest
transition sequence from
α
to
.Wedenoteby
∈S
N
(
α
)
the norm of
α
.
It is easy to see that for normed processes
α, β
we have the following facts:
(
α
)=0iff
α
=
.
2. Norm is additive:
N
1.
N
(
αβ
)=
N
(
α
)+
N
(
β
).
3.
∼
preserves norms: If
α ∼ β
then
N
(
α
)=
N
(
β
).
Clearly
α
is normed if and only if each process occurring in it is normed. We
define a function
:
S→S
such that for
α
∈S
,if
α
is normed then
α
=
α
,if
α
is un-normed then
α
is the least prefix of
α
which ends with an un-normed
process. And we will call the part of
α
after
α
its tail. Thus the tail of any
normed state is always
.Wesaythat
α
is standard if
α
=
α
.Inotherwords,
a state is standard just in case its tail is
.
A straightforward consequence of the definition of having a norm is that if
α
is un-normed then
αβ
∼
α
holds for any
β
∈S
.
Search WWH ::
Custom Search