# Using Simulation Relations

Suppose we have a complicated deterministic state machine *A*. We wish
to show that its input-output function satisfies some property. That is, every
behavior satisfies some condition.

We construct a simpler nondeterministic machine *B* whose input-output
relation satisfies the same property, where *B* simulates *A*. The
theorem guarantees that *A* will satisfy this property, too. That is, since
all behaviors of *B* satisfy the property, all behaviors of *A* must
also.

Conversely, if there is some property that we must assure that no behavior
of *A* has, it is sufficient to show that no behavior of the simpler machine
*B* has it. This scenario is typical of a **safety** problem, where
we must show that dangerous outputs from our system are not possible.