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

C
FS

S

Lemma 6.26

FS .
Proof We only need to check that the first clause in Definition 6.21 is equivalent to
the first clause in Definition 6.22 . For one direction, we consider the relation

coincides with

R : ={ ( s , ʘ ) | s ⃒ ʵ and ʘ ⃒ ʵ }

C

and show R ↆ

FS . Suppose s

R ʘ . By Lemma 6.24 there are two infinite sequences

˄
−ₒ ʔ 1

˄
−ₒ ʔ 2

˄
−ₒ ... and ʘ −ₒ ʘ 1 ˄

˄

s −ₒ ... . T hen we have both ʔ 1 ⃒ ʵ

and ʘ 1 ⃒ ʵ . Note that ʔ 1 ⃒ ʵ if and only if t ⃒ ʵ for each t ∈ ʔ 1 .

† ʘ 1 as we have ʔ 1 = t ∈ ʔ 1 ʔ 1 ( t )

· t , ʘ 1 = t ∈ ʔ 1 ʔ 1 ( t ) Therefore, ʔ 1 R · ʘ 1 ,

and t 1 because ʔ 1 , like s , is a distribution.

For the other direction, we show that ʔ (

R ʘ 1 . Here | ʔ 1 |=

FS ) † ʘ and ʔ

⃒ ʵ imply ʘ ⃒ ʵ .

FS ʘ and s

Then as a special case, we get s ⃒ ʵ imply ʘ ⃒ ʵ . By repeated

application of Lemma 6.25 , we can obtain two infinite sequences

˄
−ₒ⃒

˄
−ₒ⃒

˄
−ₒ⃒

˄
−ₒ⃒ ʔ ⃒ ʔ 1 ⃒ ... and ʘ ⃒ ʘ 1 ⃒ ...

FS ) † ʘ i for all i

C

such that ʔ i ( ≥ 1. By Lemma 6.24 this implies ʘ ⃒ ʵ .

C
FS

S
FS

C

The advantage of this new relation over is that in order to check s

FS ʘ

˄
−ₒ⃒

ʘ ,
rather than an infinite sequence of moves. However, to construct this matching move
we cannot rely on clause 2 in Definition 6.22 , as the move generated there might
actually be empty, which we have seen in Example 6.2 . Instead, we need a method
for generating weak moves that contain at least one occurrence of a ˄ -action.

when s diverges, it is sufficient to find a single matching move ʘ ⃒

˄
−ₒ p ʘ whenever we can | A t

Definition 6.23 (Productive Moves) Let us write s

| A t ˄ infer s −ₒ p ʘ from the last two rules in Fig. 6.2 . In effect this means that t

must contribute to the action.
These productive actions are extended to subdistributions in the standard manner,
giving ʔ ˄

⃒ p ʘ .
The following lemma is adapted from Lemma 5.8 in the last chapter, which still
holds in our current setting.
Lemma 6.27
(1) If Φ ⃒ Φ then Φ | A ʔ ⃒ Φ | A ʔ and ʔ | A Φ ⃒ ʔ | A Φ .
(2) If Φ

a
−ₒ

a
−ₒ

a
−ₒ Φ and a Φ | A ʔ and ʔ | A Φ .

∈ A then Φ | A ʔ | A Φ ʔ

a
−ₒ Φ, ʔ

a
−ₒ ʔ and a ∈ A then ʔ | A Φ

˄
−ₒ ʔ | A Φ .

(3) If Φ

(4) ( j ∈ J p j · Φ j ) | A ( k ∈ K q k · ʔ k ) = j ∈ J k ∈ K ( p j · q k ) · ( Φ j | A ʔ k ) .

R ↆ S × D sub ( S ) be two relations satisfying u

(5) Let = s | A t

and ʨ = ʘ | A t with s R ʘ and t ∈ S. Then ʔ R † ʘ and Φ ∈ D sub ( S ) implies
( ʔ | A Φ )

R , R ʨ whenever u

†

R ( ʘ | A Φ ) .