• 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

Theorem: Input/Output Equivalence

Simulation between two machines indicates that one abstracts the other. Bisimulation indicates that they have equivalent input/output behavior. These results rest on the following theorem and corollary:

Theorem. Let B simulate A.Then

Behaviors_A ⊂ Behaviors_B.

Intuitively, the theorem simply states that B can match every move of A and produce the same output sequence. It also implies that if B cannot produce a particular output sequence, then neither can A. This is stated formally in the following corollary.

Corollary. Let B simulate A.Then if (x, y) ∉ Behaviors_B then (x, y) ∉ Behaviors_A.