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

Proof For every k part (iii) follows trivially from (ii). We prove (i) and (ii) simulta-
neously, by induction on k , with the case k = 0 being trivial. The inductive case, for

k + 1, follows the argument in the proof of Lemma 5.12.

ʵ . Then ˕ k + 1
s

(i) First suppose s ⃒ = div and therefore ʘ |= div , which gives

the required ʘ ⃒ ʵ .

˄
−ₒ Now suppose s ʔ . Here, there are two cases; if in addition s ⃒ ʵ we

have already seen that ʘ ⃒ ʵ and this i s the required matching move from ʘ ,

FS ) † ʵ . So let us assume that s

⃒

ʵ . Then by the definition of ˕ k + 1
s

since ʔ (

˕ ʔ , and we obtain the required matching move from
ʘ from the inductive hypothesis: induction on part (ii) gives some ʘ such that
ʘ

|=

we must have that ʘ

FS ) † ʘ .
The matching move for s

ʘ and ʔ ( ⃒

a
−ₒ ʘ is obtained in a similar manner.

X ˄

, by the definition of ˕ k + 1
s

Finally suppose s −ₒ . Since this implies s −ₒ we

X

must have that ʘ |= ref ( X ), which actually means that ʘ ⃒ −ₒ .

( s ∈ ʔ

(ii) Note that ˕ k + 1
ʔ

ʔ ( s )

˕ k + 1
s

= ( div ) 1 −| ʔ | ↕

| ʔ | ·

) and therefore by

ʘ div + s ∈ ʔ ʔ ( s ) ⃒ −| | · ·

ʘ s such that ʘ div |= definition ʘ (1 ʔ )

˕ k + 1
s

div and ʘ s |= . By definition, ʘ div ⃒ ʵ , so by Theorem 6.5 (i)

⃒ s ∈ ʔ

and the reflexivity and transitivity of ⃒ we obtain ʘ ʔ ( s ) · ʘ s .

k + 1
FS

By part (i) we have s ʘ s for every s in ʔ , which in turn means that

) † s ∈ ʔ

k + 1

ʔ ( ʔ ( s ) · ʘ s .

FS

F ʔ if and only if ʘ Theorem 6.16 FS ʔ.

Proof One direction follows immediately from Theorem 6.15 . For the opposite
direction, suppose ʘ

In a finitary pLTS, ʘ

F ʔ . By Lemma 6.37 we have ʔ ˕ ʔ , and hence ʘ ˕ ʔ , |= |=

FS ʔ . That

for all k ≥ 0. By part (iii) of the previous lemma we thus know that ʘ

ʘ FS ʔ now follows from Corollary 6.12 .

6.7.3 Characteristic Tests for Formulae

The import of Theorem 6.16 is that we can obtain completeness of the failure simula-
tion preorder with respect to the must-testing preorder by designing for each formula
˕ a test that in some sense characterises the property of a process of satisfying ˕ .
This has been achieved for the pLTS generated by the recursion free fragment of
rpCSP in Sect. 5.7. Here, we generalise this technique to the pLTS generated by the
set of finitary rpCSP terms.
As in Sect. 5.7, the generation of these tests depends on crucial characteristics
of the testing function

d (

), which are summarised in Lemmas 6.39 and 6.42
below, corresponding to Lemmas 5.9 and 5.10, respectively.

A − , −

Lemma 6.39 Let ʔ be a rpCSP process, and T , T i be tests.