Rationale

Why does this proof technique make sense? The technique should smell familiar. It's inductive in nature. There's a base case (``for each initial state '') and an inductive step, defined in terms of all possible action instances (``for each state transitions ''). As before, because the action sets are finite, we can do a big case analysis, one action per case, in the inductive step.

• In the base step, notice there is no requirement that all initial states of the abstract machine be covered. So, there may be some abstract executions that have no corresponding concrete execution since we could not even get started. This is okay since we only need to show a subset relationship between behavior sets.
• The intuition behind the inductive step is that if a state transition can occur in the concrete machine then it must be allowed to occur in the abstract machine. If we show the inductive step for all state transitions in the concrete machine, then we will have shown it for all of its possible executions. (Notice that in showing the commuting diagram for each action of the concrete machine, we are really showing it for each state transition that involves that action.)

After showing the base case and inductive step, we will have shown that each trace in the behavior set of the concrete machine has a corresponding (modulo the abstraction function) trace in the behavior set of the abstract machine. Hence, the behavior set of the concrete machine is a subset of the behavior set of the abstract machine (modulo the abstraction function), which is what we needed to prove.

Aside: In our proof technique, because of our simplistic way of associating actions in one machine to another (through the one-to-one function ) we are associating a single state transition in C to a single state transition in A. More generally, a state transition in C might map to a sequence of transitions in the abstract machine A. This generalization is especially needed for proving concurrent state machines correct and/or dealing with state machines with internal as well as external actions. We won't be using this generalization at all.