Feedback Composition

Consider two state machines connected with a feedback loop:

Assumption:

• Outputs_A Ì Inputs_B
• Outputs_B2 Ì Inputs_A2

Definition of the composition:

• States = States_A ´ States_B
• Inputs = Inputs_A1
• Outputs = Outputs_B1

updates function is found by iteration to a fixed point:

• Start with unknown on the feedback arc
• Foreach state machine:
  • If output can be determined, produce it
  • If state transition can be determined, take it
• Repeat until no progress is made.

Two possible outcomes:

• All outputs are determined
• Some signals are still unknown

In the latter case, the composition is ill formed.