Input-Output Automata

The input/output automaton model, developed by Lynch and Tuttle, is a labelled transition system model for components in asynchronous concurrent systems. The actions of an I/O automaton are classified as input, output and internal actions, where input actions are required to be always enabled. An I/O automaton has "tasks"; in a fair execution of an I/O automaton, all tasks are required to get turns infinitely often. The behavior of an I/O automaton is describable in terms of traces, or alternatively in terms of fair traces. Both types of behavior notions are compositional.

The standard introductory reference for I/O automata is the CWI paper by Lynch and Tuttle. All the details appear in Tuttle's M.S. thesis. A summary of the thesis appears in a 1987 PODC paper. A nice description of the model appears in Chapter 8 of Lynch's book, Distributed Algorithms.

The book Distributed Algorithms contains many algorithms and their proofs, all described in terms of I/O automata. I/O automata are used to model both shared memory and message-passing algorithms. The book Atomic Transactions contains algorithms for database concurrency control and abort recovery, again in terms of I/O automata. Other uses of I/O automata are sprinkled throughout the literature on distributed algorithms.

TOC / LCS / MIT
Last modified: February 26, 2002 Comments?