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

Let Φ 1 = k = 0 ʔ k 1 and Φ 2 = k = 0 ʔ k 2 . By (iii) and (iv) above we obtain a
weak ˄ move ʔ ⃒ Φ 1 + Φ 2 .For k ≥ 0, let ʓ k = ʔ k | A ( T 1 T 2 ), let ʓ 0 : : = ʵ

and let ʓ k + 1 = ʔ k 1 | A T 1 + ʔ k 2 | A T 2 . Moreover, ʓ :

: = Φ 1 | A T 1 + Φ 2 | A T 2 . Now all

conditions of Definition 6.5 are fulfilled, so ʔ 0 | A ( T 1 T 2 ) ⃒ ʓ is an initial segment

of ʔ 0 | A ( T 1 T 2 ) ⃒ ʨ . By Proposition 6.4 ,wehave Φ 1 | A T 1 + Φ 2 | A T 2 ⃒ ʨ .

d ( T 1

Lemma 6.42 If o ∈ A T 2 , ʔ ) then there are a q ∈ [0, 1] and subdistributions

ʔ 1 , ʔ 2 ∈ D sub ( sCSP ) such that ʔ ⃒ q · ʔ 1 + (1 − q ) · ʔ 2 and o = q · o 1 + (1 − q ) · o 2

d ( T i , ʔ i ) .

for certain o i ∈ A

d ( T 1

Proof If o ∈ A T 2 , ʔ ) then there is an extreme derivative of [( T 1 T 2 ) | Act ʔ ],

say ʨ , such that $ ʨ = o . By Lemma 6.41 there are Φ 1,2 such that

Φ 2
(ii) and [ T 1 | Act Φ 1 ]

(i) ʔ ⃒ Φ 1 +

+ [ T 2 | Act Φ 2 ] ⃒ ʨ .

By Theorem 6.5 (ii), there are some subdistributions ʨ 1 and ʨ 2 such that ʨ = ʨ 1 + ʨ 2

1, 2. Let o i = and T i | Act Φ i ⃒ ʨ i for i = $ ʨ i .As ʨ i is stable we obtain that

o i ∈ A

d ( T i , Φ i ). We also have o

o 1 + o 2 . = $ ʨ = $ ʨ 1 + $ ʨ 2 =

We now distinguish two cases:
• f ʨ 1 = ʵ , then we take ʔ i = Φ i , o i = o i for i

= =

1, 2 and q 0. Symmetrically,

o i if ʨ 2 = ʵ , then we take ʔ i = Φ i , o i =

= =

for i 1, 2 and q 1.

| Φ 1 |
| Φ 1 + Φ 2 |

1
q Φ 1 , ʔ 2 =

1
1 − q Φ 2 ,

• f ʨ 1 = ʵ and ʨ 2 = ʵ , then we let q = , ʔ 1 =

1

q o 1 and o 2 = − q o 2 .

1

o 1 =

1

o 1 + o 2

·

ʔ 1 +

− ·

ʔ 2 = Φ 1 +

·

o 1 +

− ·

o 2 =

It is easy to check that q (1 q ) Φ 2 , q (1 q )

and o i ∈ A

d ( T i , ʔ i ) for i

= 1, 2.

Proposition 6.14 For every formula ˕ ∈ F there exists a pair ( T ˕ , v ˕ ) with T ˕ an

[0, 1] ʩ ʩ-test and v ˕ ∈ such that

d ( T ˕ , ʔ ): o

ʔ |= ˕ if and only if ∃ o ∈ A ≤ v ˕ . (6.26)

T ˕ is called a characteristic test of ˕ and v ˕ its target value .
Proof The proof is adapted from that of Lemma 5.13, from where we take the
following remarks: As in vector-based testing ʩ is assumed to be countable (cf.
page 74) and ʩ -tests are finite expressions, for every ʩ -test there is an ˉ ʩ

not occurring in it. Furthermore, if a pair ( T ˕ , v ˕ ) satisfies requirement ( 6.26 ), then
any pair obtained from ( T ˕ , v ˕ ) by bijectively renaming the elements of ʩ also
satisfies that requirement. Hence, two given characteristic tests can be assumed to
be ʩ-disjoint , meaning that no ˉ

∈

∈ ʩ occurs in both of them.

is identical to that used in Sect. 5.7, with the addition of one
extra constant div . So we need a new characteristic test and target value for this latter
formula and reuse those from Sect. 5.7 for the rest of the language.

Our modal logic F

ˉ .

• Let ˕ = . Take T ˕ : = ˉ for some ˉ ∈ ʩ , and v ˕ : =

0 .

• Let ˕ = div . Take T ˕ : = ˄.ˉ for some ˉ ∈ ʩ , and v ˕ : =