Axiomatizing probabilistic processes: ACP with generative probabilities

Extended abstract
  • J. C. M. Baeten
  • J. A. Bergstra
  • S. A. Smolka
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


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 prACP 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.

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

Our results for ACP I and prACP 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 prACP I .


Axiom System Probabilistic Process Stratify Model Probabilistic Version Complete Axiomatization 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [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
  2. [BK84]
    J. A. Bergstra and J. W. Klop. Process algebra for synchronous communication. Information and Computation, 60:109–137, 1984.zbMATHMathSciNetGoogle Scholar
  3. [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
  4. [BW90]
    J. C. M. Baeten and W. P. Weijland. Process Algebra. Cambridge Tracts in Computer Science 18, Cambridge University Press, 1990.Google Scholar
  5. [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
  6. [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
  7. [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
  8. [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
  9. [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
  10. [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
  11. [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
  12. [Mil80]
    R. Milner. A Calculus of Communicating Systems. Volume 92 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1980.Google Scholar
  13. [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
  14. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • J. C. M. Baeten
    • 1
  • J. A. Bergstra
    • 2
  • S. A. Smolka
    • 3
  1. 1.Dept. of Math and Computing ScienceEindhoven University of TechnologyMB EindhovenThe Netherlands
  2. 2.Programming Research GroupUniversity of AmsterdamDB AmsterdamThe Netherlands
  3. 3.Department of Computer ScienceSUNY at Stony BrookStony BrookUSA

Personalised recommendations