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