Robust asynchronous protocols are finite-state

Abstract

We consider networks of finite-state machines which communicate over reliable channels which may reorder messages. Each machine in the network also has a local input tape. Since channels are unbounded, the network as a whole is, in general, infinite-state. An asynchronous protocol is a network equipped with an acceptance condition. Such a protocol is said to be robust if it never deadlocks and, moreover, it either accepts or rejects each input in an unambiguous manner. The behaviour of a robust protocol is insensitive to nondeterminism introduced by either message reordering or the relative speeds at which components read their local inputs. Using an automata-theoretic model, we show that, at a global level, every robust asynchronous protocol has a finite-state representation. To prove this, we establish a variety of pumping lemmas. We also demonstrate a distributed language which does not admit a robust protocol.