Information Technology Reference
In-Depth Information
k
FS
Proposition 6.13
In a finitary pLTS, for every k
≥
0
the relation
is closed and
convex.
k
FS
Proof
By induction on
k
.For
k
=
0 it is obvious. So let us assume that
is
closed and convex. We have to show that
(
k
+
1)
·
s
is closed and convex, for every state
s
(6.24)
FS
(
k
+
1)
FS
If
s
⃒
ʵ
, then this follows from the corollary above, since in this case
s
·
coincides with
{
ʔ
|
ʔ
⃒
ʵ
}
. So let us assume that this is not the case.
A
, which we know by the corollary
above to be closed and is obviously convex. Also for every
ʘ
and
ʱ
we let
For every
A
ↆ
Act
let
R
A
={
ʔ
|
ʔ
⃒
−ₒ}
ʱ
⃒
k
FS
)
†
)
G
ʘ
,
ʱ
:
={
ʔ
|
(
ʔ
·
)
∩
(
ʘ
·
(
=∅}
.
ʱ
⃒
By Corollary
6.7
, the relation
is lifted from a closed convex relation. By Corol-
FS
)
†
is also
closed. So we can appeal to Lemma
6.35
and conclude that each
G
ʘ
,
ʱ
is closed.
By Definition
6.2
(2), it is also easy to see that
G
ʘ
,
ʱ
is convex. But it follows that
s
k
FS
k
lary
6.10
, the assumption that
is closed and convex implies that (
(
k
+
1)
FS
·
is also closed and convex as it can be written as
ʱ
−ₒ
A
∩{
R
A
|
s
−ₒ}∩∩{
G
ʘ
,
ʱ
|
s
ʘ
}
Before the main result of this section we need one more technical lemma.
k
Lemma 6.36
Let S be a finite set of states. Suppose
R
ↆ
S
×
D
sub
(
S
)
is a
(
k
+
1)
k
. Then
sequence of closed convex relations such that
R
ↆ
R
∩
k
=
0
k
)
†
∩
k
=
0
R
k
)
†
.
(
R
ↆ
(
k
)
†
ʘ
for every
k
R
∞
denote (
∩
k
=
0
R
k
) and suppose
ʔ
(
Proof
Let
R
≥
0. We have
R
∞
)
†
ʘ
.
to show that
ʔ
(
,which is easily seen to be a closed
set. For each
k
, we know from Lemma
6.34
that the set
Ch
(
Let
G
={
f
:
S
ₒ
D
sub
(
S
)
|
ʘ
=
Exp
ʔ
(
f
)
}
k
) is closed. Finally,
R
k
)
†
ʘ
, Proposi-
consider the collection of closed sets
H
k
k
)
=
Ch
(
R
∩
G
; since
ʔ
(
R
tion
6.1
assures us that all of these are non-empty. Also
H
(
k
+
1)
H
k
and, therefore,
ↆ
∩
k
=
0
H
k
is also nonempty.
Let
f
be an arbitrary element of this intersection. For any state
s
by the finite-intersection property (Theorem 2.4)
R
∞
) and
∈
dom
(
R
∞
)
k
)wehave
s
k
f
(
s
), that is
s
R
∞
f
(
s
). So
for every
k
≥
0, since
dom
(
ↆ
dom
(
R
R
R
∞
,
f
R
∞
). From convexity and Proposition
6.1
,
f
is a choice function for
∈
Ch
(
R
∞
)
†
it follows that
ʔ
(
Exp
ʔ
(
f
). But from the definition of the
G
we know that
ʘ
=
Exp
ʔ
(
f
), and the required result follows.
FS
ʘ if and only if s
FS
ʘ.
Theorem 6.14
In a finitary pLTS, s
FS
ↆ
FS
Proof
Since
it is sufficient to show the opposite inclusion, which by
FS
is a failure simulation, viz. if
FS
ↆ
FS
). Suppose
s
FS
ʘ
,
definition holds if
F
(
Search WWH ::
Custom Search