Introduction

The history of bisimulation is well documented in earlier chapters of this book. In this chapter we will look at a major non-trivial extension of the theory of labelled transition systems: probabilistic transition systems. There are many possible extensions of theoretical and practical interest: real-time, quantitative, independence, spatial and many others. Probability is the best theory we have for handling uncertainty in all of science, not just computer science. It is not an idle extension made for the purpose of exploring what is theoretically possible. Non-determinism is, of course, important, and arises in computer science because sometimes we just cannot do any better or because we lack quantitative data from which to make quantitative predictions. However, one does not find any use of non-determinism in a quantitative science like physics, though it appears in sciences like biology where we have not yet reached a fundamental understanding of the nature of systems.

When we do have data or quantitative models, it is far preferable to analyse uncertainty probabilistically. A fundamental reason that we want to use probabilistic reasoning is that if we merely reported what is possible and then insisted that no bad things were possible, we would trust very few system designs in real life. For example, we would never trust a communication network, a car, an aeroplane, an investment bank nor would we ever take any medication! In short, only very few idealised systems ever meet purely logical specifications. We need to know the ‘odds’ before we trust any system.