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

• Let ˕ = ref ( X ) with X ↆ Act . Take T ˕ : = a ∈ X a.ˉ for some ˉ ∈ ʩ , and set

0 .

v ˕ : =

• Let ˕ = a ˈ . By induction, ˈ has a characteristic test T ˈ with target value v ˈ .

Take T ˕ : = ˄.ˉ a.T ˈ where ˉ ∈ ʩ does not occur in T ˈ , and v ˕ : = v ˈ .

• Let ˕ ˕ 2 . Choose an ʩ -disjoint pair ( T i , v i ) of characteristic tests T i with

target values v i , for i

= ˕ 1 ∧

= 1, 2. Furthermore, let p ∈ (0, 1] be chosen arbitrarily,

and take T ˕ : = T 1 p ↕ T 2 and v ˕ : = p · v 1 + (1 − p ) · v 2 .

• Let ˕ ˕ 2 . Again choose an ʩ -disjoint pair ( T i , v i ) of characteristic tests

T i with target values v i , i

= ˕ 1 p ↕

1, 2, this time ensuring that there are two distinct
success actions ˉ 1 , ˉ 2 that do not occur in any of these tests. Let T i :

=

= T i 2 ↕ ˉ i

1 1

and v i : 1, 2 we have that T i is also a characteristic

test of ˕ i with target value v i . Take T ˕ :

=

2 v i + 2

=

ˉ i . Note that for i

T 1 T 2 v 1 + v 2 .

= = · − ·

and v ˕ : p (1 p )

Note that v ˕ ( ˉ ) ʩ does not occur in T ˕ .

As in the proof of Lemma 5.13, we now check by induction on ˕ that ( 6.26 ) above
holds; the proof relies on Lemmas 6.39 and 6.42 .

= 0 whenever ˉ ∈

• Let ˕ = . For all ʔ ∈ D sub ( sCSP )wehave ʔ |= ˕ and it always holds that

d ( T ˕ , ʔ ): o

∃ o ∈ A ≤ v ˕ , using Lemma 6.39 (1).

• Let ˕ = div . Suppose ʔ |= ˕ . Then, we have that ʔ ⃒ ʵ . By Lemma 6.39 (2),

0 ∈ A

d ( T ˕ , ʔ ).
Now suppose

0 , so we apply

d ( T ˕ , ʔ ): o

∃ o ∈ A ≤ v ˕ . This implies o =

Lemma 6.39 (2) and obtain ʔ ⃒ ʵ . Hence ʔ |= ˕ .

X

• Let ˕ = ref ( X ) with X ↆ Act . Suppose ʔ |= ˕ . Then ʔ ⃒ −ₒ . We can use

Lemma 6.39 (3) and obtain 0 ∈ A

d ( T ˕ , ʔ ).

0 ,so ʔ

A

∃ ∈ A

d ( T ˕ , ʔ ): o

≤ = ⃒ −ₒ

Now suppose o v ˕ . This implies o by

|=

Lemma 6.39 (3). Hence ʔ ˕ .

a
⃒ • Let ˕ = a ˈ with a ∈ Act . Suppose ʔ |= ˕ . Then there is a ʔ with ʔ ʔ

and ʔ |=

d ( T ˈ , ʔ ): o

ˈ . By induction, ∃ o ∈ A ≤ v ˈ . By Lemma 6.39 (4), we

d ( T ˕ , ʔ ).
Now suppose

get o ∈ A

d ( T ˕ , ʔ ): o ≤

∃ o ∈ A v ˕ . This implies o ( ˉ ) = 0, hence by

a
⃒ Lemma 6.39 (4) there is a ʔ with ʔ ʔ and o

d ( T ˈ , ʔ ). By induction,

∈ A

ʔ |=

ˈ ,so ʔ |= ˕ .

• Let ˕ = ˕ 1 ∧ ˕ 2 and suppose ʔ |= ˕ . Then ʔ |= ˕ i for i = 1, 2 and hence, by

d ( T i , ʔ ): o i ≤ d ( T ˕ , ʔ )

induction, ∃ o i ∈ A v i . Thus, o : = p · o 1 + (1 − p ) · o 2 ∈ A

by Lemma 6.39 (5), and o ≤ v ˕ .

d ( T ˕ , ʔ ): o

Now, suppose ∃ o ∈ A ≤ v ˕ . Then, using Lemma 6.39 (5), we know

d ( T i , ʔ ). Recall that T 1 , T 2 are

that o = p · o 1 + (1 − p ) · o 2 for certain o i ∈ A

ʩ -disjoint tests. One has o i ≤ v i for both i = 1, 2, for if o i ( ˉ ) > v i ( ˉ ) for some

i ʩ , then ˉ must occur in T i and hence cannot occur in

T 3 − i . This implies v 3 − i ( ˉ )

= 1or2and ˉ ∈

= 0 and thus o ( ˉ ) > v ˕ ( ˉ ), in contradiction with the

assumption. By induction, ʔ |= ˕ i for i = 1, 2, and hence ʔ |= ˕ .

• Let ˕ = ˕ 1 p ↕ ˕ 2 . Suppose ʔ |= ˕ . Then there are ʔ 1 , ʔ 2 ∈ D sub ( sCSP ) with

ʔ 1 |= ˕ 1 and ʔ 2 |= ˕ 2 such that ʔ ⃒ p · ʔ 1 + (1 − p ) · ʔ 2 . By induction, for