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.
Examples
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.
Process I/O automaton
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.)
FIFO message channel
A message channel can also be modeled by an I/O automaton. Figure 2 illustrates a typical unidirectional FIFO channel automaton, named Ci,j. It has input actions of the form send(m)i,j, and output actions of the form receive(m)i,j. Each message m may contain 0 or 1 (m ∈ {0,1}). The state of the automaton stores a FIFO queue of all messages that have been sent but not yet received.
In a typical distributed system where both process automata and communication channel automata exist, they are composed in a way that output actions of one automaton are matched and executed with identically-named input actions of the other automata. For example, consider a system composed of two process, Pi and Pj, and a communication channel Ci,j from process Pi to process Pj. In this setting, process Pi executes the output action send(m)i,j, if and only if channel Ci,j also executes its send(m)i,j input action.
Atomic read/write register
Figure 3 illustrates an atomic read/write register I/O automaton in a shared memory system with two processes, P1 and P2. The value V stored in the register is of type integer (V ∈ Z). The state of the automaton stores this value. Input actions consist of writei(V), which represents process Pi requesting to write a value V to the register (where i ∈ {1,2} and V ∈ Z), and readi, which corresponds to a process Pi requesting to read the value currently stored in the register. The output action acki is used to inform process Pi that the write request has successfully completed. The output action Vi represents the value V being returned as a response to a read request by process Pi.
The automaton also includes internal actions perform_Write(V), which writes the value V to the register (by updating the state of the automaton), and perform_Read, which is used to read the value V stored in the state. (These internal actions are not shown in Figure 3.)
Formal specification An I/O automaton A, or simply an automaton, comprises five components: sig(A) states(A) start(A) trans(A) tasks(A)
These five components are described below.
Signature The initial step in formalization of an I/O automaton A is the definition of its signature, sig(A). A signature S describes the I/O automaton's actions using three disjoint sets of actions: in(S): input actions, out(S): output actions, and int(S): internal actions.
Based on the above formalization of input, output and internal actions, it is possible to define the following objects.
ext(S): the external actions, defined as in(S) ∪ out(S) local(S): the locally controlled actions, defined as out(S) ∪ int(S) extsig(S): the external signature, defined as (in(S), out(S), ø) acts(S) is defined as the set of all the actions of signature S.
States The set of states of automaton A, denoted states(A), need not be finite. This is a significant generalization of the usual notion of finite automata, as it enables modeling systems with unbounded data structures like counters and unbounded length queues. The set of start states (also known as initial states) is a non-empty subset of states. Multiple start states are allowed so that some input information can be included in the start states.
Transition relation The state-transition relation of automaton A is denoted trans(A) ⊆ states(A) × acts(sig(A)) × states(A). It satisfies the property that "for every state s and every input action π, there is a transition (s, π, s') ∈ trans(A)."
A transition, also known as a step of I/O automaton A, is defined as an element (s, π, s') of trans(A). An input transition refers to a transition (s, π, s') when π is an input action, output transition indicates a transition (s, π, s') when π is an output action and so on. For any state s and action π, if the I/O automaton A has some transition of the form (s, π, s'), then π is said to be enabled in s. I/O automata are described as input-enabled because all input actions are required to be enabled in every state. A quiescent state s is defined as a state where only input actions are enabled.
Tasks The fifth component of the I/O automaton A, tasks (A), is a task partition, defined as an equivalence relation on locally controlled actions of A, which has at most countably many equivalence classes. Informally, the task partition tasks(A), represents an abstract description of "tasks," or "threads of control," within A.
This partition is used to define fairness conditions on an execution of the automaton. These conditions require the automaton to continue giving fair turns to each of its tasks during its execution. This is particularly helpful when modelling a system component that performs multiple jobs. For instance, a component that participates in an ongoing algorithm while periodically reporting status information to its environment simultaneously would have two tasks. The partition is also useful when several automata are composed (to produce a larger system automaton) when specifying that all the automata in the composition continue to take steps in the composed system.
Example: Formal definition of channel I/O automaton As described above, Ci,j is an example of I/O automaton that represents a unidirectional FIFO channel from process Pi to process Pj. Let m be a binary message: m ∈ {0,1}. The automaton Ci,j can be formally defined as follows.
Signature:
sig(Ci,j) specifies that the automaton has two kinds of actions: An input action of (Ci,j) is of the form send(m)i,j, where m ∈ {0,1}. An output action of (Ci,j) is of the form receive(m)i,j, where m ∈{0,1}.
Intuitively, the action send(m)i,j indicates that a message m has entered the channel when it is sent by process Pi and the action receive(m)i,j indicates that a message m has left the channel when it is delivered to process Pj.
States:
states(Ci,j) is the set of all finite sequences of elements m ∈ {0,1}. Intuitively, the state represents the sequence of messages currently en route from the sender, process Pi, to the receiver, process Pj, in the order they were sent.
start(Ci,j), representing the initial states of the queue, contains only the empty sequence.
Transitions
The transition relation can be modelled in a precondition-effect style, where all the transitions that include each specific type of action are grouped into a single piece of code. In this code, the conditions which must be satisfied before allowing an action to occur, are formalized as a predicate on the pre-state s, which is the state before the action occurs. Consequent changes to the state that result from the execution of the action are coded in the form of a simple program. This program is executed indivisibly, as a single transition. If this program is applied to the state s, the new state s' results.
The transitions of Ci,j are described as:
for send(m)i,j: Precondition: None Effect: m is added to the end of the sequence stored in the state (where m ∈ {1,0})
for receive(m)i,j: Precondition: m is the first element in the sequence stored in the state (where m ∈ {1,0}) Effect: remove the first element of the sequence stored in the state
Intuitively, the send action can be executed any time; it causes the addition of the message m to the end of the queue of messages in che channel. The receive action removes and returns the first element of the queue.
Tasks
tasks(Ci,j), represents a task partition that groups together all actions of form receive into a single task. Intuitively, handing over messages to process Pj is considered as a single task.
{receive(m)i,j : m ∈ {0,1}}.
Execution and trace
Execution In a run of an automaton, a string is generated that describes the behaviour of the component the automaton models. "An execution fragment of I/O Automaton A is either
a finite sequence, s0, π1, s1, π2,... , πr, sr, or an infinite sequence, s0, π1, s1,π2,...,πr,sr,...,
of alternating states and actions of A such that (sk, πk+1, sk+1) is a transition of A for every k ≥ 0."
A finite sequence must terminate with a state. An execution is defined as an execution fragment that begins with start state. The set of executions of A is represented by execs(A). A reachable state in I/O automaton A is the final state of a finite execution of A.
Assume α is a finite execution fragment of A ending with state sf. Assume further that α' is any execution fragment of A that begins with sf, the last state of α. In this case, the sequence produced by concatenating α and α', and eliminating the duplicate occurrence of sf, the last state of α, is represented by α.α' . This sequence is also an execution fragment of I/O automaton A.
Trace A trace of an I/O automaton A is the sequence of external actions that occurs in some execution α of A. The set of all traces of A is represented as traces(A).
Example: Three executions Executions a, b and c are three executions of the automaton Ci,j described in Formal Definition of Channel I/O Automaton (where message m ∈ {0, 1}). In this example, the states are indicated by putting the sequence of messages in queue in brackets; the empty sequence is represented by λ.
(a) [λ], send(1)i,j, , receive(1)i,j, [λ], send(0)i,j, , receive(0)i,j, [λ] (b) [λ], send(1)i,j, , receive(1)i,j, [λ], send(0)i,j, (c) [λ], send(1)i,j, , send(1)i,j, , send(0)i,j, ....
Operations on automata
Composition operation