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

[ 14 ], the state c. ( d 2 ↕ e )of R 1 , reachable after an a and a b step, needs to be related
to the distribution ( c.d 2 ↕

c.e )of R 2 , containing the two states a.b and a.c . This
relation cannot be obtained through lifting, as this would entail relating the single
state c. ( d 2 ↕ e ) to each of the states c.d and c.e . Such a relation would not be sound,
because c. ( d 2 ↕ e ) is able to perform the sequence of actions ce half of the time,
whereas the process c.d cannot mimic this.
In [ 36 ], another notion of simulation is proposed, whose definition is too compli-
cated to explain in few sentences. They show for a class of probabilistic processes
that do not contain ˄ actions, that probabilistic may testing is captured exactly
by their notion of simulation. Nevertheless, their notion of simulation makes
strictly more identifications than ours. As an example, let us consider the processes
R 1 = c ) of Example 5.11 , which also

appear in Sect. 5 of [ 36 ]. There it is shown that R 1

a 2 ↕ ( b c ) and R 3 = ( a b ) 2 ↕ ( a

R 3 holds in their semantics.
However, in our framework we have R 1 pmay R 3 , as demonstrated in Example 5.11 .
The difference can only be explained by the circumstance that in [ 36 ] processes, and
hence also tests, may not have internal actions. So this example shows that tests with
internal moves can distinguish more processes than tests without internal moves,
even when applied to processes that have no internal moves themselves.
Our notion of forward simulation first appears in [ 7 ], although the preorder S

of Definition 5.5 is new. Segala has no expressions that denote distributions and
consequently is only interested in the restriction of the simulation preorder to states
( automata in his framework). It turns out that for states s a n d t (or expressions in
the set sCSP in our framework) we have s

s t , so on their common
domain of definition, the simulation preorder of [ 7 ] agrees with ours. This notion
of simulation is strictly more discriminating than the simulation of [ 36 ], and strictly
less discriminating than the ones from [ 14 ] and [ 35 ].

S t iff s

References

1. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
2. Segala, R.: Testing probabilistic automata. Proceedings of the 7th International Conference on
Concurrency Theory. Lecture Notes in Computer Science, vol. 1119, pp. 299-314. Springer,
Heidelberg (1996)
3. De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci. 34 ,
83-133 (1984)
4. Hennessy, M.: An Algebraic Theory of Processes. The MIT Press, Cambridge (1988)
5. Yi, W., Larsen, K.G.: Testing probabilistic and nondeterministic processes. Proceedings of
the IFIP TC6/WG6.1 12th International Symposium on Protocol Specification, Testing and
Verification, IFIP Transactions , vol. C-8, pp. 47-61. North-Holland (1992)
6. Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C.C., Zhang, C.: Remarks on testing
probabilistic processes. Electron. Notes Theor. Comput. Sci. 172 , 359-397 (2007)
7. Segala, R.: Modeling and verification of randomized distributed real-time systems. Tech. Rep.
MIT/LCS/TR-676. PhD thesis, MIT, Dept. of EECS (1995)
8. Lynch, N., Segala, R., Vaandrager, F.W.: Observing branching structure through probabilistic
contexts. SIAM J. Comput. 37 (4), 977-1013 (2007)