3 - Behavioural equivalences

Summary

We have previously remarked that CCS, like all other process algebras, can be used to describe both implementations of processes and specifications of their expected behaviours. A language like CCS therefore supports the so-called single-language approach to process theory – that is, the approach in which a single language is used to describe both actual processes and their specifications. An important ingredient of these languages is therefore a notion of behavioural equivalence or behavioural approximation between processes. One process description, say SYS, may describe an implementation and another, say SPEC, may describe a specification of the expected behaviour. To say that SYS and SPEC are equivalent is taken to indicate that these two processes describe essentially the same behaviour, albeit possibly at different levels of abstraction or refinement. To say that, in some formal sense, SYS is an approximation of SPEC means roughly that every aspect of the behaviour of this process is allowed by the specification SPEC and thus that nothing unexpected can happen in the behaviour of SYS. This approach to program verification is also sometimes called implementation verification or equivalence checking.

Criteria for good behavioural equivalence

We have already argued informally that some processes that we have met so far ought to be considered as behaviourally equivalent.