Dynamic input/output automata, a formal model for dynamic systems
Paul C. Attie, Nancy Ann Lynch · 2001
We present a mathematical state-machine model, the Dynamic I/O Automaton (DIOA) model, for defining and analyzing dynamic systems of interacting components. The systems we consider are dynamic in two senses: (1) components can be created and destroyed as computation proceeds, and (2) the set of events in which a component may participate can change as computation proceeds. The new model admits a notion of external system behavior, based on sets of traces. It also features a parallel composition operator for dynamic systems, which satisfies standard execution projection and pasting results, and a notion of simulation from one dynamic system to another, which can be used to prove that one system implements the other.