M Mukund, K Narayan Kumar, J Radhakrishnan and M Sohoni
Proc. ICALP '98, Springer LNCS 1443 (1998) 188-199.
© Springer-Verlag Berlin Heidelberg
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.