Closing a System in the Dynamic Input/Output Automata Model
Tatjana Kapus · The Computer Journal · 2010
By definition, an input/output (or I/O) automaton is closed if there are no input actions in its action signature, and open otherwise. The dynamic I/O automata (DIOA) model is a special kind of the I/O automata one in which automata can be created and destroyed dynamically, and automata action signatures can change from state to state. In this paper, we draw attention to the possibility that a DIOA model of a system is open in the sense of the above definition although it seems to the specifier to be closed. This can be the reason why some expected properties cannot be proved to hold for the system. We, therefore, introduce a restriction operator for DIOA to help obtain a closed model in which the expected system properties could be verified.