Axiomatizing probabilistic processes: ACP with generative probabilities
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 − .
KeywordsAxiom System Probabilistic Process Stratify Model Probabilistic Version Complete Axiomatization
Unable to display preview. Download preview PDF.
- [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
- [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