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

−ₒ ʔ k + 1 and ʔ = k = 1 ʔ k . Since it holds that

˄

that s = ʔ 0 , ʔ k = ʔ k + ʔ k , ʔ k

FS ) † ʘ , using Proposition 6.2 we can define ʘ

ʔ 0 + : ʘ 0 + ʔ 0 ʘ 0 = s ( = so

FS ) † ʘ 0 and ʔ 0 FS ) † ʘ 0 . Since ʔ 0

˄
−ₒ

FS ) † ʘ 0

that ʔ 0 (

S S

ʔ 1 and ʔ 0

S

( (

FS ) † ʘ 1 .
Repeating the above procedure gives us inductively a series ʘ k , ʘ k

it follows that ʘ 0

S

⃒ ʘ 1 with ʔ 1 (

, ʘ k of sub-

FS ) †

ʘ k ,

≥

0, such that ʘ 0 = ʘ k , ʘ k = ʘ k

+

distributions, for k ʘ , ʔ k (

= i ʘ i

FS ) † FS ) †

˄
⃒ ʔ k ʘ k

S

, ʔ k

S

ʘ k and ʘ k ʘ k . We define ʘ :

( ( .

FS ) †

By Additivity (Remark 6.2 ), we have ʔ

S

ʘ . It remains to be shown that

(

ʘ .
For that final step, since ( ʘ

ʘ ⃒

⃒ ) is closed according to Lemma 6.17 , we can

ʘ by exhibiting a sequence ʘ i ʘ i

establish ʘ ⃒ with ʘ ⃒ for each i and with

the ʘ i being arbitrarily close to ʘ . Induction establishes for each i that

ʘ i ʘ ⃒ ʘ i ʘ k : = + .

k ≤ i

ʔ |= ʔ i |= Since | 1, we are guaranteed to have that lim i ₒ∞ | 0, whence by

FS ) †

Lemma 6.2 , using that ʔ i

S

ʘ i ʘ i 0. Thus, these ʘ i s

( , also lim i ₒ∞ | |=

form the sequence we needed.
That concludes the case for

ʔ |= 1. If on the other hand ʔ =

| ʵ , that is we have

FS ) † ʵ trivially.

ʔ |=

S S

| 0, then ʘ ⃒ ʵ follows immediately from s

FS ʘ , and ʵ (

ʔ , then by Theorem 6.11 we have s ʔ 1 p ↕ ʔ ʵ

In the general case, if s ⃒ ⃒

for some probability p and distributions ʔ 1 , ʔ ʵ , with ʔ = ʔ 1 and ʔ ʵ ⃒ p · ʵ .

FS ) †

ʘ 1 p ↕ ʘ ʵ with ʔ 1

S

ʘ 1

From the mass-1 case above, we have ʘ ⃒ ( and

FS ) † ʘ ʵ ; from the mass-0 case, we have ʘ ʵ ⃒

ʔ ʵ ʵ and hence ʘ 1 p ↕ ʘ ʵ ⃒

(

p · ʘ 1 by Theorem 6.5 (i); thus transitivity yields ʘ ⃒ p · ʘ 1 , with ʔ = p ·

FS ) † p

ʔ 1 (

The proof of Theorem 6.12 refers to Theorem 6.11 where the underlying pLTS is
assumed to be finitary. As we would expect, Theorem 6.12 fails for infinitary pLTSs.

·

ʘ 1 as required, using Definition 6.2 (2).

Ex a mple 6.22 We have seen in Example 6.21 that th e state s from ( 6.20 ) is related
to 0 via the relation

S e

FS . We now com pa re s with 0 according to FS . From state

s , we have the weak transition s ⃒ 0 1 / 2 ↕ ʵ , which cannot be matched by any

e

transition from 0 , thus s

FS 0 . This means that Theorem 6.12 fails for infinitely

branching processes.
If we replace state s by the state s 2 from ( 6.22 ), similar phenomenon happens.
Therefore, Theorem 6.12 also fails for finitely branching but infinite-state processes.

6.6.3 Precongruence

FS is preserved
by the constructs of rpCSP . The proofs follow closely the corresponding proofs in

The purpose of this section is to show that the semantic relation