Information Technology Reference
In-Depth Information
6.7.1
Inductive Characterisation
S
FS
The relation
of Definition
6.21
is given coinductively; it is the largest fixed point
of an equation
R
=
F
(
R
). An alternative approach, therefore, is to use that
F
(
−
)to
S
FS
define
as a limit of approximants:
k
Definition 6.25
For every
k
≥
0 we define the relations
FS
ↆ
S
×
D
sub
(
S
)as
follows:
0
FS
(i)
:
=
S
×
D
sub
(
S
)
k
+
1
k
(ii)
:
=
F
(
FS
)
FS
=
k
=
0
FS
k
Finally, let
FS
.
A simple inductive argument ensures that
:
S
FS
k
ↆ
FS
, for every
k
≥
0, and
FS
ↆ
FS
. The converse is, however, not true in general.
A (nonprobabilistic) example is well-known in the literature; it makes essential
use of an infinite branching. Let
P
be the process
rec
x.a.x
and
s
a state in a pLTS
that starts by making an infinitary choice, namely for each
k
S
therefore that
1 it has the option
to perform a sequence of
a
actions with length
k
in succession and then deadlock.
This can be described by the infinitary CSP expression
≥
k
=
1
a
k
. Then [[
P
]]
FS
s
,
a
−ₒ
because the move [[
P
]]
[[
P
]] cannot be matched by
s
. However, an easy inductive
FS
s
.
Once we restrict our nonprobabilistic systems to be finitely branching, however,
a simple counting argument will show that
k
FS
a
k
argument shows that [[
P
]]
for every
k
, and therefore that [[
P
]]
FS
; see [
11
, Theo-
rem 2.1] for the argument applied to bisimulation equivalence. In the probabilistic
case, we restrict to both finite-state
and
finitely branching systems, and the effect
of that is captured by topological
compactness
. Finiteness is lost unavoidably when
we remember that, for example, the process
a.
0
S
FS
coincides with
b.
0
can move via
⃒
to a dis-
tribution [[
a.
0
]]
p
↕
[0, 1].
Nevertheless, those uncountably many weak transitions can be generated by arbitrary
interpolation of two transitions [[
a.
0
[[
b.
0
]] for any of the uncountably many probabilities
p
∈
˄
−ₒ
˄
−ₒ
b.
0
]]
[[
a.
0
]] a n d [[
a.
0
b.
0
]]
[[
b.
0
]] ,
and that is the key structural property that compactness captures.
Because compactness follows from closure and boundedness, we approach this
topic via closure.
Note that the metric spaces (
D
sub
(
S
),
d
1
) with
d
1
(
ʔ
,
ʘ
)
=
max
s
∈
S
|
ʔ
(
s
)
−
ʘ
(
s
)
|
and (
S
ₒ
D
sub
(
S
),
d
2
) with
d
2
(
f
,
g
)
=
max
s
∈
S
d
1
(
f
(
s
),
g
(
s
)) are complete. Let
X
be a subset of either
D
sub
(
S
)or
S
ₒ
D
sub
(
S
). Clearly,
X
is bounded. So if
X
is
closed, it is also compact.
Definition 6.26
A relation
R
ↆ
S
×
D
sub
(
S
) is said to be
closed
if for every
s
∈
S
the set
s
is closed.
Two examples of closed relations are
·
R
={
ʔ
|
s
R
ʔ
}
a
⃒
⃒
and
for any action
a
, as shown by
Lemma
6.17
and Corollary
6.6
.
Our next step is to show that each of the relations
FS
are closed. This requires
some results to be first established.
Search WWH ::
Custom Search