Information Technology Reference
In-Depth Information
1
test
T
=
a.
(
b.ˉ
2
↕
c.ˉ
), we see that
A
(
T
,
R
1
)
={
1
}
and
A
(
T
,
R
2
)
={
2
}
. Therefore
R
1
pmay
R
2
and
R
2
pmust
R
1
.
Example 5.6
The axiom
P
=
P
P
is unsound.
Let
R
1
and
R
2
denote (
a
2
↕
b
) and (
a
2
↕
b
)
(
a
2
↕
b
), respectively. It is easy
1
2
}
to calculate that
but, because of the way we interpret exter-
nal choice as an operator over distributions of states in a pLTS, it turns out that
[[
R
2
]]
A
(
a.ˉ
,
R
1
)
={
3
=
a
)
2
↕
b
))
2
↕
a
)
2
↕
A
={
4
}
[[((
a
(
a
((
b
(
b
b
))]] and so
(
a.ˉ
,
R
2
)
.
Therefore,
R
2
pmay
R
1
and
R
2
pmust
R
1
.
Example 5.7
The axiom
P
p
↕
(
Q
R
)
=
(
P
p
↕
Q
)
(
P
p
↕
R
) is unsound.
Consider the processes
R
1
=
a
2
↕
(
b
c
) and
R
2
=
(
a
2
↕
b
)
(
a
2
↕
c
), and the test
T
1
=
a.ˉ
(
b.ˉ
2
↕
c.ˉ
). In the best of possible worlds, when we apply
T
1
to
R
1
we obtain probability 1, that is
max
(
1. Informally, this is because
half the time when it is applied to the subprocess
a
of
R
1
, optimistically the subtest
a.ˉ
is actually run. The other half of the time, when it is applied to the subprocess
(
b
A
(
T
1
,
R
1
))
=
c.ˉ
) is actually used. And here
again, optimistically, we obtain probability 1: whenever the test
b.ˉ
is used it might
be applied to the subprocess
b
, while when
c.ˉ
is used it might be applied to
c
.
Formally we have
c
), optimistically the subtest
T
r
=
(
b.ˉ
2
↕
1
1
A
(
T
1
,
R
1
)
=
2
·
A
(
T
1
,
a
)
+
2
·
A
(
T
1
,
b
c
)
1
2
·
=
(
A
(
a.ˉ
,
a
)
∪
A
(
T
r
,
a
))
+
1
2
·
(
A
(
T
1
,
b
)
∪
A
(
T
1
,
c
)
∪
A
(
a.ˉ
,
b
c
)
∪
A
(
T
r
,
b
c
))
1
1
0,
2
}∪{
0,
2
}∪{
0,
2
,1
=
2
·
(
{
1
}∪{
0
}
)
+
2
·
(
{
0
}∪{
}
)
0,
4
,
2
,
4
,1
={
}
However, no matter how optimistic we are when applying
T
1
to
R
2
we can never get
probability 1; the most we can hope for is
3
4
, which might occur when
T
1
is applied
to the subprocess (
a
2
↕
b
). Specifically, when the subprocess
a
is being tested the
subtest
a.ˉ
might be used, giving probability 1, and when the subprocess
b
is being
tested the subtest (
b.ˉ
2
↕
c.ˉ
) might be used, giving probability
1
2
. We leave the
reader to check that formally
0,
4
,
2
,
4
}
A
(
T
1
,
R
2
)
={
from which we can conclude
R
1
pmay
R
2
.
We can also show that
R
2
pmust
R
1
, using the test
T
2
=
(
b.ˉ
c.ˉ
)
(
a.ˉ
3
↕
(
b.ˉ
2
↕
c.ˉ
))
.
Reasoning pessimistically, the worst that can happen when applying
T
2
to
R
1
is that
we get probability 0. Each time the subprocess
a
is tested the worst probability will
occur when the subtest (
b.ˉ
c.ˉ
) is used; this results in probability 0. Similarly,
Search WWH ::
Custom Search