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

5.5.1 The Simulation Preorders

Following tradition it would be natural to define simulations as relations between
states in a pLTS [ 13 , 14 ], as we did in Sect. 3.5. However, technically it is more con-
venient to use relations in sCSP ( sCSP ). One reason may be understood through

the example in Fig. 5.5 . Although in Example 5.3 we found out that R 2 pmay R 1 ,we
do have R 1 pmay R 2 . If we are to relate these processes via a simulation-like rela-
tion, then the initial state of R 1 needs to be related to the initial distribution of R 2 ,
containing the two states a.b and a.c .
Our definition of simulation uses weak transitions [ 15 ], which have the standard
definitions except that they now apply to distributions, and

× D

˄
−ₒ is used instead of

˄
−ₒ

. This reflects the understanding that if a distribution may perform a sequence
of internal moves before or after executing a visible action, different parts of the
distribution may perform different numbers of internal actions:

˄
⃒

˄
−ₒ ∗ ʔ 2 .

• Let ʔ 1 ʔ 2 whenever ʔ 1

˄
−ₒ ∗

˄
−ₒ ∗ ʔ 2 whenever a

a
⃒

a
−ₒ

• Similarly, ʔ 1 ʔ 2 denotes ʔ 1 ∈ Act .

A
−ₒ

ʱ
−ₒ

A
−ₒ

• We write s with A ↆ Act when ∀ ʱ ∈ A ∪{ ˄ } : s , and also ʔ

A
−ₒ

when ∀ s ∈ ʔ : s .

A
−ₒ

A
−ₒ ʔ pre for some ʔ pre such that ʔ pre

• More generally, write ʔ ⃒ if ʔ −ₒ .

Definition 5.4 A relation R ↆ S × D ( S ) is said to be a failure simulation if s R ʘ

implies

ʱ
−ₒ

ʱ
⃒

ʔ then there exists some ʘ such that ʘ ʘ and ʔ

† ʘ

• f s R

A
−ₒ

A
−ₒ

• f s then ʘ ⃒ .

We write s FS ʘ if there is some failure simulation R such that s R ʘ . Simi-

larly, we define (forward) simulation and s s ʘ by dropping the second clause in

Definition 5.4 .

Definition 5.5 The (forward) simulation preorder S and failure simulation

preorder FS on pCSP are defined as follows:

˄
⃒

s ) † ʘ P S Q iff [[ Q ]] ʘ for some ʘ with [[ P ]] (

˄
⃒ s ) † ʘ. P FS Q iff [[ P ]] ʘ for some ʘ with [[ Q ]] (

We have chosen the orientation of the preorder symbol to match that of must testing,
which goes back to the work of De Nicola and Hennessy [ 3 ]. This orientation also
matches the one used in CSP [ 1 ] and related work, where we have SPECIFICATION

IMPLEMENTATION. At the same time, we like to stick to the convention popular
in the CCS community of writing the simulated process to the left of the preorder
symbol and the simulating process (that mimics moves of the simulated one) on the
right. This is the reason for the orientation of the symbol

FS .