Information Technology Reference
In-Depth Information
assign to each node a number to indicate its level in the tree. Let
T
=
i
∈
I
T
i
.We
prove the following two claims
(a) If
s
is a state-based process and
o
∈
A
(
T
,
s
), then there are some
{
q
i
}
i
∈
I
with
i
∈
I
q
i
=
⃒
i
∈
I
q
i
·
=
i
∈
I
q
i
o
i
, and
o
i
∈
A
˄
1 such that
s
ʔ
i
,
o
(
T
i
,
ʔ
i
).
{
q
i
}
i
∈
I
with
i
∈
I
q
i
=
(b) If
ʔ
∈
D
(
sCSP
) and
o
∈
A
(
T
,
ʔ
), then there are some
1
⃒
i
∈
I
q
i
·
=
i
∈
I
q
i
o
i
, and
o
i
∈
A
˄
(
T
i
,
ʔ
i
)
by simultaneous induction on the order mentioned above, applied to
s
and
ʔ
.
such that
ʔ
ʔ
i
,
o
(a) We have two subcases depending on whether
s
can make an initial
˄
move or
not.
• f
s
cannot make a
˄
move, that is
s
˄
−ₒ
, then the only possible moves from
T
|
Act
s
are
˄
moves originating in
T
;
T
has no non-
˄
moves, and any non-
˄
moves that might be possible for
s
on its own are inhibited by the alphabet
Act
of the composition. Suppose
o
∈
A
(
T
,
s
). Then there are som
e
{
q
i
}
i
∈
I
with
i
∈
I
q
i
=
=
i
∈
I
q
i
o
i
and
o
i
∈
A
1 such that
o
(
T
i
,
s
)
=
A
(
T
i
,
s
). Obviously
⃒
i
∈
I
q
i
·
˄
s
.
• f
s
can make one or more
˄
moves, then we have
s
˄
we also have [[
s
]]
−ₒ
ʔ
j
for
j
∈
J
,
where without loss of generality
J
can be assumed to be a nonempty finite set
disjoint from
I
, the index set for
T
. The possible first moves for
T
|
Act
s
are
˄
moves either of
T
or of
s
, because
T
cannot make initial non-
˄
moves and that
prevents a proper synchronisation from occurring on the first step. Suppose
that
o
p
k
}
k
∈
I
∪
J
with
k
∈
I
∪
J
p
k
=
∈
A
(
T
,
s
). Then there are some
{
1 and
p
k
o
k
o
=
(5.14)
k
∈
I
∪
J
o
i
∈
A
(
T
i
,
s
)
for all
i
∈
I
(5.15)
o
j
∈
A
(
T
,
ʔ
j
)
for all
j
∈
J
.
(5.16)
For each
j
∈
J
, we know by the induction hypothesis that
˄
⃒
ʔ
j
ʔ
ji
p
ji
·
(5.17)
i
∈
I
o
j
=
p
ji
o
ji
(5.18)
i
∈
I
o
ji
∈
A
(
T
i
,
ʔ
ji
)
(5.19)
p
ji
}
i
∈
I
with
i
∈
I
p
ji
=
for some
{
1. Let
q
i
=
p
i
+
p
j
p
ji
j
∈
J
1
q
i
(
p
i
·
ʔ
ji
)
ʔ
i
=
s
+
p
j
p
ji
·
Search WWH ::
Custom Search