Testing Finite Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 141

Proposition 5.9 Let P and Q be in nCSP . Then P FS Q implies P E must Q.
Proof Similar to the proof of Proposition 5.8 , but using a reversed orientation of
the preorders. The only real difference is the case (2), which we consider now. So
assume Q FS [[ P ]], where Q has the form i ∈ I a i .Q i . Let X be any set of actions

X
−ₒ . Therefore, there exists a P such such that X ∩{ a i } i ∈ I =∅ ; then i ∈ I a i .Q i

˄
⃒

X
−ₒ [[ P ]] that [[ P ]] . By the Derivative lemma,

E must P . P (5.30)

a i
−ₒ [[ Q i ]], there exist P i , P i , P Since i ∈ I a i .Q i such that

i

˄
⃒

a i
−ₒ

˄
⃒ [[ P i ]] [[ P

i

s ) † [[ P

[[ P ]] [[ P i ]] ]] a n d [[ Q i ]] ( ]] .

i

Now

E must P i (5.31)
using the Derivative lemma, and P i FS Q i , by Definition 5.5 . By induction, we have
P i E must Q i , hence

P

a i .P i E must a i .Q i (5.32)

i ∈ I i ∈ I

The desired result is now obtained as follows:

E must P

P

i ∈ I P i

by ( I1 ), ( 5.30 ) and ( 5.31 )

a i .P i

E must

by ( Must2 )

i ∈ I

E must a i .Q i by ( 5.32 )

i ∈ I

Propositions 5.8 and 5.9 give us the completeness result stated in Theorem 5.7 .

5.11 Bibliographic Notes

In this chapter we have studied three different aspects of may and must testing
preorders for finite processes: (i) we have shown that the may preorder can be char-
acterised as a coinductive simulation relation, and the must preorder as a failure
simulation relation; (ii) we have given a characterisation of both preorders in a fini-
tary modal logic; and (iii) we have also provided complete axiomatisations for both
preorders over a probabilistic version of recursion-free CSP. Although we omitted
our parallel operator

| A from the axiomatisations, it and similar CSP and CCS-like
parallel operators can be handled using standard techniques, in the must case at the
expense of introducing auxiliary operators. A generalisation of results (i) and (ii)
above to a probabilistic ˀ -calculus, with similar proof techniques of characteristic
formulae and characteristic tests, has appeared in [ 17 ].