Introduction - Semantics of Probabilistic Processes: An Operational Approach - page 5

consequence, if two processes behave differently we can tell them apart by a finite
test.
We also introduce a notion of real-reward testing that allows for negative rewards.
It turns 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.
In Chap. 7 we introduce a notion of weak probabilistic bisimulation simply by
taking the symmetric form of the simulation preorder given in Chap. 6. It provides a
sound and complete proof methodology for an extensional behavioural equivalence,
a probabilistic variant of the traditional reduction barbed congruence well known in
concurrency theory.
References
1. Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam
(1984)
2. Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
3. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
4. Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Comput. 60 ,
109-137 (1984)
5. Baeten, J.C.M., Weijland, W.P.: Process Algebra, Cambridge Tracts in Theoretical Computer
Science, vol. 18. Cambridge University Press, Cambridge (1990)
6. Giacalone, A., Jou, C.C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent sys-
tems. Proceedings of IFIP TC2 Working Conference on Programming Concepts and Methods
(1990)
7. Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities.
Proceedings of IEEE Real-Time Systems Symposium. IEEE Computer Society Press, 278-287
(1990)
8. Lowe, G.: Probabilities and priorities in timed CSP. Ph.D. Thesis, Oxford (1991)
9. Andova, S.: Process algebra with probabilistic choice. Tech. Rep. CSR 99-12, Eindhoven
University of Technology (1999)
10. Herescu, O.M., Palamidessi, C.: Probabilistic asynchronous pi-calculus. Tech. Rep., INRIA
Futurs and LIX (2004)
11. Scott, D., Strachey, C.: Toward a mathematical semantics for computer languages. Technical
Monograph PRG-6, Oxford University Computing Laboratory (1971)
12. Floyd, R.W.: Assigning meanings to programs. Proc. Am. Math. Soc. Symp. Appl. Math. 19 ,
19-31 (1967)
13. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12 (10), 576-
580 (1969)
14. Plotkin, G.: The origins of structural operational semantics. J Log Algebraic Program 60-61,
3-15 (2004)
15. Park, D.: Concurrency and automata on infinite sequences. Proceedings of the 5th GI-
Conference on Theoretical Computer Science, Lecture Notes in Computer Science, vol. 104,
Springer, 167-183 (1981)
16. De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci. 34 ,
83-133 (1984)
17. Hennessy, M.: Algebraic Theory of Processes. The MIT Press, Cambridge (1988)