Information Technology Reference
In-Depth Information
Let
ʘ
=
i
∈
I
,
j
∈
J
i
p
i
q
ij
·
ʘ
ij
. By Theorem 6.5(i) the relation
⃒
is linear. Now, it is
=
i
∈
I
p
i
j
∈
J
i
q
ij
ʘ
i
ʱ
⃒
ʱ
⃒
ʘ
.
easy to see that
is also linear. It follows that
ʘ
(
i
∈
I
p
i
j
∈
J
i
q
ij
·
ʔ
ij
)(
≈
s
)
†
, we notice that
ʔ
=
≈
s
)
†
ʘ
.
By the linearity of (
˄
⃒
ʔ
then there is some ʘ
with
Theorem 7.2
In a finitary pLTS, if s
≈
s
ʘ and s
˄
⃒
ʘ
and ʔ
(
≈
s
)
†
ʘ
.
Proof
The arguments are similar to those in the proof of Theorem 6.12. Suppose
s
is a state and
ʘ
a distribution in a finitary pLTS such that
s
≈
s
ʘ
and
s
ʘ
˄
⃒
ʔ
.
Referring to Definition 6.4, there must be
ʔ
k
,
ʔ
k
and
ʔ
k
for
k
≥
0 such that
s
=
ʔ
0
,
ʔ
k
+
1
and
ʔ
=
k
=
1
ʔ
k
. Since
ʔ
0
+
˄
−ₒ
ʔ
k
,
ʔ
k
ʔ
k
=
ʔ
k
+
ʔ
0
=
≈
s
ʘ
,
s
using Proposition 6.2 there exist some
ʘ
0
and
ʘ
0
ʘ
0
+
ʘ
0
such that
ʘ
=
,
˄
−ₒ
ʔ
0
≈
s
)
†
ʘ
0
≈
s
)
†
≈
s
)
†
and
ʔ
0
ʘ
0
. Since
ʔ
0
ʔ
1
and
ʔ
0
ʘ
0
,by
(
(
(
≈
s
)
†
ʘ
1
.
Repeating the above procedure gives us inductively a series
ʘ
k
,
ʘ
k
Proposition
7.1
we have
ʘ
0
⃒
ʘ
1
with
ʔ
1
(
,
ʘ
k
of sub-
≈
s
)
†
ʘ
k
ʘ
k
distributions, for
k
≥
0, such that
ʘ
0
=
ʘ
,
ʔ
k
(
ʘ
k
,
ʘ
k
=
+
,
=
i
ʘ
i
˄
⃒
ʔ
k
≈
s
)
†
ʘ
k
,
ʔ
k
≈
s
)
†
ʘ
k
and
ʘ
k
ʘ
k
. We define
ʘ
(
(
:
.
By Additivity (Remark 6.2), we have
ʔ
≈
s
)
†
ʘ
. It remains to be shown that
(
ʘ
.
For that final step, since the set
ʘ
⃒
ʘ
|
ʘ
}
{
ʘ
⃒
is closed by Lemma 6.17,
ʘ
i
for each
i
and with the
ʘ
i
's being arbitrarily close to
ʘ
. Induction establishes for each
i
the
weak transition
ʘ
ʘ
by exhibiting a sequence
ʘ
i
we can establish
ʘ
⃒
with
ʘ
⃒
+
k
≤
i
ʘ
k
ʘ
i
(
ʘ
i
). Since
ʔ
is a full distribution (cf.
⃒
:
=
ʔ
|=
ʔ
i
|=
Definition
7.2
), whose mass is 1, i.e.
|
1, we must have lim
i
ₒ∞
|
0.
≈
s
)
†
It is easy to see that for any two subdistributions
ʓ
1
,
ʓ
2
if
ʓ
1
(
ʓ
2
then they
have the same mass. Therefore, it follows from the condition
ʔ
i
≈
s
)
†
ʘ
i
(
that
ʘ
i
0. Thus these
ʘ
i
's form the sequence we needed.
lim
i
ₒ∞
|
|=
ʱ
⃒
≈
s
)
†
ʘ and ʔ
ʔ
. Then there
Corollary 7.1
In a finitary pLTS, suppose ʔ
(
ʱ
⃒
≈
s
)
†
ʘ
.
is some ʘ
with ʘ
ʘ
and ʔ
(
Proof
Given the two previous results, this is fairly straightforward. Suppose that
ʱ
⃒
≈
s
)
†
ʘ
.If
ʱ
is
˄
then the required
ʘ
follows by an application
of Theorem
7.2
, since the relation
ʔ
and
ʔ
(
ʔ
˄
⃒
is actually defined to be
⃒
.
ʱ
−ₒ
ʔ
.An
Otherwise, by definition we know
ʔ
⃒
ʔ
1
,
ʔ
1
ʔ
2
and
ʔ
2
⃒
≈
s
)
†
application of Theorem
7.2
gives a
ʘ
1
such that
ʘ
⃒
ʘ
1
and
ʔ
1
(
ʘ
1
.An
ʱ
⃒
≈
s
)
†
application of Proposition
7.1
gives a
ʘ
2
such that
ʘ
1
ʘ
2
and
ʔ
2
(
ʘ
2
.
ʘ
such that
ʔ
(
≈
s
)
†
ʘ
.
Finally, another application of Theorem
7.2
gives
ʘ
2
⃒
The result now follows since the transitivity of
⃒
, Theorem 6.6, gives the
ʱ
⃒
ʘ
.
transition
ʘ
≈
s
)
†
ʘ implies ʔ
Theorem 7.3
In a finitary pLTS, ʔ
(
≈
ʘ.
≈
s
)
†
≈
s
)
†
)
−
1
. We show that
Proof
Let
R
denote the relation (
∪
((
R
is a bisimulation
relation, from which the result follows.
Suppose that
ʔ
R
ʘ
. There are two possibilities:
Search WWH ::
Custom Search