Testing Finite Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 134

• Let ˕ = . For all ʔ ∈ D ( sCSP )wehave ʔ |= ˕ and ∃ o ∈ A ( T ˕ , ʔ ): o ≤ v ˕ ,

using Lemma 5.9 (1).

˄
⃒ = ↆ Act . Suppose ʔ |=

˕ . Then there is a ʔ with ʔ ʔ

• Let ˕ ref ( X ) with X

. By Lemma 5.9 (2), 0

X
−ₒ

and ʔ

∈ A ( T ˕ , ʔ ).

0 , so by Lemma 5.9 (2)

Now suppose ∃ o ∈ A ( T ˕ , ʔ ): o ≤ v ˕ . This implies o =

˄
⃒

X
−ₒ there is a ʔ with ʔ ʔ and ʔ

. Hence ʔ |= ˕ .

a
⃒

ˆ

˕ . Then there is a ʔ with ʔ ʔ

• Let ˕ = a ˈ with a ∈ Act . Suppose ʔ |=

and ʔ |= ( T ˈ , ʔ ): o

ˈ . By induction, ∃ o ∈ A ≤ v ˈ . By Lemma 5.9 (3), we

know that o ∈ A ( T ˕ , ʔ ).

Now suppose ∃ o ∈ A ( T ˕ , ʔ ): o ≤ v ˕ . This implies o ( ˉ ) = 0, so by using

a
⃒ Lemma 5.9 (3) we see that there is a ʔ with ʔ ʔ and o ( T ˈ , ʔ ). By

∈ A

induction, ʔ |=

ˈ ,so ʔ |= ˕ .

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

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

by Lemma 5.9 (4), and o ≤ v ˕ .

Now suppose ∃ o ∈ A ( T ˕ , ʔ ): o ≤ v ˕ . Then, using Lemma 5.9 (4), we have that

o = p · o 1 + (1 − p ) · o 2 for certain o i ∈ A ( T i , ʔ ). Note that T 1 , T 2 are ʩ -disjoint

tests. One has o i ≤

= =

v i for all i 1, 2, for if o i ( ˉ ) > v i ( ˉ ) for some i 1or2

∈

and ˉ ʩ , then ˉ must occur in T i and hence cannot occur in T 3 − i . This implies

v 3 − i ( ˉ ) 0 and thus o ( ˉ ) > v ˕ ( ˉ ), in contradiction with the assumption. By

induction, ʔ

=

|= ˕ i for all i = 1, 2, and hence ʔ |= ˕ .

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

˄
⃒ p · ʔ 1 +

ˆ

with ʔ i |= ˕ i such that ʔ (1 − p ) · ʔ 2 . By induction, for i = 1, 2,

v i . Hence, there are o i ∈ A ( T i , ʔ i ) with there are o i ∈ A ( T i , ʔ i ) with o i ≤

o i ≤ v i . Thus o : o 1 + o 2 ∈ A = p · (1 − p ) · ( T ˕ , ʔ ) by Lemma 5.9 (5), and o ≤ v ˕ .

Now suppose ∃ o ∈ A ( T ˕ , ʔ ): o ≤ v ˕ . Then, by Lemma 5.10 , there are q ∈ [0, 1]

˄
⃒

q ) o 2 and ʔ 1 , ʔ 2 , such that ʔ q · ʔ 1 + (1 − q ) · ʔ 2 and o = q · o 1 + (1 −

for some o i ∈ A ( T i , ʔ i ). Now i : o i ( ˉ i ) v i ( ˉ i )

1

∀ = =

2 , so, using that T 1 , T 2 are

1

o 1 ( ˉ 1 ) v 1 ( ˉ 1 )

1

ʩ -disjoint tests, we have

2 q

= q · = o ( ˉ 1 ) ≤ v ˕ ( ˉ 1 ) = p · =

2 p

1

· o 2 ( ˉ 2 ) v 2 ( ˉ 2 )

1

and − p ).

Together, these inequalities say that q = p . Exactly as in the previous case one
obtains o i ≤

2 (1

− q ) = (1 − q ) = o ( ˉ 2 ) ≤ v ˕ ( ˉ ) = (1 − p ) · =

2 (1

v i 1, 2. Given that T i = for all i = T i 2 ↕ ˉ i , using Lemma 5.9 (4), it

ˉ i for some o i ∈ A

must be that o =

1 1

2 2 o i +

( T i , ʔ i ) with o i ≤ v i . By induction,

ʔ i |= ˕ i for all i = 1, 2, and hence ʔ |= ˕ .

In case ˕ ∈ L , the formula cannot be of the form ref ( X ). Then a straightforward

induction yields that ˉ ∈ ʩ v ˕ ( ˉ )

= 1 and for all ʔ ∈ D ( pCSP ) and o ∈ A ( T ˕ , ʔ )

we have ˉ ∈ ʩ o ( ˉ )

= 1. Therefore, o ≤ v ˕ iff o ≥ v ˕ iff o = v ˕ , yielding

( 5.28 ).

Theorem 5.6

pmay Q then P

L Q.

1. If P