基于 Barb 与上下文的量子互模拟：抑制非确定性观察者的能力

过去几年中，出现了若干量子进程演算扩展的提案。其动机很明确：随着量子通信协议的发展，需要抽象并聚焦于量子并发系统的基本特性，正如 CCS 对其经典对应物所做的那样。然而迄今为止，无论是语法还是行为语义，都尚未出现公认标准。事实上，各种提案在量子值的观测属性上并未达成一致，并且这类属性的合理性也从未依据量子理论的规范加以验证。为此，我们引入一种新的演算——线性量子 CCS（Linear Quantum CCS），并研究基于 barb 与上下文的行为等价性的特征。我们的演算可视为 qCCS（基于值传递 CCS）的异步线性版本。线性确保每一个量子比特恰好被发送一次，从而精确指定进程的哪些量子比特与上下文发生交互。我们利用上下文来考察互模拟与量子理论的关系。我们表明，通用上下文的观测能力是与量子理论不相容的：粗略地说，它们可在不测量（从而不扰动）量子值的情况下，依据量子值执行非确定性移动。因此，我们精炼了操作语义，以阻止上下文执行不可行的非确定性选择。这诱导出一种更粗的互模拟，更契合量子环境：(i) 它将量子态的不可区分性提升到了进程分布层面，且 (ii) 尽管存在额外约束，仍保持了基于经典信息的非确定性选择的表达力。据我们所知，我们的语义是首个同时满足上述两个性质的语义。