Information Technology Reference
In-Depth Information
Fig. 5.5
Action prefix does not distribute over probabilistic choice
such that
min
(
A
(
T
,
P
))
=
min
(
A
(
T
,
Q
)). In case
max
(
A
(
T
,
P
))
> max
(
A
(
T
,
Q
))
we find in particular that
P
pmay
Q
, and in case
min
(
A
(
T
,
P
))
> min
(
A
(
T
,
Q
)) we
obtain
P
pmust
Q
.
Example 5.3
a.P
p
↕
a.Q
is unsound.
Consider the example in Fig.
5.5
.In
R
1
the probabilistic choice between
b
and
c
is
taken after the action
a
, while in
R
2
the choice is made before the action has happened.
These processes can be distinguished by the nondeterministic test
T
The axiom
a.
(
P
p
↕
Q
)
=
a.c.ˉ
.
First consider running this test on
R
1
. There is an immediate choice made by the test,
effectively running either the test
a.b.ˉ
on
R
1
or the test
a.c.ˉ
; in fact the effect of
running either test is exactly the same. Consider
a.b.ˉ
. When run on
R
1
the
a
action
immediately happens, and there is a probabilistic choice between running
b.ˉ
on
either
b
or
c
, giving as possible results
=
a.b.ˉ
{
}
{
}
1
or
0
; combining these according to the
1
1
1
definition of the function
V
f
(__) we get
2
·{
0
}+
2
·{
1
}=
2
. Since running the test
(
T
,
R
1
) turns out to be the same set
2
.
Now consider running the test
T
on
R
2
. Because
R
2
, and hence also
T
a.c.ˉ
has the same effect,
A
|
Act
R
2
,
V
f
(__), the
test must first be applied to the probabilistic components,
a.b
and
a.c
, respectively,
and the results subsequently combined probabilistically. When the test is run on
a.b
, immediately a nondeterministic choice is made in the test, to run either
a.b.ˉ
starts with a probabilistic choice, due to the definition of the function
Search WWH ::
Custom Search