Formal Analysis of Quantum Systems using Process Calculus
Formal Analysis of Quantum Systems using Process Calculus
复制标题
DOI：
10.4204/eptcs.59.9
复制
发表时间：
2011-08
期刊：
影响因子：
--
通讯作者：
T. A. Davidson;S. Gay;R. Nagarajan
中科院分区：
文献类型：
--
作者：
T. A. Davidson;S. Gay;R. Nagarajan
量子通信和密码协议正在成为一项重要的实用技术。虽然大量的成功的研究已经做了证明他们的正确性，大多数这些工作并没有利用熟悉的技术，从形式化的方法，如规范的形式逻辑，形式化建模语言，抽象层次的分离，组合分析。我们认为，这些技术将是必要的大规模系统的分析，结合联合收割机量子和经典组件，并总结了初步调查的结果，使用行为等价过程演算。本文是西蒙·盖伊在ICE'11上的特邀演讲的摘要。
Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods, such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and compositional analysis. We argue that these techniques will be necessary for the analysis of large-scale systems that combine quantum and classical components, and summarize the results of initial investigation using behavioural equivalence in process calculus. This paper is a summary of Simon Gay's invited talk at ICE'11.