COMPUTERS AND MORE

Often we want to know whether two systems described in this notation behave the same way. For example, perhaps we have a description of a specification which the system should satisfy, and also a description of the design of a system. We'd like to show that the actual design behaves the same way as the specification.

When can we say that two systems behave the same way? There are lots of choices, depending on what we mean by behaviour. We can start by observing that two systems certainly do not behave the same if one of them can perform some sequence of actions which the other is unable to perform. For example, if one of our systems is described as a.b.0, we can write

a.b.0 -- a --> b.0 -- b --> 0

meaning that a.b.0 can do action a and become b.0, and then b.0 can do action b and become 0. We say that the process a.b.0 has the trace (a,b). It's obvious that a.c.0 doesn't have this trace, so a.b.0 and a.c.0 do not have the same behaviour in this sense. We say that they are not may (or trace) equivalent. We define may equivalence by saying that two systems P and Q are may equivalent if they have exactly the same set of traces.

That's a good start, but sometimes it's not enough. Consider the following example:

A = a.A

B = a.B + a.0

What are the traces of A? Well, we found above that A can keep on doing action a for ever, so its traces are () (the empty trace) (a), (a,a), (a,a,a) and so on, for any number of "a"s you like.

What about B? B behaves either as a.B or as a.0. So the set of traces of B is the union of the set of traces of a.B and the set of traces of a.0. The set of traces of a.0 is just the empty trace () and (a). If we take the other branch, you see that B can also do all the other traces consisting of any number of "a"s. It's obvious that it can't do anything else, because there's no action mentioned in its definition apart from a.

Therefore both A and B have the same set of traces, namely, they can do the traces consisting of doing any number of "a"s in succession including 0. A and B are may equivalent.

However, would we be happy if A were the specification of a system to be built and B were a proposed design? Probably not: because in the specification, the system has no choice but to go on doing "a"s for ever. In particular, the specified system cannot deadlock: it cannot reach a state where it is impossible for it to do anything. However, B can deadlock, just by choosing the right hand option and behaving as a.0, which will do just one a and then won't be able to do anything ever again.

This is an argument for deciding that A and B do not behave the same, even though they are may equivalent. Therefore we need a finer -- more detailed -- definition of what it means for two systems to behave the same. How else could we define behaviour? You might like to think of some options, and investigate the advantages and disadvantages of your choices. There is no one right answer.