Input/output automaton

Input/output automata provide a formal model, applicable in describing most types of an asynchronous concurrent system. On its own, the I/O automaton model contains a very basic structure that enables it to model various types of distributed systems. To describe specific types of asynchronous systems, additional structure must be added to this basic model. The model presents an explicit method for describing and reasoning about system components such as processes and message channels that interact with one another, operating at arbitrary relative speeds. The I/O automata were first introduced by Nancy A. Lynch and Mark R. Tuttle in "Hierarchical correctness proofs for distributed algorithms", 1987. "An I/O automaton models a distributed system component that can interact with other system components. It is a simple type of state machine in which the transitions are associated with named actions." There are three types of actions: input, output, and internal actions. The automaton uses its input and output actions to communicate with its environment, whereas the internal actions are only visible to the automaton itself. Unlike internal and output actions that are selected and carried out by the automaton, the input actions – which simply arrive from the environment - are not under automaton's control. I/O automata can be used to model individual components of a distributed system, such as a process, a message channel in a message passing system, or a shared data structure in a shared memory systems. Figure 1 depicts an example of an I/O automaton for a process in an asynchronous message-passing distributed system. In this setting, process Pi communicates with other processes by using a message passing system. Its output actions are of the form send(m)i,j, which represents process Pi sending a message with contents m to process Pj. The input actions are of form receive(m)k,i, representing the receipt of message with contents m by process Pi from process Pk. (The internal actions of Pi, which would correspond to the algorithm that the process is running are not shown.