# Axiomatizing probabilistic processes: ACP with generative probabilities

## Abstract

This paper is concerned with finding complete axiomatizations of probabilistic processes. We examine this problem within the context of the process algebra ACP and obtain as our end-result the axiom system _{pr}ACP _{I} ^{−-} , a probabilistic version of ACP which can be used to reason algebraically about the reliability and performance of concurrent systems. Our goal was to introduce probability into ACP in as simple a fashion as possible. Optimally, ACP should be the homomorphic image of the probabilistic version in which the probabilities are forgotten.

We begin by weakening slightly ACP to obtain the axiom system ACP _{I} ^{−} The main difference between ACP and ACP _{I} ^{−} is that the axiom *x+δ=x*, which does not yield a plausible interpretation in the generative model of probabilistic computation, is rejected in ACP _{I} ^{−} . We argue that this does not affect the usefulness of ACP _{I} ^{−} in practice, and show how ACP can be reconstructed from ACP _{I} ^{−} with a minimal amount of technical machinery.

_{pr}ACP _{I} ^{−} is obtained from ACP _{I} ^{−} through the introduction of probabilistic alternative and parallel composition operators, and a process graph model for _{pr}ACP _{I} ^{−} based on *probabilistic bisimulation* is developed. We show that _{pr}ACP _{I} ^{−} is a sound and complete axiomatization of probabilistic bisimulation for finite processes, and that _{pr}ACP _{I} ^{−} can be homomorphically embedded in ACP _{I} ^{−} as desired.

Our results for ACP _{I} ^{−} and _{pr}ACP _{I} ^{−} are presented in a modular fashion by first considering several subsets of the signatures. We conclude with a discussion about the suitability of an internal probabilistic choice operator in the context of _{pr}ACP _{I} ^{−} .

## Keywords

Axiom System Probabilistic Process Stratify Model Probabilistic Version Complete Axiomatization## Preview

Unable to display preview. Download preview PDF.

## References

- [BBS92]J. C. M. Baeten, J. A. Bergstra, and S. A. Smolka.
*Axiomatizing Probabilistic Processes: ACP with Generative Probabilities*. Technical Report, Dept. of Math and Computing Science, Technical University of Eindhoven, Eindhoven, The Netherlands, 1992.Google Scholar - [BK84]J. A. Bergstra and J. W. Klop. Process algebra for synchronous communication.
*Information and Computation*, 60:109–137, 1984.zbMATHMathSciNetGoogle Scholar - [BM89]B. Bloom and A. R. Meyer. A remark on bisimulation between probabilistic processes. In Meyer and Tsailin, editors,
*Logik at Botik*, Springer-Verlag, 1989.Google Scholar - [BW90]J. C. M. Baeten and W. P. Weijland.
*Process Algebra. Cambridge Tracts in Computer Science 18*, Cambridge University Press, 1990.Google Scholar - [Chr90]I. Christoff.
*Testing Equivalences for Probabilistic Processes*. Technical Report DoCS 90/22, Ph.D. Thesis, Department of Computer Science, Uppsala University, Uppsala, Sweden, 1990.Google Scholar - [CSZ92]R. Cleaveland, S. A. Smolka, and A. E. Zwarico. Testing preorders for probabilistic processes. In
*Proceedings of the 19th ICALP*, July 1992.Google Scholar - [GJS90]A. Giacalone, C.-C. Jou, and S. A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In
*Proceedings of Working Conference on Programming Concepts and Methods*, IFIP TC 2, Sea of Gallilee, Israel, April 1990.Google Scholar - [JL91]B. Jonsson and K. G. Larsen. Specification and refinement of probabilistic processes. In
*Proceedings of the 6th IEEE Symposium on Logic in Computer Science*, Amsterdam, July 1991.Google Scholar - [JS90]C.-C. Jou and S. A. Smolka. Equivalences, congruences, and complete axiomatizations for probabilistic processes. In J. C. M. Baeten and J. W. Klop, editors,
*Proceedings of CONCUR '90*, pages 367–383, Springer-Verlag, Berlin, 1990.Google Scholar - [LS89]K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. In
*Proceedings of 16th Annual ACM Symposium on Principles of Programming Languages*, 1989.Google Scholar - [LS92]K. G. Larsen and A. Skou. Compositional verification of probabilistic processes. In
*Proceedings of CONCUR '92*, Springer-Verlag Lecture Notes in Computer Science, 1992.Google Scholar - [Mil80]R. Milner.
*A Calculus of Communicating Systems*. Volume 92 of*Lecture Notes in Computer Science*, Springer-Verlag, Berlin, 1980.Google Scholar - [Tof90]C. M. N. Tofts. A synchronous calculus of relative frequency. In J. C. M. Baeten and J. W. Klop, editors,
*Proceedings of CONCUR '90*, pages 467–480, Springer-Verlag, Berlin, 1990.Google Scholar - [vGSST90]R. J. van Glabbeek, S. A. Smolka, B. Steffen, and C. M. N. Tofts. Reactive, generative, and stratified models of probabilistic processes. In
*Proceedings of the 5th IEEE Symposium on Logic in Computer Science*, pages 130–141, Philadelphia, PA, 1990.Google Scholar