Information Technology Reference
In-Depth Information
Proof
Similar to the proof of Proposition 3.1.
ʱ
−ₒ ↆ
We apply this definition to the action relations
sCSP
×
D
(
sCSP
)inthe
operational semantics of
pCSP
, and obtain lifted relations between
D
(
sCSP
) and
(
sCSP
), which to ease the notation we write as
ʔ
ʱ
D
−ₒ
ʘ
; then, using
pCSP
terms
to represent distributions, a simple instance of a transition between distributions is
given by
a
−ₒ
(
a.b
a.c
)
2
↕
a.d
b
2
↕
d.
Note that we also have
a
−ₒ
(
a.b
a.c
)
2
↕
a.d
(
b
2
↕
c
)
2
↕
d
(5.1)
a.c
)
2
↕
because, viewed as a distribution, the term (
a.b
a.d
may be rewritten as
((
a.b
a.c
)
2
↕
(
a.b
a.c
))
2
↕
a.d
representing the sum of point distributions
1
4
·
1
4
·
1
2
·
(
a.b
a.c
)
+
(
a.b
a.c
)
+
a.d
from which the move (
5.1
) can easily be derived using the three moves from states
a
−ₒ
a
−ₒ
a
−ₒ
a.b
a.c
b
a.b
a.c
c
a.d
d.
The lifting construction can also be used to define the concept of a
partial
internal
move between distributions, one where part of the distribution does an internal move
and the remainder remains unchanged. Write
s
˄
−ₒ
ˆ
˄
−ₒ
s
.
This relation between states and distributions can be lifted to one between distri-
butions and distributions, and again for notational convenience we use
ʔ
1
ʔ
if either
s
ʔ
or
ʔ
=
˄
−ₒ
ʔ
2
to denote the lifted relation. As an example, again using process terms to denote
distributions, we have
˄
−ₒ
(
a
b
)
2
↕
(
a
c
)
a
2
↕
(
a
b
2
↕
c
)
.
This follows because as a distribution (
a
b
)
2
↕
(
a
c
) may be written as
1
1
1
1
4
·
(
a
b
)
+
4
·
(
a
b
)
+
4
·
(
a
c
)
+
4
·
(
a
c
)
and we have the four moves from states to distributions:
˄
−ₒ
˄
−ₒ
(
a
b
)
a
(
a
b
)
(
a
b
)
˄
−ₒ
a
˄
−ₒ
c.
(
a
c
)
(
a
c
)
Search WWH ::
Custom Search