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

choice. However, the distributivities of both [ 30 ] and [ 32 ] constitute identifications
that cannot be justified by our testing approach; see [ 6 ].
In Jou and Smolka [ 33 ], as in [ 28 , 29 ], probabilistic equivalences based on traces,
failures and readies are defined. These equivalences are coarser than

pmay .For

example, let

P : = a. (( b.d c.e ) 2 ↕ ( b.f c.g ))

Q : = a. (( b.d c.g ) 2 ↕ ( b.f c.e )) .

The two processes cannot be distinguished by the equivalences of [ 28 , 29 , 33 ].
However, we can tell them apart by the test:

T : = a. (( b.d.ˉ 2 ↕ c.e.ˉ ) ( b.f.ˉ 2 ↕ c.g.ˉ ))

0, 2 ,1

1

since A ( T , P ) ={ } and A ( T , Q ) ={

2 }

, that is, P pmay Q .

5.11.2 Probabilistic Simulations

Four different notions of simulation for probabilistic processes occur in the literature,
each a generalisation of the well-known concept of simulation for nondeterministic
processes [ 34 ]. The most straightforward generalisation [ 35 ] is defined as in Defi-
nition 3.5. This simulation induces a preorder strictly finer than S and pmay .For

example, it does not satisfy the law

a. ( P p ↕ Q ) a.P a.Q

that holds in probabilistic may testing semantics. The reason is that the process
a.P a.Q can answer the initial a move of a. ( P p ↕ Q ) by taking either the a move
to P , or the a move to Q , but not by a probabilistic combination of the two. Such
probabilistic combinations are allowed in the probabilistic simulation of [ 14 ], which
induces a coarser preorder on processes, satisfying the above law. In our terminology
it can be defined by changing the requirement above into

ʱ
−ₒ

ʱ
−ₒ

R

ʘ then there is a ʔ with t ʔ and ʘ

R

† ʔ .

if s t and s

A weak version of this probabilistic simulation, abstracting from the internal action
˄ , weakens this requirement into

ʱ
−ₒ

ʱ
⃒

ʘ then there is a ʔ with t ʔ and ʘ

† ʔ .

if s R t and s R

Nevertheless, also this probabilistic simulation does not satisfy all the laws we have
shown to hold for probabilistic may testing. In particular, it does not satisfy the
law ( May3 ). Consider for instance the processes R 1 =

a.b.c. ( d 2 ↕ e ) and R 2 =

a. ( b.c.d 2 ↕ b.c.e ). The law ( May3 ), which holds for probabilistic may testing, would

yield R 1 R 2 . If we are to relate these processes via a probabilistic simulation à la