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

Theorem 5.2 If P S Q then P pmay Q.

pCSP ˉ

Proof For any test T ∈ and process P ∈ pCSP the set V f ( T | Act P )is

finite, so

P pmay Q ,iff max ( V f ([[ T | Act P ]])) ≤ max ( V f ([[ T | Act Q ]])) for every test T .

(5.7)

pCSP ˉ and ʱ ∈

The following properties for ʔ 1 , ʔ 2 ∈ Act ˄ are not hard to establish:

ʱ
⃒ ʔ 1 ʔ 2 implies max ( V f ( ʔ 1 )) ≥ max ( V f ( ʔ 2 )) . (5.8)

s ) † ʔ 2 implies max ( ʔ 1 ( V f ( ʔ 1 )) ≤ max ( V f ( ʔ 2 )) . (5.9)

Now suppose P S Q . Since S is preserved by the parallel operator, we have

T | Act Q for an arbitrary test T . By definition, this means that there is a

distribution ʔ such that [[ T

| Act P S T

˄
⃒ s ) † ʔ .By( 5.8 ) and ( 5.9 )

| Act Q ]] ʔ and [[ T | Act P ]] (

we infer that max ( V f [[ T | Act P ]] ) ≤ max ( V f [[ T | Act Q ]]). The result now follows from

( 5.7 ).

It is tempting to use the same idea to prove that P pmust Q ,but

now using the function min in place of max . However, the min -analogue of Property
( 5.8 ) is in general invalid. F or exa mple, let R b e the pr ocess a

FS Q implies P

| Act ( a ˉ ). We have

˄
ₒ

min ( V f ( R )) = 1, yet R 0 | Act 0 and min ( V f ( 0 | Act 0 )) = 0. Therefore, it is not the

˄
⃒

ˆ

case that ʔ 1 V f ( ʔ 2 )). Examining this example

reveals that the culprit is the “scooting” ˄ transitions, which are ˄ transitions of a
state that can enable an ˉ action at the same time.
Our strategy is therefore as follows: when comparing two states, “scooting” tran-
sitions are purposefully ignored. Write s

ʔ 2 implies min ( V f ( ʔ 1 )) ≤ min (

ʱ
−ₒ ˉ ʔ if both s

ˉ
−ₒ

ʱ
−ₒ

and s ʔ hold.

˄
−ₒ ˉ as

˄
−ₒ

˄
−ₒ ˉ in place of

˄
−ₒ We define using . Similarly, we define ⃒ ˉ

and ʱ ⃒ ˉ . Thus, the subscript ˉ on a transition of any kind indicates that no state

is passed through in which ˉ is enabled. A version of failure simulation adapted to
these transition relations is then defined as follows.

sCSP ˉ ( sCSP ˉ ) be the largest binary relation such

O

Definition 5.6 Let

FS ↆ

× D

O

that s

FS ʘ implies

ʱ
−ₒ ˉ ʔ , then there is some ʘ with ʘ

ʱ
⃒ ˉ ʘ and ʔ (

FS ) † ʘ

• f s

X
−ₒ

X
−ₒ

˄
⃒ ˉ ʘ and ʘ X , then there is some ʘ with ʘ

• f s with ˉ ∈ .

FS ) † ʘ .
Note that for processes P , Q in pCSP (as opposed to pCSP ˉ ), we have P

˄
⃒ ˉ ʘ for some ʘ with [[ Q ]] (

FS Q ,iff [ P ]]

Let P

FS Q iff

FS Q .
Proposition 5.4

P

If P , Q are processes in pCSP with P

FS Q and T is a process

in pCSP ˉ

FS T

then T | Act P | Act Q.

Proof Similar to the proof of Theorem 5.1 .