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

Now suppose ʘ FS ʔ . By Proposition 6.7 , there exists some ʘ with ʘ ⃒ ʘ
and ʔ (

e

FS ) † ʘ . By the above claim and Lemma 6.32 we obtain

( ʘ ) ( ʔ ) ,

V ( ʘ ) ↇ V ≤ Sm V

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

Theorem 6.13 For any finitary processes P and Q,ifP FS Q then P pmust Q.

Proof We reason as follows.

FS Q

P

implies [ P | Act T ] FS [ Q | Act T ] Lemma 6.30 , for any test T

implies V ([ P | Act T ]) ≤ Sm V ([ Q | Act T ]) [ · ]is ˉ -respecting; Lemma 6.33

d ( T , P ) d ( T , Q )

iff A ≤ Sm A Definition 6.24

pmust Q.

iff P Definition 6.11

In the proof of the soundness result above, we use Lemma 6.30 , which holds for
finitary processes only. For infinitary processes, a preorder induced by

S
FS

is not

sound for must testing.

E xample 6.24 We have seen in Example 6.21 that the state s from ( 6.20 ) is related to
0 via the relation q ˉ [ 2 ,1]

FS . If we apply test ˄.ˉ to both s and 0 , we obtain

{ | q ∈ }

ˉ

FS ) †

S

as an outcome set for the former and { } for the latter. Although s ( 0 ,we

d ( ˄.ˉ , s ).
If we replace sta te s by the state s 2 from ( 6.22 ), similar phenomenon happens.
Although s 2 (

d ( ˄.ˉ , 0 )

have A ≤ Sm A

FS ) † 0 ,wehave

} ≤ Sm q ˉ

1

2 ,1

ˉ

d ( ˄.ˉ , 0 ) d ( ˄.ˉ , s 2 ) .

A ={ | q ∈ = A

6.7 Failure Simulation is Complete for Must Testing

This section establishes the completeness of the failure simulation preorder with
respect to the must testing preorder. It does so in three steps. First, we provide
a characterisation of the preorder relation

FS by an inductively defined relation.
Secondly, using this, we develop a modal logic that can be used to characterise
the failure simulation preorder on finitary pLTSs. Finally, we adapt the results of
Sect. 5.7 to show that the modal formulae can in turn be characterised by tests; again
this result depends on the underlying pLTS being finitary. From this, completeness
follows.