How do we show the satisfies relationship holds between
two state machines?
Given our two state machines,
and
,
in general it is not
so straightforward to determine if C satisfies A because
their state sets, 
and 
, may be different.
The proof technique we present uses an abstraction function
to relate these state sets
.