Information Technology Reference
In-Depth Information
Fig. 5.3
Example of testing
to the process
b
d
. We see that 25 % of the time the test is unsuccessful, in
that it does not reach a state where
ˉ
is possible, and 75 % of the time it
may
be
successful, depending on how the now internal choice between the actions
b
and
c
is resolved, but it is not the case that it
must
be successful.
[[
T
c
|
Act
P
]] is representable as a finite graph that encodes all possible interactions of
the test
T
with the process
P
. It only contains the actions
˄
and
ˉ
. Each occurrence
of
˄
represents a nondeterministic choice, either in
T
or
P
themselves, or as a
nondeterministic response by
P
to a request from
T
, while the distributions represent
the resolution of underlying probabilities in
T
and
P
. We use the structure [[
T
|
Act
P
]]
to define
(
T
,
P
), a nonempty subset of [0, 1] representing the set of probabilities
that applying
T
to
P
will be a success.
A
ₒ
P
+
([0, 1]), which when applied
to any state in
sCSP
returns a finite subset of [0, 1]; it is extended to the type
D
V
f
:
sCSP
Definition 5.1
We define a function
(
sCSP
)
ₒ
P
+
([0, 1]) via the convention
V
f
(
ʔ
):
=
Exp
ʔ
V
f
(cf. Sect. 4.2).
⊧
⊨
ˉ
−ₒ
{
1
}
if
s
,
{ V
f
(
ʔ
)
˄
−ₒ
ˉ
−ₒ
˄
−ₒ
V
f
(
s
)
=
|
s
ʔ
}
if
s
,
s
,
⊩
{
}
0
otherwise
We will tend to write the expected value of
V
f
explicitly and use the convenient
notation
V
f
(
ʔ
)
=
ʔ
(
s
1
)
· V
f
(
s
1
)
+
...
+
ʔ
(
s
n
)
· V
f
(
s
n
)
where
ʔ
={
s
1
,
...s
n
}
. Note that
V
f
(__) is indeed a well-defined function, because
the pLTS
is finitely branching and well-founded.
For example consider the transition systems in Fig.
5.4
, where for reference we
have labelled the nodes. Then
sCSP
,
Act
˄
,
ₒ
V
f
(
s
1
)
={
1, 0
}
while
V
f
(
s
2
)
={
1
}
, and therefore
Search WWH ::
Custom Search