EECS20N: Signals and Systems

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.