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