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