Abstract
We connect probabilistic Action Systems and probabilistic CSP, inducing healthiness conditions for the probabilistic traces, failures and divergences of the latter.
A probabilistic sequential semantics for pGCL [31] is “inserted underneath” an existing but non-probabilistic link between action systems and CSP. Thus the link, which earlier yielded the classic CSP healthiness conditions [34], is induced to produce probabilistic versions of them “for free”.
Although probabilistic concurrency has enjoyed the attentions of a very large number of researchers over many years—including ourselves [37]—we nevertheless hope to gain new insights by combining the two approaches CSP and pGCL. In the meantime, however, we probably raise more questions than we answer: in particular, the issue of compositionality—for the moment—remains as delicate as ever.
We retrace the path of an earlier work [34].
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Abrial, J.-R.: Extending B without changing it (for developing distributed systems). In: Habrias, H. (ed.) First Conference on the B Method, November 1996, pp. 169–190. Laboratoire LIANA, L’Institut Universitaire de Technologie (IUT) de Nantes (1996)
Back, R.-J.R., Butler, M.J.: Fusion and simultaneous execution in the refinement calculus. Acta Informatica 35(11), 921–949 (1998)
Back, R.-J.R., Kurki-Suonio, R.: Decentralisation of process nets with centralised control. In: 2nd ACM SIGACT-SIGOPS Symp. Principles of Distributed Computing, pp. 131–142 (1983)
Butler, M.J.: A CSP approach to action systems. Technical report, Oxford University, DPhil Thesis (1992)
Butler, M.J.: csp2B: A practical approach to combining CSP and B. Formal Aspects of Computing, 182–196 (2000)
Butler, M.J., Morgan, C.C.: Action systems, unbounded nondeterminism and infinite traces. Formal Aspects of Computing 7(1), 37–53 (1995)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)
Davies, J.W., Roscoe, A.W., Woodcock, J.C.P. (eds.): Millennial Perspectives in Computer Science, Palgrave. Cornerstones of Computing (2000)
de Nicola, M., Hennessy, M.: Testing equivalence for processes. Theoretical Computer Science 34 (1984)
Dijkstra, E.W.: A Discipline of Programming. Prentice Hall International, Englewood Cliffs (1976)
He, J.: Process refinement. In: McDermid, J. (ed.) The Theory and Practice of Refinement, Butterworths (1989)
He, J.: Process simulation and refinement. Formal Aspects of Computing 1(3), 229–241 (1989)
He, J., Seidel, K., McIver, A.K.: Probabilistic models for the guarded command language. Science of Computer Programming 28, 171–192 (1997) Available at [30 key HSM95]
Hesselink, W.H.: Programs, Recursion and Unbounded Choice. Cambridge Tracts in Theoretical Computer Science, vol. 27. Cambridge University Press, Cambridge (1992)
Ho-Stuart, C.: Private communication (1996)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–583 (1969)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs (1985)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)
Jones, C.: Probabilistic nondeterminism. Monograph ECS-LFCS-90-105, Edinburgh University, Ph.D. Thesis (1990)
Jones, C., Plotkin, G.: A probabilistic powerdomain of evaluations. In: Proceedings of the IEEE 4th Annual Symposium on Logic in Computer Science, pp. 186–195. Computer Society Press, Los Alamitos (1989)
Jonsson, B., Ho-Stuart, C., Yi, W.: Testing and refinement for nondeterministic and probabilistic processes. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 418–430. Springer, Heidelberg (1994)
Josephs, M.B.: A state-based approach to communicating processes. Distributed Computing 3(1), 9–18 (1988)
Kozen, D.: Semantics of probabilistic programs. Jnl. Comp. Sys. Sciences 22, 328–350 (1981)
Kozen, D.: A probabilistic PDL. Jnl. Comp. Sys. Sciences 30(2), 162–178 (1985)
Lowe, G.: Probabilities and priorities in timed CSP. Technical Monograph PRG-111, Oxford University Computing Laboratory, DPhil Thesis (1993)
Lowe, G.: Representing nondeterministic and probabilistic behaviour in reactive processes (1993), web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/prob.html
McIver, A.K., Morgan, C.C.: Games, probability and the quantitative μ-calculus qMu. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 292–310. Springer, Heidelberg (2002)
McIver, A.K., Morgan, C.C.: Results on the quantitative μ-calculus qMμ. ACM Trans. Comp. Logic (2004) provisionally accepted
McIver, A.K., Morgan, C.C., Sanders, J.W.: Probably Hoare? Hoare probably! In: Davies., et al. (eds.) [8], pp. 271–282.
McIver, A.K., Morgan, C.C., Sanders, J.W., Seidel, K.: Probabilistic Systems Group: Collected reports, web.comlab.ox.ac.uk/oucl/research/areas/probs/bibliography.html
McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Technical Monographs in Computer Science. Springer, Heidelberg (2004)
Mislove, M.: Nondeterminism and probabilistic choice: Obeying the laws, math.tulane.edu/~mwm/
Morgan, C.C.: The specification statement. ACM Transactions on Programming Languages and Systems 10(3), 403–419 (1988) Reprinted in [39]
Morgan, C.C.: Of wp and CSP. In: Feijen, W.H.G., van Gasteren, A.J.M., Gries, D., Misra, J. (eds.) Beauty is Our Business. Springer, Heidelberg (1990)
Morgan, C.C., McIver, A.K.: pGCL: Formal reasoning for random algorithms. South African Computer Journal 22 (1999), Available at [30 key pGCL]
Morgan, C.C., McIver, A.K., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18(3), 325–353 (1996), doi.acm.org/10.1145/229542.229547
Morgan, C.C., McIver, A.K., Seidel, K., Sanders, J.W.: Refinement-oriented probability for CSP. Formal Aspects of Computing 8(6), 617–647 (1996)
Morgan, C.C., McIver, A.K.: Cost analysis of games using program logic. In: Proc. 8th Asia-Pacific Software Engineering Conference (APSEC 2001) (December 2001), Abstract only: full text available at [30 Key MDp01]
Morgan, C.C., Vickers, T.N. (eds.): On the Refinement Calculus. FACIT Series in Computer Science. Springer, Berlin (1994)
Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming 9(3), 287–306 (1987)
Nelson, G.: A generalization of Dijkstra’s calculus. ACM Transactions on Programming Languages and Systems 11(4), 517–561 (1989)
Pnueli, A.: Linear and branching structures in the semantics and logics of reactive systems. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 15–32. Springer, Heidelberg (1985)
Roscoe, A.W., Reed, G.M., Forster, R.: The successes and failures of behavioural models. In: Davies., et al. (eds.) [8].
Seidel, K.: Probabilistic communicating processes. Technical Monograph PRG-102, Oxford University, DPhil Thesis (1992)
Woodcock, J.C.P., Morgan, C.C.: Refinement of state-based concurrent systems. In: Langmaack, H., Hoare, C.A.R., Bjorner, D. (eds.) VDM 1990. LNCS, vol. 428, pp. 340–351. Springer, Heidelberg (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Morgan, C. (2005). Of Probabilistic wp and CSP—and Compositionality. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds) Communicating Sequential Processes. The First 25 Years. Lecture Notes in Computer Science, vol 3525. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11423348_12
Download citation
DOI: https://doi.org/10.1007/11423348_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25813-1
Online ISBN: 978-3-540-32265-8
eBook Packages: Computer ScienceComputer Science (R0)