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