一句话：证明在异步通信下，增强服务器为转发器后 must-前序的标准刻画仍成立，并在 Rocq 中机械化。
De Nicola 与 Hennessy 的 must-前序是保持活性的精化：若 p 满足的所有客户端也被 q 满足，则 q 精化 p。该定义对客户端全称量化，缺乏实用证明方法；在输出非阻塞的异步语义下，替代刻画尤其困难，过往多用特设定义。本文证明，若将服务器增强为转发器——可输入任意消息并把它存回共享缓冲区——则 must-前序的标准刻画可原样推广到异步通信。工作在 Rocq 中构造性机械化，不依赖特定演算；结果适用于 Selinger 的带反馈输出缓冲 agent，即通过共享无序缓冲区通信的标号迁移系统，涵盖异步 CCS 与异步 π 演算。标准共归纳刻画可用于在 Rocq 中证明这类系统间的 must-前序关系，并显示 Brouwer 的 bar induction 对推理保持活性的程序变换很有用。
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.
DOI 原文 ·
@inproceedings{paperbot3947,
title = {Constructive characterisations of the
<scp>must</scp>
-preorder for asynchrony},
author = {Giovanni Bernardi and Ilaria Castellani and Paul Laforgue and Vincent Padovani and Léo Stefanesco},
booktitle = {TOPLAS},
year = {2026},
doi = {10.1145/3842749}
}