Constructive characterisations of the must-preorder for asynchrony

Abstract

De Nicola and Hennessy's must-preorder is a liveness preserving refinement which states that a server q refines a server p if all clients satisfied by p are also satisfied by q. Owing to the universal quantification over clients, this definition does not yield a practical proof method, and alternative characterisations are necessary to reason over it. Finding these characterisations for asynchronous semantics, i.e. where outputs are non-blocking, has thus far proven to be a challenge, usually tackled via ad-hoc definitions. We show that the standard characterisations of the must-preorder carry over as they stand to asynchronous communication, if servers are enhanced to act as forwarders, ie they can input any message as long as they store it back into the shared buffer. Our development is constructive, is completely mechanised in Rocq, and is independent of any calculus: our results pertain to Selinger output-buffered agents with feedback. This is a class of Labelled Transition Systems that represents programs that communicate via a shared unordered buffer, as in asynchronous CCS or the asynchronous \(\pi\) -calculus. We show that the standard coinductive characterisation lets us prove in Rocq that such Labelled Transition Systems are related by the must-preorder. Finally, our proofs show that Brouwer's bar induction principle is a useful technique to reason on liveness preserving program transformations.