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

a
⃒

closed and convex. Its lifting coincides with , which can be shown by some

arguments analogous to those in the proof of Proposition 6.3 .

The second consequence of Theorem 6.9 concerns the manner in which diver-
gent computations arise in pLTSs. Consider again the infinite state pLTS given in
Example 6.5 . There is no state s that wholly diverges, that is satisfying s

⃒ ʵ , yet

there are many partially divergent computations. In fact for every k ≥ 2wehave

1

s k ⃒

k [[ a. 0 ]]. This cannot arise in a finitary pLTS; if there is any partial derivation
in a finitary pLTS, ʔ ʔ with ʔ |

⃒ | ʔ | > | , then there is some state in the pLTS

that wholly diverges.
WesayapLTSis convergent if s ⃒ ʵ for no state s ∈ S .

Lemma 6.18 Let ʔ be a subdistribution in a finite-state, convergent and determin-
istic pLTS. If ʔ

ʔ then ʔ |

⃒ | ʔ |=| .

Proof S . In other words,

each ˄ sequence from a state s is finite and ends with a distribution that cannot enable
a ˄ transition. In a deterministic pLTS, each state has at most one outgoing transition.
So from each s there is a unique ˄ sequence with length n s ≥

Since the pLTS is convergent, then s ⃒ ʵ for no state s ∈

0.

˄
−ₒ

˄
−ₒ

˄
−ₒ···

˄
−ₒ

˄
−ₒ s ʔ 1 ʔ 2 ʔ n s

Let p s be ʔ n s ( s ), where s is any state in the support of ʔ n s . We set

= {

n s |

∈ }

n max s S

p = min { p s | s ∈ S }

ʔ

where n and p are well defined as S is assumed to be a finite set. Now let ʔ ⃒

be any weak derivation constructed by a collection of ʔ k , ʔ k such that

ʔ 0 + ʔ 0 ʔ =

˄
−ₒ ʔ 1 ʔ 0 ʔ 1 +

.

˄
−ₒ ʔ k + 1 ʔ k ʔ k + 1 +

.
with ʔ = k = 0 ʔ k . From each ʔ kn + i with k , i ∈ N , the block of n steps of ˄

transition leads to ʔ ( k + 1) n + i ʔ ( k + 1) n + i |≤| ʔ kn + i | such that | (1 − p ). It follows that

j = 0 |

ʔ j |= n − 1

0 k = 0 |

ʔ kn + i |

i =

≤ n − 1

i = 0 k = 0 |

ʔ i |

−

p ) k

(1

= n − 1

i = 0 | ʔ i |

1
p

ʔ 0 |

n
p

≤|

Therefore, we have that lim k ₒ∞ ʔ k | ʔ |=| ʔ |

= 0, which in turn means that .