Formal verification techniques using quantum process calculus
Formal verification techniques using quantum process calculus
复制标题
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
T. A. Davidson
中科院分区：
文献类型：
--
作者：
T. A. Davidson
量子通信是一个快速增长的研究和开发领域。虽然大规模量子计算机的成功构建可能还需要几年的时间，但已经有了使用量子密码学进行安全通信的商业实现。形式化方法在经典通信和密码系统中的应用已经非常成功，现在被英特尔、微软和NASA等组织广泛应用于工业领域。我们有理由相信，量子系统的验证也会有类似的好处。在这篇论文中，我们将重点放在使用进程演算，特别是通信量子进程（CQP），分析量子协议。同余关系是过程演算的一个重要方面，因为它们为等式推理提供了基础。先前关于量子过程的同余关系的工作排除了测量产生的经典信息，因此无法分析许多有趣的已知量子通信协议。由于测量、纠缠和平行合成之间的相互作用，发展一般量子过程的同余关系是困难的。我们定义了一个标记的过渡关系CQP，以描述外部的相互作用。基于这种语义，我们定义了CQP过程的观测等价性概念，即概率分支双相似性。我们发现，这种关系是不保留的平行组成，但我们能够获得更深入的了解概率分支和测量之间的联系。基于这种新的理解，我们提出了一种新的语义量子过程，结合混合量子态的概率分支。对于这个新的语义模型，我们定义了完全概率分支双相似性，并证明了它是一个同余。我们使用这个同余关系来讨论一个公理化的方法来验证量子过程。本文以量子隐形传态协议为例，证明了它与量子信道是一致的。我们定义了一个翻译从CQP到量子模型的验证（QMC），以提供自动化验证技术，使用CQP规范。我们证明，这种翻译保留了CQP过程的语义，从而使一个多方面的方法，通过加强手动技术的过程演算的好处，模型检查的正式验证。
Quantum communication is a rapidly growing area of research and development. While the successful construction of a large-scale quantum computer may be some years away, there are already commercial implementations of secure communication using quantum cryptography. The application of formal methods to classical communication and cryptographic systems has been very successful, and is now widely used in industry by organisations such as Intel, Microsoft and NASA. There is reason to believe that similar benefits can be expected for the verification of quantum systems. In this thesis, we focus on the use of process calculus, specifically Communicating Quantum Processes (CQP), for the analysis of quantum protocols. Congruence relations are an important aspect of process calculus, since they provide the foundation for equational reasoning. Previous work on congruence relations for quantum processes excluded the classical information arising from measurements, and was therefore unable to analyse many of the interesting known quantum communication protocols. Developing a congruence relation for general quantum processes is difficult because of the interaction between measurement, entanglement and parallel composition. We define a labelled transition relation for CQP in order to describe external interactions. Based on this semantics, we define a notion of observational equivalence for CQP processes, namely probabilistic branching bisimilarity. We find that this relation is not preserved by parallel composition, however we are able to gain a deeper understanding of the link between probabilistic branching and measurement. Based on this newfound understanding, we present a novel semantics for quantum processes, combining mixed quantum states with probabilistic branching. With respect to this new semantic model, we define full probabilistic branching bisimilarity and prove that it is a congruence. We use this congruence relation to discuss an axiomatic approach to the verification of quantum processes. The quantum teleportation protocol is used as a primary example throughout, and we prove that it is congruent to a quantum channel. We define a translation from CQP to the Quantum Model Checker (QMC) in order to provide automated verification techniques using CQP specifications. We prove that this translation preserves the semantics of CQP processes, thereby enabling a multifaceted approach to formal verification by enhancing the manual techniques of process calculus with the benefits of model checking.