Showing Equivalence

How do you show whether two machines are equivalent or not? There are two general approaches you can take. First, you could work within just the semantic domain

and show that the two semantic entities, in this case quadruples, are equivalent. If your notion of equivalence is not defined directly in terms of quadruples, but rather behavior sets then your semantic domain would be behavior sets and you'd have to show equivalence between two behavior sets, which might require showing equivalence between traces, etc..

Or, second, you could work within the syntactic domain

and show that the two syntactic descriptions, e.g., pre/post-condition specifications, Z specifications, or CSP programs, are equivalent in some sense. For example, for two different pre/post-condition specifications or two different Z specifications you might show that each of the predicates of one implies the corresponding predicate of the other and vice versa. For CSP programs, you might use properties of process algebras to show equivalence. Since the two syntactic descriptions are ``the same,'' then they denote the same semantic entity, in this a case a quadruple representing a state machine; thus, they must describe the same state machine.

Another way to categorize how we might show the equivalence between two machines is as follows:

• Show equivalence from first principles using mathematical logic, theories of sets and sequences, induction, etc. Since equality on sets, sequences, integers, booleans, and other primitive types is mathematically well-defined, if you beat everything down to these primitive types, then you have a way of showing equivalence. This technique could be used if you wanted to show the equivalence of two quadruples.
• Show one ``simulates'' the other and vice versa. Anything I can do in one machine has some equivalent action or sequence of actions in the other. For example, if you wanted to show that one behavior set is the same as the other, then you might use this approach.
• Transform one into the other. For example, if you wanted to show that one state machine description is ``the same'' as the other, you might use this approach. Showing that compiled code is ``correct'' amounts to showing that the transformed code is ``the same'' as the original code.