Testing Finitary Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 187

Corollary 6.8 (Zero-one Law - Deterministic Case) If for some s tatic derivative
policy dp over a finite-state pLTS there is for some s a derivation s ⃒ dp ʔ with
| ʔ | < 1 then in fact for some (possibly different) state s ʵ we have s ʵ ⃒ dp ʵ.
Proof ⃒ dp ʵ . Then the pLTS induced

by dp is convergent. Since it is o bviously finite-state and deterministic, we apply
Lemma 6.18 and obtain

Suppose that for no state s do we have s

ʔ |=| ʔ |

| s |= 1, contradicting the assumption that | < 1.

Therefore, there must exist some state s ʵ that wholly diverges.

Although it is possible to have processes that diverge with some probability strictly
between zero and one, in a finitary system it is possible to “distill” that divergence
in the sense that in many cases we can limit our analyses to processes that either
wholly diverge (can do so with probability one) or wholly converge (can diverge
only with probability zero). This property is based on the zero-one law for finite-state
probabilistic systems, and we present the aspects of it that we need here.

Lemma 6.19 (Distillation of Divergence - Deterministic Case) For an y state s and
static derivative policy dp over a finite-state pLTS, if there is a deri va tion s ⃒ dp ʔ

then there is a probability p and full distributions ʔ 1 , ʔ ʵ such that s ( ʔ 1 p ↕ ʔ ʵ ) ⃒

and ʔ = ʔ 1 and ʔ ʵ ⃒

p · ʵ.

We m o dify dp so as to obtain a static policy dp by setting dp ( t )

= dp ( t )

Proof

⃒ dp ʵ , in which case we set dp ( t )

↑

except when t . The new policy determines

⃒ dp ʔ for some subdistribution ʔ , and induces a
sub-pLTS from the pLTS induced by dp . Note that the s ub -pLTS is deterministic
and convergent. By Lemma 6.18 , we know that

a unique weak derivation ʔ

| ʔ |=| s |= 1. We split ʔ up

into ʔ 1 + ʔ ʵ ʔ ʵ

is wholly divergent under policy dp and
ʔ 1 is supported by all other states. From ʔ ʵ the policy dp determines th e weak
derivation ʔ ʵ ⃒ dp ʵ . Combining the two weak derivations we have s

so that each state in

⃒ dp

ʔ 1 + ʔ ʵ ⃒ dp ʔ 1 . As we only divide the original weak derivation into two stages

and do not change the ˄ transition from each state, the final subdistribution will not
change, thus ʔ 1 =

ʔ . Finally, we determine p , ʔ 1 and ʔ ʵ ʔ |

by letting p =| ,

ʔ 1 =

1

p ʔ and ʔ ʵ =

1

p ʔ ʵ .

1 −

Theorem 6.11 ( Distillation of Divergence—General Case) For any s , ʔ in a fini-
tary p LTS with s ⃒ ʔ there is a probability p and full distributions ʔ 1 , ʔ ʵ

such

( ʔ 1 p ↕ ʔ ʵ ) and ʔ = ʔ 1 and ʔ ʵ ⃒

that s ⃒ p · ʵ.

Proof ( I is a finite index set) be all the static d erivative policies

in the finitary pLTS. Each polic y determines a weak derivation s

Let { dp i | i ∈ I }

ʔ i . From

⃒ dp i

ʔ then ʔ = i ∈ I p i ʔ i Theorem 6.9 , we know that if s ⃒ for some p i with

i ∈ I p i =

1. By Lemma 6.19 , for each i ∈ I , there is a probability q i and full

distributions ʔ i ,1 , ʔ i , ʵ such that s ( ʔ i ,1 q i ↕ ʔ i , ʵ ), ʔ i = ʔ i ,1 , and ʔ i , ʵ ⃒ ⃒ q i · ʵ .

=| i ∈ I p i q i · Finally, we determine p , ʔ 1 and ʔ ʵ ʔ i ,1 | , ʔ 1 =

1

p ʔ ,

by letting p

p i ∈ I p i (1

and ʔ ʵ =

1

q i ) ʔ i , ʵ . They satisfy our requirements just by noting that −

⃒ i ∈ I p i ( ʔ i ,1 q i ↕

1 −

ʔ i , ʵ ) ʔ 1 p ↕ ʔ ʵ

s

The requirement on the pLTS to be finitary is essential for this distillation of
divergence, as we explain in the following examples.

=