Information Technology Reference
In-Depth Information
In case
P
∈
sCSP
, a statement
P
S
Q
cannot always be established by a simulation
†
R
such that [[
P
]]
R
[[
Q
]] .
Example 5.14
Compare the processes
P
=
a
2
↕
b
and
P
P
. Note that [[
P
]] is the
1
1
distribution
2
a
+
2
b
, whereas [[
P
P
]] is the point distribution
P
P
. The relation
R
given by
(
2
a
+
1
(
P
P
)
R
2
b
)
a
R
a
b
R
b
0
R
0
˄
−ₒ
(
2
a
1
is a simulation, because the
˄
step
P
P
+
2
b
) can be matched by the idle
˄
⃒
transition (
2
a
1
2
b
)
(
2
a
1
2
b
), and we have (
2
a
1
2
b
)
(
2
a
1
2
b
). Thus
†
+
+
+
R
+
s
)
†
[[
P
]], and therefore
P
P
S
P
.
This
t
ype
o
f rea
soning
does not apply to the oth
er dire
ction. A
ny sim
ulation
s
(
2
a
+
1
(
P
P
)
2
b
)
=
[[
P
]], hence [[
P
P
]] (
R
with (
2
a
1
†
P
+
2
b
)
R
P
would have to satisfy
a
R
P
P
an
d
b
R
P
P
. However,
a
−ₒ
the move
a
0
cannot
be mat
ched by the p
ro
cess
P
P
, as the only transition
˄
−ₒ
1
2
b
), and only half of that distribution
can match the
a
move. As a consequence, no such simulation exists, and we find that
[[
P
]] (
(
2
a
the latter process can do is
P
P
+
s
)
†
[[
P
S
P
P
]] does not hold. Nevertheless, we still have
P
P
. Here, the
˄
⃒
˄
⃒
transition
from Definition
5.5
comes to the rescue. As [[
P
P
]]
[[
P
]] and
s
)
†
[[
P
]], we obtain
P
S
P
P
.
Example 5.15
[[
P
]] (
Let
P
=
a
2
↕
b
and
Q
=
P
P
. We can establish that
P
S
Q
s
)
†
[[
Q
]] that comes from the following observations:
because [[
P
]] (
1
2
a
1
2
b
1. [[
P
]]
=
+
1
2
(
2
a
1
1
2
(
2
a
1
2. [[
Q
]]
=
a
+
2
a
b
)
+
b
+
2
b
b
)
s
(
2
a
1
2
a
3.
a
a
+
b
)
s
(
2
a
1
4.
b
b
+
2
b
b
).
This kind of reasoning does not apply to
FS
. For example, we have
FS
(
1
1
2
a
a
2
a
a
+
b
)
because the state on the left hand side can refuse to do action
b
while the distribution
on the right hand side cannot. Indeed, it holds that
Q
FS
P
.
Because of the asymmetric use of distributions in the definition of simulations
it is not immediately obvious that
S
and
FS
are actually preorders (reflexive and
transitive relations) and hence,
FS
are equivalence relations. In order to
show this, we first need to establish some properties of
S
and
s
and
FS
.
Suppose
i
∈
I
p
i
=
ʱ
⃒
Lemma 5.4
1
and ʔ
i
Φ
i
for each i
∈
I , with I a finite
index set. Then
ʱ
⃒
p
i
·
ʔ
i
p
i
·
Φ
i
i
∈
I
i
∈
I
Search WWH ::
Custom Search