This paper introduces the input-output automaton model for asynchronous distributed algorithms, enabling modular and hierarchical correctness proofs. The model allows for the formalization of high-level algorithmic ideas and their rigorous simulation at lower levels. The authors present a hierarchical approach to proving the correctness of Schönhage's distributed arbiter algorithm, which manages resource allocation in a network. The arbiter algorithm is described at three levels of abstraction: a high-level specification, a graph-theoretic model, and a distributed implementation. The high-level model defines the arbiter's correctness conditions, including mutual exclusion and no lockout. The graph-theoretic model represents the arbiter as an acyclic graph with users at the leaves and arbiter nodes in the interior. The distributed implementation details the protocol for individual processes. The authors address the limitations of existing process languages like CCS and CSP, which lack a clear distinction between internal and external events. They propose the input-output automaton model, which distinguishes between input (external) and output (internal) actions. This model allows for the formalization of fairness and the simulation of higher-level algorithms at lower levels. The paper defines the input-output automaton, its composition, and fairness conditions. It introduces the concept of a possibilities mapping to relate the states of different automata. The authors then use this model to construct a hierarchical correctness proof for Schönhage's arbiter, showing that the low-level implementation satisfies the high-level specification. The paper concludes with a discussion of the model's potential for expressing asynchronous distributed algorithms while maintaining clean automata-theoretic semantics. The hierarchical approach allows for the decomposition of complex algorithms into simpler, more manageable components, enabling rigorous verification of their correctness.This paper introduces the input-output automaton model for asynchronous distributed algorithms, enabling modular and hierarchical correctness proofs. The model allows for the formalization of high-level algorithmic ideas and their rigorous simulation at lower levels. The authors present a hierarchical approach to proving the correctness of Schönhage's distributed arbiter algorithm, which manages resource allocation in a network. The arbiter algorithm is described at three levels of abstraction: a high-level specification, a graph-theoretic model, and a distributed implementation. The high-level model defines the arbiter's correctness conditions, including mutual exclusion and no lockout. The graph-theoretic model represents the arbiter as an acyclic graph with users at the leaves and arbiter nodes in the interior. The distributed implementation details the protocol for individual processes. The authors address the limitations of existing process languages like CCS and CSP, which lack a clear distinction between internal and external events. They propose the input-output automaton model, which distinguishes between input (external) and output (internal) actions. This model allows for the formalization of fairness and the simulation of higher-level algorithms at lower levels. The paper defines the input-output automaton, its composition, and fairness conditions. It introduces the concept of a possibilities mapping to relate the states of different automata. The authors then use this model to construct a hierarchical correctness proof for Schönhage's arbiter, showing that the low-level implementation satisfies the high-level specification. The paper concludes with a discussion of the model's potential for expressing asynchronous distributed algorithms while maintaining clean automata-theoretic semantics. The hierarchical approach allows for the decomposition of complex algorithms into simpler, more manageable components, enabling rigorous verification of their correctness.