Information Technology Reference
In-Depth Information
to distinguish processes that are not bisimilar. For this purpose we use the pLTS
determined by the language
rpCSP
. For the remainder of this section we focus on
this particular pLTS.
We will eventually establish the completeness by showing that
≈
rbc
is a bisim-
ulation, but this requires that we first develop a few auxiliary properties of
≈
rbc
in
this setting. The technique used normally involves examining the barbs of processes
in certain contexts; the following lemma gives extra power to this technique. If an
action name
c
does not appear in the processes under consideration, we say
c
is
fresh
.
ʔ
≈
rbc
(
ʘ
ʘ
where p>
0
and
Lemma 7.4
In
rpCSP
suppose
(
ʔ
|
c.
0
)
p
↕
|
c.
0
)
p
↕
c is a fresh action name. Then ʔ
≈
rbc
ʘ.
Proof
Consider the relation
(
ʔ
|
c.
0
)
p
↕
ʔ
≈
rbc
(
ʘ
|
c.
0
)
p
↕
ʘ
for some
ʔ
,
ʘ
and fresh
c
}
R
={
(
ʔ
,
ʘ
)
|
We show that
R
ↆ≈
rbc
, by showing that
R
satisfies the three defining properties
of
≈
rbc
.
(1)
R
is compositional. Suppose
ʔ
R
ʘ
;wehavetoshow(
ʔ
|
Φ
)
R
(
ʘ
|
Φ
), for any
ʘ
there are some
ʔ
,
ʘ
and fresh
c
such that
distribution
Φ
. Since
ʔ
R
ʔ
,
ʓ
ʘ
.
ʛ
≈
rbc
ʓ
where
ʛ
=
(
ʔ
|
c.
0
)
p
↕
=
(
ʘ
|
c.
0
)
p
↕
(7.3)
Since
≈
rbc
is compositional, we have (
ʛ
|
Φ
)
≈
rbc
(
ʓ
|
Φ
). Therefore, it fol-
(
ʔ
|
(
ʘ
|
lows that (
ʔ
|
Φ
|
c.
0
)
p
↕
Φ
)
≈
rbc
(
ʘ
|
Φ
|
c.
0
)
p
↕
Φ
),
which means,
by
definition, that (
ʔ
|
Φ
)
R
(
ʘ
|
Φ
).
⇓
≥
q
(2)
R
is barb-preserving. Suppose
ʔ
for some action
a
and probability
q
, where
a
ʘ
. Again we may assume (
7.3
) above. Consider the testing process
a.c.b.
0
,
where
b
is fresh. Since
R
ʔ
≈
rbc
is compositional, we have
(
ʛ
|
a.c.b.
0
)
≈
rbc
(
ʓ
|
a.c.b.
0
)
.
⇓
≥
p
b
. Since
c
is fresh
for
ʘ
, the latter has no potential to enable the action
c
, and thus
ʘ
|
⇓
≥
pq
b
|
a.c.b.
0
)
|
a.c.b.
0
)
Note that (
ʛ
, which implies (
ʓ
a.c.b.
0
is
not able to fire the action
b
. Therefore, the action is triggered by
ʘ
and it must
be the case that (
ʘ
|
c.
0
⇓
≥
q
b
, which implies
ʘ
⇓
≥
q
|
a.c.b.
0
)
.
a
˄
⃒
ʔ
for some distribution
ʔ
.
Let
ʓ
and
ʛ
be determined as in (
7.3
) above. Then
ʛ
(3)
R
is reduction-closed. Suppose
ʔ
R
ʘ
and
ʔ
˄
⃒
(
ʔ
|
ʔ
. Since
c.
0
)
p
↕
≈
rbc
ʓ
, there is some
ʓ
with
ʓ
ʓ
and (
ʔ
|
ʔ
≈
rbc
ʓ
. In other
ʛ
⃒
c.
0
)
p
↕
˄
⃒
words, there are some
ʘ
,
ʘ
such that
ʓ
≡
(
ʘ
|
ʘ
with
ʘ
ʘ
c.
0
)
p
↕
˄
⃒
and
ʘ
ʘ
. Thus (
ʔ
|
ʔ
≈
rbc
(
ʘ
|
ʘ
. Thus by definition
c.
0
)
p
↕
c.
0
)
p
↕
ʔ
R
ʘ
.
In
rpCSP
,if
(
i
∈
I
p
i
·
≈
rbc
ʘ with
i
∈
I
p
i
=
Proposition 7.4
ʔ
i
)
1
, then there
⃒
i
∈
I
p
i
·
ʘ
i
and ʔ
i
≈
rbc
ʘ
i
for each i
∈
I .
˄
are some ʘ
i
such that ʘ
Search WWH ::
Custom Search