Paul Laforgue

Constructive characterisations of the must-preorder for asynchrony

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...