First-order axioms for asynchrony

Abstract

We study properties of asynchronous communication independently of any concrete concurrent process paradigm. We give a general-purpose, mathematically rigorous definition of several notions of asynchrony in a natural setting where an agent is asynchronous if its input and/or output is filtered through a buffer or a queue, possibly with feedback. In a series of theorems, we give necessary and sufficient conditions for each of these notions in the form of simple first-order or second-order axioms. We illustrate the formalism by applying it to asynchronous CCS and the core join calculus.