Information Technology Reference
In-Depth Information
ˉ
s
∈
ʔ
k
, that is whenever it marches on, it is not successful,
s
−ₒ
for every
ˉ
∈
ʩ
.
Lemma 6.7
(
Existence of Extreme Derivatives)
(i) For every subdistribution ʔ there exists some (stable) ʔ
such that ʔ
ʔ
.
⃒
ʔ
and ʔ
ʔ
then ʔ
=
ʔ
.
(ii) In a deterministic pLTS, if ʔ
⃒
⃒
Proof
We construct a derivation as in Definition
6.4
of a stable
ʔ
by defining the
components
ʔ
k
,
ʔ
k
and
ʔ
k
using induction on
k
. Let us assume that the subdistribu-
tion
ʔ
k
has been defined; in the base case
k
0 this is simply
ʔ
. The decomposition
of this
ʔ
k
into the components
ʔ
k
and
ʔ
k
is carried out by defining the former to
be precisely those states that must stop, that is, those
s
for which
s
=
˄
−ₒ
. Formally
ʔ
k
is determined by:
⊧
⊨
˄
ʔ
k
(
s
) f
s
−ₒ
ʔ
k
(
s
)
=
⊩
0
otherwise
Then
ʔ
k
is given by the
remainder
of
ʔ
k
, namely those states that can perform a
˄
action:
⊧
⊨
˄
−ₒ
ʔ
k
(
s
) f
s
ʔ
k
(
s
)
=
⊩
0
otherwise
Note that these definitions divide the support of
ʔ
k
into two disjoints sets, namely
the support of
ʔ
k
and the support of
ʔ
k
. Moreover, by construction we know that
ʔ
k
˄
−ₒ
ʘ
, for some
ʘ
;welet
ʔ
k
+
1
be an arbitrary such
ʘ
.
This completes our definition of an extreme derivative as in Definition
6.4
and so
we have established (i).
For (ii), we observe that in a deterministic pLTS the above choice of
ʔ
k
+
1
is
unique, so that the whole derivative construction becomes unique.
It is worth pointing out that the use of subdistributions, rather than distributions,
is essential here. If
ʔ
diverges, that is, if there is an infinite sequence of derivations
ʔ
˄
−ₒ
˄
−ₒ
˄
−ₒ
...
, then one extreme derivative of
ʔ
is th
e empty
subdistributio
n
ʵ
. For
example, the only transition of
rec
x.x
is
rec
x.x
ʔ
1
...ʔ
k
˄
−ₒ
rec
x.x
,
and therefore
rec
x.x
diverges; consequently its unique extreme derivative is
ʵ
.
The final ingredient in the definition of the set of outcomes
d
(
T
,
P
) is to use this
notion of extreme derivative to formalise the subdistributions that can be reached
from [[[
T
|
Act
P
]]]. Note that all states
s
∈
ʘ
A
in the support of an extreme derivative
ˉ
−ₒ
either satisfy
s
for a unique
ˉ
∈
ʩ
,orhave
s
ₒ
.
[0, 1]
ʩ
Definition 6.9
(Outcomes) The outcome $
ʘ
∈
of a stable subdistribution
ʘ
is given by $
ʘ
(
ˉ
):
=
ʘ
(
s
).
ˉ
−ₒ
s
∈
ʘ
,
s
Putting all three ingredients together, we arrive at a definition of
A
d
(
T
,
P
):
Search WWH ::
Custom Search