# Process Algebra with Probabilistic Choice

## Abstract

Published results show that various models may be obtained by combining parallel composition with probability and with or without non-determinism. In this paper we treat this problem in the setting of process algebra in the form of *ACP*. First, probabilities are introduced by an operator for the internal probabilistic choice. In this way we obtain the Basic Process Algebra with probabilistic choice *prBPA*. After-wards, *prBPA* is extended with parallel composition to *ACP* _{π} ^{+} . We give the axiom system for *ACP* _{π} ^{+} and a complete operational semantics that preserves the interleaving model for the dynamic concurrent processes. Considering the PAR protocol, a communication protocol that can be used in the case of unreliable channels, we investigate the applicability of *ACP* _{π} ^{+} . Using in addition only the priority operator and the preabstraction operator we obtain a recursive specification of the behaviour of the protocol that can be viewed as a Markov chain.

## Keywords

Probability Distribution Function Operational Semantic Axiom System Probabilistic Choice Parallel Composition## Preview

Unable to display preview. Download preview PDF.

## References

- 1.S. Andova,
*Process algebra with interleaving probabilistic parallel composition*, Eindhoven University of Technology, CSR 99-xx, 1999.Google Scholar - 2.J.C.M. Baeten, J. A. Bergstra,
*Global renaming operators in concrete process algebra*, Information and Computation 78, pp. 205–245, 1988.MathSciNetCrossRefzbMATHGoogle Scholar - 3.J.C.M. Baeten, W. P. Weijland,
*Process algebra*, Cambridge University Press, 1990.Google Scholar - 4.J.C.M. Baeten, C. Verhoef,
*Concrete process algebra*, Handbook of Logic in Computer Science, volume 4: “Semantic Modelling”, Oxford University Press, 1995.Google Scholar - 5.J.C.M. Baeten, J.A. Bergstra,
*Process algebra with partial choice*, Proc. CONCUR’94, Uppsala, B. Jonsson & J. Parrow, eds., LNCS 836, Springer Verlag, pp. 465–480, 1994.Google Scholar - 6.J.C.M. Baeten, J.A. Bergstra, S.A. Smolka,
*Axiomatizing probabilistic processes: ACP with generative probabilities*, Information and Computation 121(2), pp. 234–255, Sep. 1995.MathSciNetCrossRefzbMATHGoogle Scholar - 7.J.A. Bergstra, J.W. Klop,
*Process algebra for synchronous communication*, Information and Control 60, pp. 109–137, 1984.MathSciNetCrossRefzbMATHGoogle Scholar - 8.P.R. D’Argenio, C. Verhoef,
*A general conservative extension theorem in process algebra with inequalities*, Theoretical Computer Science 177, pp. 351–380, 1997.MathSciNetCrossRefzbMATHGoogle Scholar - 9.P.R. D’Argenio, H. Hermanns, J.-P. Katoen
*On generative parallel composition*, Preliminary Proc. of PROBMIV’98, Indianopolis, USA, C. Baier & M. Huth & M Kwiatkowska & M. Ryan ed., pp. 105–121, 1998.Google Scholar - 10.A. Giacalone, C.-C. Jou, S. A. Smolka,
*Algebraic reasoning for probabilistic concurrent systems*, Proc. Working Conference on Programming Concepts and Methods, IFIP TC 2, Sea of Galilee, Israel, M. Broy & C.B. Jones ed., pp. 443–458, 1990.Google Scholar - 11.R.J. van Glabbeek, S. A. Smolka, B. Steffen, C. M. N. Tofts,
*Reactive, generative and stratified models of probabilistic processes*, Proc. of 5th Annual IEEE Symp. on Logic in Computer Science, Philadelphia, PA, pp. 130–141, 1990.Google Scholar - 12.H. Hansson,
*Time and probability in formal design of distributed systems*, Ph.D. thesis, DoCS 91/27, University of Uppsala, 1991.Google Scholar - 13.C.-C. Jou, S. A. Smolka
*Equivalences, congruences and complete axiomatizations for probabilistic processes*, Proc. CONCUR’ 90, LNCS 458, Springer Verlag, Berlin, pp. 367–383, 1990.Google Scholar - 14.K. G. Larsen, A. Skou,
*Bisimulation through probabilistic testing*, Proc. of 16th ACM Symp. on Principles of Programming Languages, Austin, TX, 1989.Google Scholar - 15.F.W. Vaandrager,
*Two simple protocols*, In:*Applications of Process algebra*, Cambridge University Press, J.C.M. Baeten ed., pp. 23–44, 1990.Google Scholar - 16.M.Y. Vardi,
*Automatic verification of probabilistic concurrent finite state programs*, Proc. of 26th Symp. on Foundations of Com. Sc., IEEE Comp. Soc. Press, pp. 327–338, 1985.Google Scholar - 17.C. Verhoef,
*A general conservative extension theorem in process algebra*, Proc. of PROCOMET’94, IFIP 2 Working Conference, San Miniato, E.-R. Olderog ed., pp. 149–168, 1994.Google Scholar