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

Here the conjunctions s a

ₒ ʔ range over suitable pairs a , ʔ , and s ˄ ₒ ʔ ranges over

suitable ʔ . The -characteristic formulae ˈ s and ˈ ʔ are defined likewise, but

omitting the conjuncts ref (

L

a
−ₒ}

{ a | s ).

We write ˕ ˈ with ˕ , ˈ ∈ F if for each distribution ʔ one has ʔ |= ˕ implies

˕ s and i ∈ I ˕ i

ʔ I ;

furthermore, the following property can be established by an easy inductive proof.

|= ˈ . Then it is easy to see that ˕ s ˕ i for any i ∈

Lemma 5.11 For any ʔ ∈ D ( sCSP ) we have ʔ |= ˕ ʔ , as well as ʔ |= ˈ ʔ .

This and the following lemma help to establish Theorem 5.5 .

∈ pCSP we have that [[ P ]] |=

Lemma 5.12 For any processes P , Q ˕ [[ Q ]] implies

P FS Q, and likewise [[ Q ]] |= ˈ [[ P ]] implies P S Q.

Proof by s R ʘ iff ʘ |= ˕ s ;

to show that it is a failure simulation we first prove the following technical result:

To establish the first statement, we define the relation R

˄
⃒

ʘ : ʘ ʘ ∧

† ʘ .

|= ∃ R

ʘ ˕ ʔ implies ʔ (5.25)

˕ ʔ with ˕ ʔ = i ∈ I p i · = i ∈ I p i · Suppose ʘ |= ˕ s i , so that we have ʔ s i and

˄
⃒ ʘ with

for all i ∈ I there are ʘ i ∈ D ( sCSP ) with ʘ i |= ˕ s i such that ʘ

= i ∈ I p i · ʘ i . Since s i R ʘ i for all i ∈ I we have ʔ R

ʘ :

† ʘ .

Now we show that R is a failure simulation. Assume that s R ʘ .

Suppose s ˄

• −ₒ ʔ . Then from Definition 5.7 we have ˕ s ˕ ʔ , so that ʘ |= ˕ ʔ .

Applying ( 5.25 ) gives us ʘ

˄
⃒

ʘ with ʔ

R

† ʘ for some ʘ .

a
−ₒ

• Suppose s ʔ with a ∈ Act . Then ˕ s a ˕ ʔ ,so ʘ |= a ˕ ʔ . Hence, there

a
⃒ ʘ and ʘ |= ˕ ʔ . Again apply ( 5.25 ).

ˆ

exists some ʘ with ʘ

X
−ₒ

• Suppose s with X ↆ A . Then ˕ s ref ( X ), so ʘ |= ref ( X ). Hence, there

X
ₒ

˄
⃒ exists some ʘ with ʘ ʘ and ʘ

.

Thus, R is indeed a failure simulation. By our assumption [[ P ]] |= ˕ [[ Q ]] , using ( 5.25 ),

˄
⃒ there exists a ʘ such that [[ P ]] ʘ and [[ Q ]]

† ʘ , which gives P

R FS Q via

Definition 5.5 .
To establish the second statement, define the relation S by s S ʘ iff ʘ |= ˈ s ;

exactly as above one obtains

˄
⃒

ʘ : ʘ ʘ ∧

† ʘ .

ʘ |= ˈ ʔ implies ∃ ʔ S (5.26)

Just as above it follows that S is a simulation. By the assum p tion [[ Q ]] |= ˕ [[ P ]] , using

˄
⃒ ʘ and [[ P ]]

ˆ

( 5.26 ), there exists a ʘ such that [[ Q ]] ʘ . Hence, P S Q via S

Definition 5.5 .

Theorem 5.5

L Q then P

1. If P S Q.

F Q then P 2. If P FS Q.