Testing Finitary Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 228

structural properties of derivation sets (finite generability) and similarities (infinite
approximations), which are of independent interest. The use of Markov decision
processes and Zero-One laws was essential in obtaining our results.
We have studied a notion of real-reward testing that extends the nonnegative-
reward testing (cf. Sect. 4.4) with negative rewards. It turned out that real-reward
may preorder is the inverse of real-reward must preorder, and vice versa. More
interestingly, for finitary convergent processes, real-reward must testing preorder
coincides with nonnegative-reward testing preorder.
There is a great amount of work about probabilistic testing semantics and simula-
tion semantics, as we have seen in Sects. 4.8 and 5.11. Here we mention the closely
related work [ 9 ], where Segala defined two preorders called trace distribution pre-
congruence ( TD ) and failure distribution precongruence ( FD ). He proved that the

pmay and that for “probabilistically
convergent” systems the latter coincides with an action-based version of

former coincides with an action-based version of

pmust . The
condition of probabilistic convergence amounts in our framework to the requirement
that for ʔ

ʔ we have ʔ |=

∈ D ( S ) and ʔ ⃒ | 1. In [ 4 ] it has been shown that

TD coincides with a notion of simulation akin to S .

In [ 14 ] by restricting the power of schedulers a testing preorder is proposed and
shown to coincide with a probabilistic ready-trace preorder that is strictly coarser
than our simulation preorder but is still a precongruence [ 15 ].

References

1. Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C.: Testing finitary probabilistic processes
(extended abstract). Proceedings of the 20th International Conference on Concurrency Theory,
Lecture Notes in Computer Science, vol. 5710, pp. 274-288. Springer (2009)
2. Jones, C.: Probabilistic non-determinism. Ph.D. thesis, University of Edinburgh (1990)
3. McIver, A.K., Morgan, C.C.: Abstraction, Refinement and Proof for Probabilistic Systems.
Springer (2005)
4. Lynch, N., Segala, R., Vaandrager, F.W.: Observing branching structure through probabilistic
contexts. SIAM J. Comput. 37 (4), 977-1013 (2007)
5. Milner, R.: Communication and Concurrency. Prentice Hall, New York (1989)
6. Puterman, M.L.: Markov Decision Processes. Wiley, New York (1994)
7. Rutten, J., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing
Concurrent and Probabilistic Systems. (Volume 23 of CRM Monograph Series). American
Mathematical Society (2004)
8. Segala, R.: Modeling and verification of randomized distributed real-time systems. Tech. Rep.
MIT/LCS/TR-676, PhD thesis, MIT, Dept. of EECS (1995)
9. 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
(1996)
10. Deng, Y., van Glabbeek, R., Morgan, C.C., Zhang, C.: Scalar outcomes suffice for finitary
probabilistic testing. Proceedings of the 16th European Symposium on Programming, Lecture
Notes in Computer Science, vol. 4421, pp. 363-378. Springer (2007)
11. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J ACM 32 (1),
137-161 (1985)