We have extended a computer based tool for verification of relations between probabilistic and non-probabilistic processes with a language for probabilistic processes.
The language includes composition and abstraction constructs, with which communication between probabilistic processes can be modelled and irrelevant details hidden.
Using the language and the verification tool, we have modelled and analysed examples from the areas of operating and fault-tolerant systems.
DoCS M.Sc. thesis 91/29, June 1991 (Not available electronically)