Information Technology Reference
In-Depth Information
Suppose that
P
F
Q
. By Lemma
5.11
we have [[
Q
]]
Proof
|=
˕
[[
Q
]]
and therefore
[[
P
]]
|=
˕
[[
Q
]]
. Lemma
5.12
gives
P
FS
Q
.
Now assume that
P
L
Q
.Wehave [
P
]]
|=
ˈ
[[
P
]]
, hence [[
Q
]]
|=
ˈ
[[
P
]]
, and thus
P
S
Q
.
5.7
Characteristic Tests
Our final step towards Theorem
5.4
is taken in this section, where we show that every
modal formula
˕
can be characterised by a vector-based test
T
˕
with the property
that any
pCSP
process satisfies
˕
just when it passes the test
T
˕
.
Lemma 5.13
For every ˕
∈
F
there exists a pair
(
T
˕
,
v
˕
)
with T
˕
an ʩ test and
[0, 1]
ʩ
, such that
v
˕
∈
|=
∃
∈
A
≤
ʔ
˕
iff
o
(
T
˕
,
ʔ
):
o
v
˕
(5.27)
for all ʔ
∈
D
(
sCSP
)
, and in case ˕
∈
L
we also have
ʔ
|=
˕
iff
∃
o
∈
A
(
T
˕
,
ʔ
):
o
≥
v
˕
.
(5.28)
T
˕
is called a
characteristic test
of
˕
and
v
˕
its
target value
.
Proof
First of all note that if a pair (
T
˕
,
v
˕
) satisfies the requirements above, then any
pair obtained from (
T
˕
,
v
˕
) by bijectively renaming the elements of
ʩ
also satisfies
these requirements. Hence a characteristic test can always be chosen in such a way
that there is a success action
ˉ
ʩ
that does not occur in (the finite)
T
˕
. Moreover,
any countable collection of characteristic tests can be assumed to be
ʩ
-disjoint,
meaning that no
ˉ
∈
ʩ
occurs in two different elements of the collection.
The required characteristic tests and target values are obtained as follows.
∈
ˉ
.
•
Let
˕
=
. Take
T
˕
:
=
ˉ
for some
ˉ
∈
ʩ
, and
v
˕
:
=
•
Let
˕
=
ref
(
X
) with
X
ↆ
Act
. Take
T
˕
:
=
a
∈
X
a.ˉ
for some
ˉ
∈
ʩ
, and
0
.
v
˕
:
=
•
Let
˕
=
a
ˈ
. By induction,
ˈ
has a characteristic test
T
ˈ
with target value
v
ˈ
.
Take
T
˕
:
=
˄.ˉ
a.T
ˈ
where
ˉ
∈
ʩ
does not occur in
T
ˈ
, and
v
˕
:
=
v
ˈ
.
•
Let
˕
˕
2
. Choose an
ʩ
-disjoint pair (
T
i
,
v
i
) of characteristic tests
T
i
with
target values
v
i
, for
i
=
˕
1
∧
=
1, 2. Furthermore, let
p
∈
(0, 1] be chosen arbitrarily,
and take
T
˕
:
=
T
1
p
↕
T
2
and
v
˕
:
=
p
·
v
1
+
(1
−
p
)
·
v
2
.
•
Let
˕
˕
1
p
↕
˕
2
. Again choose an
ʩ
-disjoint pair (
T
i
,
v
i
) of characteristic tests
T
i
with target values
v
i
,
i
=
1, 2, this time ensuring that there are two distinct
success actions
ˉ
1
,
ˉ
2
that do not occur in any of these tests. Let
T
i
=
:
=
T
i
2
↕
ˉ
i
ˉ
i
. Note that for
i
1
1
2
and
v
i
:
1, 2 we have that
T
i
is also a characteristic
test of
˕
i
with target value
v
i
. Take
T
˕
:
=
2
v
i
+
=
=
T
1
T
2
=
·
v
1
+
−
·
v
2
.
and
v
˕
:
p
(1
p
)
Note that
v
˕
(
ˉ
)
=
0 whenever
ˉ
∈
ʩ
does not occur in
T
˕
. By induction on
˕
we
now check (
5.27
) above.
Search WWH ::
Custom Search