Consider the two state machines,
each denoting a behavior set, Beh(C) and Beh(A), respectively.
We take an event-based view of trace: Each trace is a sequence of
(invocation, response)
pairs and each pair represents a single execution of one of the
actions provided by the machine.
We assume for simplicity that there is a one-to-one correspondence
between the action names in the concrete machine to those in the abstract
machine and that we use a renaming function, 
, to define the
relationship:
Using we can relate each state transition involving
a C action to a state transition involving an A action.
We define the satisfies relation as follows between two state machines as follows:
Since Beh(C) is a set of traces and Beh(A) is a set of traces, the satisfies relation is satisfied if every trace in Beh(C) is in Beh(A). This means that A's set can be larger; C's set reduces the choices of possible acceptable behaviors.
Why does this definition of satisfies make sense? Viewing C as an implementation of a design specification A, this definition says that an implementor makes decisions that restrict the scope of the freedom allowed by a design. In other words, the specification is saying what may or is permitted to occur at the implementation level, not what must occur. The implementation narrows down the choice of what is allowed to happen. For example, an implementation might reduce the amount of nondeterminism allowed by the specification.
Thus, certainly having the behavior sets equal (Beh(C) = Beh(A)) is
too strong. Having the subset relation go the other way ( 
) cannot be right either; otherwise there may be
executions of the concrete machine that are not permitted by the
abstract one.
According to this definition of correctness the concrete machine with the empty behavior would be a perfectly acceptable implementation of an abstract machine. Since the empty behavior is not very satisfying, we normally assume that the set of initial states and the state transition function for the concrete machine are both non-empty; thus its behavior is non-empty.
The empty behavior case is the extreme case where the concrete machine
does not do anything bad (a safety property) since it does not do anything at all; however, the machine also
does not do anything good (a liveness property). Our
definition of satisfies does not require that our machine do
anything; the definition requires only that the machine does only allowed things.