（不同步）必须前序关系的统一特征
计算机科学中的逻辑
2026-05-05 v1 编程语言
摘要
在消息传递软件中，De Nicola 和 Hennessy 必须前序定义程序如何在另一个程序上进行改进。由于该前序缺乏可行的证明方法，使用它需要一种特征化它的替代关系。文献中至少有四种不同的替代前序定义，取决于通信是同步的还是异步的，以及是否存在值传递。这些不同定义的存在使整体理论复杂化，阻碍工具的开发，整体上表明对必要且充分条件的理解仍不完整。本文提出首个在上述四种设置中均可工作的替代特征化方法。我们通过一种与计算无关的公理化方法实现了这一目标，通过突出阻塞动作和非阻塞动作的作用，并引入新颖的标签抽象概念。标签抽象捕捉了关于安全可替代性的核心，让我们能够获得在所有所述设置中均唯一的 soundness 与 completeness 证明。我们认为这拓展了整体理论的范围，同时让我们能够以统一的方式呈现现有结果。我们的证明是构造性的，且结果在 Rocq 中完全机械化。
引用
@article{arxiv.2605.02362,
title = {A uniform characterisation of the (a)synchronous must-preorder},
author = {Giovanni Bernardi and Hugo Férée and Gaëtan Lopez},
journal= {arXiv preprint arXiv:2605.02362},
year = {2026}
}