Information Technology Reference
In-Depth Information
k
which means that
s
FS
ʘ
for every
k
≥
0. According to Definition
6.21
, in order to
FS
)
ʘ
, we have to establish three properties, the first and last of which
are trivial (for they are independent on the argument of
F
).
So suppose
s
show
s
F
(
ʱ
−ₒ
ʱ
⃒
ʔ
. We have to show that
ʘ
ʘ
for some
ʘ
such that
ʔ
(
FS
)
†
ʘ
.
For every
k
ʱ
⃒
FS
)
†
ʘ
k
.
≥
0, there exists some
ʘ
k
such that
ʘ
ʘ
k
and
ʔ
(
Now construct the sets
ʱ
⃒
D
k
ʘ
|
ʘ
and
ʔ
(
k
FS
)
†
ʘ
}
={
ʘ
.
From Lemma
6.17
and Proposition
6.13
, we know that these are closed. They are also
nonempty and
D
k
+
1
D
k
. So by the finite-intersection property the set
k
=
0
D
k
ↆ
is
ʱ
⃒
nonempty. For any
ʘ
in it, we know
ʘ
ʘ
and
ʔ
(
FS
)
†
ʘ
for every
k
≥
0. By
FS
are all closed and convex. Therefore, Lemma
6.36
may be applied to them, which enables us to conclude
ʔ
(
Proposition
6.13
, the relations
FS
)
†
ʘ
.
For Theorem
6.14
to hold, it is crucial that the pLTS is assumed to be finitary.
Example 6.25
Consider an infinitely branching pLTS with four states
s
,
t
,
u
,
v
,
0
and the transitions are
a
−ₒ
•
s
0
2
↕
s
a
−ₒ
a
−ₒ
•
t
0
,
t
t
a
−ₒ
•
u
u
˄
−ₒ
•
v
u
p
↕
t
for all
p
∈
(0, 1).
This is a finite-state b
ut
not finitely branching system, due to t
h
e infinite branch in
v
. We have that
s
k
FS
S
FS
v
for all
k
≥
0 but we do not have
s
v
.
S
FS
v
does not hold because
s
will eventually deadlock
with probability 1, whereas a
f
raction of
v
will go to
u
and never deadlock.
We now show that
s
We first observe that
s
F
S
v
fo
r
all
k
≥
0. For any
k
we start the simulation by
˄
−ₒ
choosing the move
v
(
u
2
k
↕
t
). By induction on
k
we show that
k
FS
s
(
u
2
k
↕
t
)
.
(6.25)
The base cas
e
k
=
0
is trivial. So suppose we already have (
6.25
). We now show
(
k
+
1)
that
s
(
u
↕
t
). Neither
s
nor
t
nor
u
can diverge or refuse
{
a
}
, so the only
1
FS
2
k
+
1
a
−ₒ
relevant move is the
a
-move. We know that
s
can do the move
s
0
2
↕
s
. This
a
−ₒ
can be matched by (
u
↕
t
)
(
0
2
↕
(
u
2
k
↕
t
)).
1
2
k
+
1
FS
, we also give an inductive characterisation of
Analogously to what we did for
FS
ʔ
if there exists a transition
ʘ
ʘ
match
FS
: For every
k
≥
0 let
ʘ
⃒
such
FS
denote
k
=
0
FS
)
†
ʘ
match
, and let
FS
.
that
ʔ
(
FS
ʔ if and only if ʘ
FS
ʔ.
Corollary 6.12
In a finitary pLTS, ʘ
FS
FS
, for every
k
Proof
0, it is straightforward to prove one direc-
tion:
ʘ
FS
ʔ
implies
ʘ
FS
ʔ
. For the converse,
ʘ
FS
ʔ
means that for every
k
Since
ↆ
≥
Search WWH ::
Custom Search