Feedback Composition
Consider two state machines connected with a feedback loop:
Assumption:
- OutputsA ⊂ InputsB
- OutputsB2 ⊂ InputsA2
Definition of the composition:
- States = StatesA × StatesB
- Inputs = InputsA1
- Outputs = OutputsB1
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.