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

˄
−ₒ R is more complicated and is determined by the moves

The definition of

˄
−ₒ ʔ k

ʔ k + 1 .Foragiven k this move means that

˄
−ₒ ʔ k

= p i · s i , ʔ k + 1 = p i · ʓ i , s i ʓ i

i ∈ I i ∈ I

So for each k we let

−ₒ R
s i = s

˄

ʓ ↓ k + 1
i

( s , k ) p i ·

This definition ensures
(c) ( ʔ k

˄
−ₒ R ( ʔ k + 1 ) ↓ k + 1 ;

) ↓ k

(d) ( ʔ k ) ↓ k is stable.

This completes our definition of the deterministic pLTS underlying the required
resolution; it remains to find subdistributions ʘ , ʘ over R such that ʔ = Img f ( ʘ ),

ʔ = ʘ .

Because of (b) (c) and (d), we have the following extreme derivation, which by
part (ii) of Lemma 6.7 is the unique one from ʔ ↓ 0 :

Img f ( ʘ ) and ʘ

⃒

ʔ ↓ 0 ( ʔ 0 ) ↓ 0 ( ʔ 0 ) ↓ 0

= +

˄
−ₒ R

( ʔ 0 ) ↓ 0 ( ʔ 1 ) ↓ 1 ( ʔ 1 ) ↓ 1 +

. .

˄
−ₒ R ( ʔ k + 1 ) ↓ k + 1 ( ʔ k + 1 ) ↓ k + 1

. ————————

( ʔ k ) ↓ k +

ʘ = k = 0 ( ʔ k ) ↓ k

Letting ʘ be ʔ ↓ 0 , we see that (a) above ensures ʔ

=

Img f ( ʘ ); the same note and
the linearity of f applied to distributions also gives ʔ = Img f ( ʘ ).

The converse is somewhat simpler.

Proposition 6.5 (Extreme Derivatives from Resolutions) Suppose R , ʘ , ₒ R is

a resolution of a subdistribution ʔ inapLTS S , ʩ ˄ , ₒ with resolving function f .

Then ʘ ⃒ R ʘ implies ʔ ⃒ Img f ( ʘ ) .
Proof Consider any derivation of ʘ ⃒ R ʘ along the lines of Definition 6.4 .

By systematically applying the function f to the component subdistributions in this
derivation we get a derivation Img f ( ʘ )

Img f ( ʘ ).
To show that Img f ( ʘ ) is actually an extreme derivative it suffices to show that s is
stable for every s

Img f ( ʘ ), that is, ʔ

⃒ ⃒

Img f ( ʘ ) Img f ( ʘ )

∈ . But if s ∈ , then by definition there is

⃒ R ʘ the state t must be stable.
The stability of s now follows from requirement (iii) of Definition 4.3.

ʘ some t ∈ such that s = f ( t ). Since ʘ