PCSP: a denotational model of probabilistic processes

Abstract

We present a model of probabilistic processes, which is an extension of CSP, on the basis of replacing internal non-determinism by generative probabilistic choices, and external non-determinism by reactive probabilistic choices. Our purpose when defining the model has been to maintain, as far as possible, the meaning of all the operators in classical CSP, generalizing them in a probabilistic way. Thus we try to keep valid (once probabilistically generalized), as far as possible, the laws of CSP. It is the combination of both internal and external choice that makes strongly difficult the definition of a probabilistic version of CSP. We can find in the literature quite a number of papers on probabilistic processes, but only in a few of them internal and external choices are combined trying to preserve their original meaning. The denotational semantics here presented is based on a domain of probabilistic trees with two kinds of nodes, representing the internal and external choices, the root being an internal one, which generalizes in a very natural way the corresponding trees for nonprobabilistic process algebras. We present also a testing semantics fully abstract with respect to our denotational semantics.