验证采用物理可接受调度器的量子协议

量子通信协议的可靠验证技术极其重要，因其高昂的实现成本和关键应用场景。然而，标准概率模型引入的非确定性能力并未与物理量子系统的观察属性一致，导致判等性质区分物理等价过程。与此同时，非确定性特征对于建模输入、环境和对手行为至关重要。为此，我们提出 lqCCS，一种集成并发、非确定性与量子能力的过程演算。我们引入一种以分布为语义的新模型，显式的物理可接受调度器约束概率组成，禁止非法定义的非确定性操作，同时保留建模真实协议所需的表达力。我们研究基于调度的饱和判等性质，若无观察者能区分两个过程则将其配对，并通过将量子力学中一个已知结果提升至 lqCCS 验证了其充分性：在不可辨识量子态混合物上作用的等价过程被正确识别为判等。最后，我们给出另一种语义和基于量子概率分布推广的标记判等性。这一描述了我们的行为等价性质对于并行算子是同构性，无需显式检查所有可能的上下文即可进行组成推理。我们描述了一类 lqCCS 过程，其等价性可使用标准技术判定，并分析了真实世界的量子通信协议。