Information Technology Reference
In-Depth Information
empty. Let
term
be a fresh event modeling the possibility to synchronize before
successful termination.
C
(
X
)=
s
?
x
→
C
(
X
[[
x
]])
sh
?
x
→
C
(
X
[[
x
]])
e
?
x
→
C
(
X
∪
[[
x
]] )
eh
?
x
→
C
(
X
∪
[[
x
]] )
term
→
SKIP
(1)
As outlined in the previous section the process
C
(
X
) is to be put in parallel
with the transformed process. We define
S
Con
=
to be the
alphabet on which the transformed process
T
(
P
) and the controller synchronize.
Now because
term
{|
s
,
sh
,
e
,
eh
,
term
|}
Σ
T
(
P
)
, the controller
C
cannot terminate
while
T
(
P
) is still active. Since we aim at establishing traces-equality, the par-
allel composition must be able to terminate if
P
terminates successfully. Thus,
because of the
Ω
semantics (see [9]) and distributed termination of parallel com-
position,
T
(
P
) is sequentially composed with the process
term
∈
S
Con
but
term
/
∈
SKIP
in the
following construction. The construction starts by transforming an input process
P
to
T
(
P
) and combining the result with the control process (1) to achieve the
result
Con
(
P
) (standing for
controlled
).
→
Con
(
P
)=(
T
(
P
);
term
→
SKIP
)
|
S
Con
|
C
([[ ]])
(2)
The events
s
.
x
are renamed to
x
,andtheeventsin
H
Hr
=
{|
sh
,
e
,
eh
,
term
|}
are
hidden using
Hr
(standing for
hidden
and
renamed
)
Hr
(
P
)=
P
\
H
Hr
[
s
.
x
←
x
|
x
∈
Σ
P
]
(3)
resulting in a process
Ext
(
P
)=
Hr
(
Con
(
P
))
(4)
(the
extension
of
P
) that we think of as simulating
P
but enabling it to benefit
from true concurrency. While concurrency cannot be distinguished from choice
in the interleaved semantic models
T
F
FD
, the transformation
T
allows
them to be distinguished because start and end events of two events
x
and
y
mayinterleaveonlyif
x
and
y
are concurrent in
P
. Thus, using the construction
given above, possible concurrency is captured by the bag
X
maintained by the
controller process
C
(
X
). Whenever the size of the bag exceeds one, it holds the
names of events that are performed concurrently at that point.
To ensure that a process is not 'corrupted' by
Ext
we must show that it is a
fixed point of
Ext
in the traces semantics:
,
and
Theorem 1.
For each process P of the form given above,
P
=
T
Ext
(
P
)
.
Search WWH ::
Custom Search