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

6.6.4 Soundness

In this section, we prove that failure simulations are sound for showing that processes
are related via the failure-based testing preorder. We assume initially that we are using
only one success action ˉ , so that 1.

Because we prune our pLTSs before extracting values from them, we will be
concerned mainly with ˉ -respecting structures.

| ʩ |=

Definition 6.24 Let ʔ be a subdistribution in a pLTS S , { ˉ , ˄ } , ₒ . We write V ( ʔ )

$ ʔ | ʔ }

for the set of testing outcomes { ʔ ⃒ .

Lemma 6.31 Let ʔ and ʘ be subdistributions in an ˉ-respecting pLTS given by

FS ) † ʘ, then

e

S , { ˄ , ˉ } , ₒ .Ifʔ is stable and ʔ ( V ( ʘ ) ≤ Sm V ( ʔ ) .

e

Proof We first show that if s is stable and s

FS ʘ then

V ( ʘ ) ≤ Sm V ( s ). Since s is

stable, we have only two cases:

e FS ʘ we have ʘ

ʘ with ʘ

(i) s −ₒ . Here V ( s ) ={ 0 } and since s ⃒ −ₒ ,

ʘ and $ ʘ =

whence in fact ʘ ⃒ 0. Therefore 0 ∈ V ( ʘ ) that means

V ( ʘ ) ≤ Sm V ( s ).

ˉ
−ₒ

ˉ
−ₒ ʔ for some ʔ . Here ʘ with $ ʘ =| ʘ |

(ii) s V ( s ) ={ 1 } and ʘ ⃒ .

ʘ and so again we have

Because the pLTS is ˉ -respecting, in fact ʘ ⃒

V ( ʘ ) ≤ Sm V ( s ).

e FS ) † ʘ . Use Proposition 6.2 to decom-

Now, for the general case, we suppose ʔ (

pose ʘ into s ∈ ʔ ʔ ( s )

e FS ʘ s for each s

· ∈

ʘ s such that s ʔ , and recall each

such state s is stable. From above we have that V ( ʘ s ) ≤ Sm V ( s ) for those s , and so

= s ∈ ʔ ʔ ( s ) ≤ Sm s ∈ ʔ ʔ ( s ) V ( ʘ ) · V ( ʘ s ) · V ( s ) = V ( ʔ ).

Lemma 6.32 Let ʔ be a subdistribution in an ˉ-respecting pLTS S , { ˄ , ˉ } , ₒ .

If ʔ ⃒ ʔ then ( ʔ )

V ↆ V ( ʔ ) .

Note that if ʔ ⃒ ʔ then ʔ ʔ ⃒ ʔ , so that every extreme

Proof ⃒

derivative of ʔ is also an extreme derivative of ʔ .

Lemma 6.33 Let ʔ and ʘ be subdistributions in an ˉ-respecting pLTS given by

S , { ˄ , ˉ } , ₒ .Ifʘ FS ʔ, then it holds that V ( ʘ ) ≤ Sm V ( ʔ ) .

Proof Let ʔ and ʘ be subdistributions in an ˉ -respecting pLTS S , { ˄ , ˉ } , ₒ .We

first claim that

FS ) † ʘ , then

e

If ʔ ( V ( ʘ ) ≤ Sm V ( ʔ ).

FS ) † ʘ . For any ʔ

e

ʔ we have the matching transition We assume that ʔ ( ⃒

e FS ) † ʘ . It follows from Lemmas 6.31 and 6.32 that

ʘ such that ʔ (

ʘ ⃒

( ʘ ) ( ʔ ) . V ( ʘ ) ↇ V ≤ Sm V

V ≤ Sm V

Consequently, we obtain ( ʘ ) ( ʔ ).