AI 中文总结
研究针对量子进程演算难以提供空间组合性的问题，提出用德伊茨 - 海登描述符建模，调整后得到新进程演算，能给出系统状态局部视图，定义了进程等价概念并展示双模拟，还可对开放系统建模，成功跟踪量子比特移动。
AI 中文摘要
我们提出了一种量子进程演算，它能沿进程边界分割系统状态，并独立跟踪每个进程的演化，而不丢失关于联合状态的信息，此特性称为空间组合性。组合性是推理任何复杂系统的关键，但量子进程演算一直难以提供空间组合性。我们提议用德伊茨 - 海登描述符对量子态建模，它能提供量子比特态及其演化的模块化表示。我们对这些描述符进行调整，允许对量子比特存储进行任意分割和合并，从而得到一种不同寻常的进程演算。在此演算中，量子比特传输消息携带量子比特的实际状态，而现有演算仅传输引用。该演算给出了每个进程可见的系统状态的局部视图，这些视图可重新组合成联合状态。我们定义了基于物理学有充分依据的进程等价概念，并展示了一种双模拟，其可靠性证明因空间组合性而简化。该演算可对与外部进程纠缠的开放系统进行建模，我们在BB84密钥分发协议的一个片段上展示了此能力。此示例表明德伊茨 - 海登描述符能成功跟踪量子比特跨进程和系统边界的移动，不过在推理信息流时需要密度矩阵的帮助。
英文摘要
We present a quantum process calculus that can split the system state along process boundaries and follow the evolution of each process in isolation, without losing information about the joint state-a property we call spatial compositionality. Compositionality is the key to reasoning about any complex system, yet quantum process calculi have struggled to provide its spatial kind, which would enable analyzing a system one process at a time. Many a quantum process calculi have been proposed, but they invariably rely on a global state representation based on state vectors or density matrices, with no known way to split them without losing information about entanglement. We propose to model quantum states with Deutsch-Hayden descriptors instead, which provide a modular representation of qubit states and their evolution. We adapt these descriptors to allow arbitrary splitting and merging of the store of qubits, leading to an unusual process calculus in which qubit transfer messages carry the actual state of the qubit, where existing calculi transfer only a reference. The calculus gives localized views of system state visible to each process, which can be assembled back together into the joint state. We define a notion of process equivalence with extensive justification grounded in physics and show a bisimulation whose soundness proof is simplified by spatial compositionality. The calculus can model open systems entangled with external processes, and we demonstrate this capability on a fragment of the BB84 key distribution protocol. This exercise shows that Deutsch-Hayden descriptors can successfully track qubit movements across process and system boundaries, though it needs help from density matrices to reason about information flow.
Comments27 pages
