×

Probabilistic communicating processes. (English) Zbl 0872.68111

Summary: We explore the suitability of two semantic spaces as a basis for a probabilistic variant of the language of Communicating Sequential Processes (CSP), so as to provide a formalism for the specification and proof of correctness of probabilistic algorithms. The two spaces give rise to two sublanguages, each of which is characterised by an algebraic axiomatisation which is shown to be sound and complete for finite processes. In the first semantics, processes are defined as probability measures on the space of infinite traces and operators are defined as functions (mostly transformations) of probability measures. The advantage of this semantics is that it is simple and good for reasoning about probabilistic properties such as self-stabilisation or fairness of random algorithms. The disadvantage is that neither external choice nor parallel composition other than fully synchronised parallel composition can be defined in this semantics. This problem is solved in the second model which is based on the space of conditional probability measures of infinite traces. This model leads to a set of proof rules for the deterministic properties of probabilistic algorithms, but it is more difficult to use in the analysis of probabilistic properties. The last part of the paper shows how the two models are related and how this can be exploited to combine their advantages and get around their disadvantages. This is illustrated by the example of a self-stabilising tokenring.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing

Software:

UNITY
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Alpern, B.; Schneider, F. B., Defining liveness, Inform. Process. Lett., 21, 181-185 (1985) · Zbl 0575.68030
[2] Billingsley, P., Probability and Measure (1979), Wiley: Wiley New York · Zbl 0411.60001
[3] Chandy, K. M.; Misra, J., Parallel Program Design: A Foundation (1988), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0717.68034
[4] Davies, J., Specification and proof in real-time systems, Oxford University D. Phil Thesis (1991)
[5] J. Davies and S. Schneider, Recursion induction for real-time processes, Formal Aspects Computing, to appear.; J. Davies and S. Schneider, Recursion induction for real-time processes, Formal Aspects Computing, to appear. · Zbl 0806.68073
[6] Feller, W., (An Introduction to Probability Theory and its Applications, Vol. I (1957), Wiley: Wiley New York) · Zbl 0077.12201
[7] van Glabbeek, R. J.; Smolka, S. A.; Steffen, B.; Tofts, C., Reactive, generative and stratified models of probabilistic processes, (IEEE Symp. on Logic in Computer Science. IEEE Symp. on Logic in Computer Science, Philadelphia, PA, USA (1990)) · Zbl 0832.68042
[8] Herman, T., Probabilistic self-stabilization, Inform. Process. Lett., 35, 63-67 (1990) · Zbl 0697.68027
[9] Hoare, C. A.R, Communicating Sequential Processes (1985), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[10] ISO, LOTOS: a formal description technique based on the temporal ordering of observational behaviour, IS 8807, TC97/SC21 (1989)
[11] Jones, C.; Plotkin, G., A probabilistic powerdomain of evaluations, (Proc. 4th Ann. Symp. on Logic in Computer Science (1989)) · Zbl 0716.06003
[12] Jou, C.; Smolka, S. A., Equivalences, congruences, and complete axiomatizations for probabilistic processes, (Concur 90, Theories of Concurrency, Unification and Extension. Concur 90, Theories of Concurrency, Unification and Extension, Lecture Notes in Computer Science, Vol. 458 (1990), Springer: Springer Berlin)
[13] Larsen, K. G.; Skou, A., Bisimulation through probabilistic testing, (Proc. 16th ACM Symp. on Principles of Programming Languages. Proc. 16th ACM Symp. on Principles of Programming Languages, Austin, TX (1989)) · Zbl 0756.68035
[14] LOTOS extended with probabilistic behaviours. LOTOS extended with probabilistic behaviours, Formal Aspects Computing, 5, 3 (1993) · Zbl 0774.68038
[15] Milner, R., Communication and Concurrency (1989), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[16] Pnueli, A., On the extremely fair treatment of probabilistic algorithms, (Proc. 15th Ann. Symp. on the Theory of Computing (1983)), 278-290
[17] Rao, J. R., Reasoning about probabilistic parallel programs, ACM Trans. Programming Languages Systems, 16, 3 (1994)
[18] Reed, G. M., A uniform mathematical theory for real-time distributed computing, Oxford University D. Phil Thesis (1988)
[19] Roscoe, A. W., A mathematical theory of communicating processes, Oxford University D. Phil Thesis (1982)
[20] Seidel, K., Probabilistic communicating processes, Oxford University Computing Laboratory, Technical Monograph PRG-102 (1992)
[21] Shiryayev, A. N., Probability (1984), Springer: Springer Berlin
[22] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math., 5, 285-309 (1905) · Zbl 0064.26004
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.