De Nicola and Hennessy’s must-preorder is a contextual 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 for the must-preorder, and alternative characterisations are necessary to reason on it.
In this seminar I will present the first characterisations of the must-preorder that are constructive, supported by a mechanisation in Coq, and independent from any calculus: the results pertain to Selinger output-buffered agents with feedback, which are a semantic model of asynchronous calculi.
To spur discussion, I will also summarise relevant related works, and recall historical comparisons with bisimilarity.
To the best of our knowledge, our results are the first ones showing that the alternative preorders which capture the must-preorder in synchronous settings do the job also in asynchronous ones, if servers are enhanced via forwarding.
This allows us to develop only _one_ proof of completeness and only _one_ proof of soundness for both synchronous and asynchronous settings.
Join at: imt.lu/guinigi