Model Checking for Communicating Quantum Processes
Model Checking for Communicating Quantum Processes
复制标题
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
T. A. Davidson;S. Gay;Hynek Mlnarik;R. Nagarajan;N. Papanikolaou
中科院分区：
文献类型：
--
作者：
T. A. Davidson;S. Gay;Hynek Mlnarik;R. Nagarajan;N. Papanikolaou
量子通信是一个快速增长的研究和开发领域。量子密码学已经实现了安全通信，并且可以使用商业解决方案。形式化方法在经典计算和通信系统中的应用已经非常成功，并被工业界广泛使用。我们期望量子系统的验证也有类似的好处。通信量子过程（CQP）是一种基于π演算的过程演算，包含了量子信息的原语。过程演算提供了一种代数方法来系统规范和行为分析。量子模型验证（QMC）是一种自动验证系统正确性的工具。通过对可能执行的穷举搜索，QMC可以检查使用时序逻辑公式表示的正确性属性是否满足。在本文中，我们描述了我们的方法来验证量子系统的过程演算和模型检查的组合。我们还定义了一个正式的翻译CQP的建模语言所使用的QMC，并证明这保留了所有支持的CQP过程的语义。© 2012 Old City Publishing，Inc.
Quantum communication is a rapidly growing area of research and development. Quantum cryptography has already been implemented for secure communication, and commercial solutions are available. The application of formal methods to classical computing and communication systems has been very successful, and is widely used by industry. We expect similar benefits for the verification of quantum systems. Communicating Quantum Processes (CQP) is a process calculus based on the π-calculus with the inclusion of primitives for quantum information. Process calculi provide an algebraic approach to system specification and behavioural analysis. The Quantum Model Checker (QMC) is a tool for the automated verification of system correctness. Through an exhaustive search of the possible executions, QMC can check that correctness properties expressed using temporal logic formulae are satisfied. In this paper we describe our approach to the verification of quantum systems using a combination of process calculus and model checking. We also define a formal translation from CQP to the modelling language used by QMC and prove that this preserves the semantics of all supported CQP processes. © 2012 Old City Publishing, Inc.