• Home
•  Up to Topics
•  Previous
•  Next

Week 4

• Nondeterminism
• Example
• Model
• Possible updates
• Relations
• Abstraction
• Equivalence
• Simulation
• Deterministic
• Abstraction
• Nondeterministic
• Behaviors
• Theorem
• Not theorem
• Uses
• Bisimulation
• Examples

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.