Abstract.
In this thesis we present three mathematical frameworks for the modelling
of reactive probabilistic communicating processes. We first introduce generalised
labelled transition systems as a model of such processes and introduce an
equivalence, coarser than probabilistic bisimulation, over these systems.
Two processes are identified with respect to this equivalence if, for all
experiments, the probabilities of the respective processes passing a given
experiment are equal. We next consider a probabilistic process calculus including
external choice, internal choice, action-guarded probabilistic choice,
synchronous parallel and recursion. We give operational semantics for this
calculus be means of our generalised labelled transition systems and show
that our equivalence is a congruence for this language.
Following the methodology introduced by de Bakker & Zucker, we then give denotational semantics to the calculus by means of a complete metric space of probabilistic processes. The derived metric, although not an ultra-metric, satisfies the intuitive property that the distance between two processes tends to 0 if a measure of the differences of their observable behaviour also tends to 0. We show that the denotational model is fully abstract with respect to our equivalence. We also provide a logical characterisation of the process equivalence by means of a variant of the quantitative Hennessy-Milner Logic (HML), where each HML formula is interpreted as the probability of it being satisfied by the process instead of the usual truth value. Two processes are then shown equivalent if, and only if, they agree on the quantities assigned to all HML formulae. |