Information Technology Reference
In-Depth Information
Fig. 5.6 Action prefix does not distribute over internal choice
or a.c.ˉ . With the former we get the result
{
1
}
, with the latter
{
0
}
, so overall, for
running T on a , b , we get the possible results
{
0, 1
}
. The same is true when we run
1
1
0, 2 ,1
it on a.c , and therefore
A
( T , R 2 )
=
2 ·{
0, 1
}+
2 ·{
0, 1
}={
}
.
So we have R 2 pmay R 1 and R 1 pmust R 2 .
Example 5.4
a.Q is unsound.
It is well-known that this axiom is valid in the standard theory of testing, for non-
probabilistic processes. However, consider the processes R 1 and R 2 in Fig. 5.6 , and
note that these processes do not contain any probabilistic choice. But they can be
differentiated by the probabilistic test T
The axiom a. ( P
Q )
=
a.P
c.ˉ ); the details are in Fig. 5.6 .
There is only one possible outcome from applying T to R 2 , the probability
=
a. ( b.ˉ 2
1
2 , be-
cause the nondeterministic choice is made before the probabilistic choice. On the
other hand when T is applied to R 1 there are three possible outcomes, 0,
1
2 and 1, be-
cause effectively the probabilistic choice takes precedence over the nondeterministic
choice. So we have R 1 pmay R 2 and R 2 pmust R 1 .
Example 5.5 The axiom a. ( P
a.Q is unsound.
This axiom is valid in the standard may-testing semantics. However, let us consider
the two processes R 1 =
Q )
=
a.P
a. ( b
c ) and R 2 =
a.b
a.c . By applying the probabilistic
 
Search WWH ::




Custom Search