Gavin Lowe
1992, 66pp.
In TR-24-91 we presented a probabilistic model of timed CSP, which was based upon a deterministic language with prioritized operators, augmented with a probabilistic choice operator. We gave a semantic model for this language which gave the probabilities of different behaviours occurring.
In this paper we study methods of specifying and proving correct probabilistic processes. We want to be able to prove that, whatever the environment offers, the probability of a behaviour of a process satisfying some predicate is at least some value p. For example, we will be able to prove specifications such as "the protocol correctly transmits messages within 3 seconds with probability at least 90%".
We present a number of proof rules that can be used for proving that a process meets a specification; for compound processes, the proof obligation is reduced to proof obligations upon the subcomponents.
Unfortunately, proofs of probabilistic processes are harder than those for non-probabilistic processes: there are a number of factors which complicate matters. We examine these factors and show how they can be dealt with.
We illustrate the proof system by applying it to a protocol transmitting data over an unreliable medium, and derive the probability of messages being correctly transmitted within a given time.